## 6 Security Analysis
### Authentication Proof Using BAN Logic  
BAN logic is a well-known tool, which provides a mutual authentication proof of cryptographic protocols [27]. Based on the rules and analytical logic defined in the tool, I aim to prove that \(P_{i}\) and \(P_{j}\) believe the key \(K_{i,j}\) computed as a shared secret known only to them. Some notations I use for the proof are described as follows. * \(A\ |\equiv X\): \(A\) believes statement \(M\). * \(A\ \lhd M\): \(A\) sees statement \(M\). * \(\#(M)\): Formula \(M\) is fresh. * \(A\ |\sim M\): \(A\) once said statement \(M\). * \((M,N)\): \(M\) or \(N\) is one part of formula \((M,N)\). * \(A\ \Longrightarrow M\): \(A\) has jurisdiction over statement \(M\). * \(\langle M\rangle_{N}\): This represents \(M\) combined with formula \(N\). * \(A\ \stackrel{{ K}}{{\leftrightarrow}}\ B\): Value \(K\) is known only to \(A\) and \(B\), and it is used for their communication. * \(A\ \stackrel{{ M}}{{\leftrightarrow}}\ B\): Formula \(M\) is a secret known only by \(A\) and \(B\). Only \(A\) and \(B\) can use \(M\) to authenticate each other. Based on the principle of BAN logic and the procedure of the proposed protocol, the following six authentication goals should be satisfied. \(\textit{Goal 1}\): \(S_{m}\ |\equiv\Big{(}S_{m}\stackrel{{ R_{i,m}}}{{\leftrightarrow}}P_{i} \Big{)}\). \(S_{m}\) believes \(R_{i,m}\) is a secret value sent by \(P_{i}\), and \(R_{i,m}\) is a secret key shared by \(S_{m}\) and \(P_{i}\). \(\textbf{(G1)}\) \(\textit{Goal 2}\): \(P_{i}\ |\equiv\Big{(}P_{i}\stackrel{{ R_{i,m}}}{{\leftrightarrow}}S_{m} \Big{)}\). \(P_{i}\) believes \(R_{i,m}\) is a secret key shared by \(P_{i}\) and \(S_{m}\). \(\textbf{(G2)}\) \(\textit{Goal 3}\): \(S_{n}\ |\equiv\Big{(}S_{n}\stackrel{{ R_{j,n}}}{{\leftrightarrow}}P_{j} \Big{)}\). \(S_{n}\) believes \(R_{j,n}\) is a secret value sent by \(P_{j}\), and \(R_{j,n}\) is a secret key shared by \(S_{n}\) and \(P_{j}\). \(\textbf{(G3)}\) \(\textit{Goal 4}\): \(P_{j}\ |\equiv\Big{(}P_{j}\stackrel{{ R_{i,m}}}{{\leftrightarrow}}S_{n} \Big{)}\). \(P_{j}\) believes \(R_{j,n}\) is a secret key shared by \(P_{j}\) and \(S_{n}\). \(\textbf{(G4)}\) \(\textit{Goal 5}\): \(P_{i}\ |\equiv\Big{(}P_{i}\stackrel{{ K_{i,j}}}{{\leftrightarrow}}P_{j} \Big{)}\). \(P_{i}\) believes \(K_{i,j}\) is a secret value sent by \(P_{j}\), and \(K_{i,j}\) is a secret key shared by \(P_{i}\) and \(P_{j}\). \(\textbf{(G5)}\)_Goal 6:_\(P_{j}\ |\equiv\left( \begin{array}{c}F_{j}\stackrel{{ K_{i,j}}}{{\leftrightarrow}}P_{i} \end{array} \right)\). \(P_{j}\) believes \(K_{i,j}\) is a secret value sent by \(P_{t}\), and \(K_{i,j}\) is a secret key shared by \(P_{j}\) and \(P_{i}\). (**G6**)  
I consider four messages communicated in the login and authentication phase for the analysis, described as follows. _Message 1._\(P_{i}\to S_{m}:(a_{i,m}.G,y_{i,m1}. (u_{i,m}||ID_{i})\oplus T_{i,m} mod\ p,y_{i,m2}.t_{i,m1} mod\ p,y_{i,m2}.t_{i,m2} mod\ p,T_{i,m})\). _Message 2._\(S_{m}\to P_{i}:(b_{m,i}.G,b_{m,i}.T_{n,j},h(Y_{m,j}||K_{m,j}||ID_{i}||ID_{S_{m}}) )_{K_{i,m}}\). _Message 3._\(P_{j}\to S_{n}:(a_{i,m}.G,y_{i,m1}. (u_{j,m1}||ID_{j})\oplus T_{i,m} mod\ p,y_{i,m2}.t_{i,m1} mod\ p,y_{i,m2}.t_{j,m2} mod\ p,T_{j,n})\). _Message 4._\(S_{m}\to P_{j}:(b_{n,j}.G,b_{n,j}.Y_{m,j},h(Y_{n,j}||K_{n,j}||ID_{j}||ID_{S_{m}}) )_{K_{j,n}}\). The idealized form of these messages used in the BAN logic is given below. _Message 1._\(P_{i}\to S_{m}:((C_{i,m1},c_{i,m21}.s_{i,m},a_{i,m})\chi_{x,n},T_{i,m})\). _Message 2._\(S_{m}\to P_{i}:(b_{m,i}.G,b_{m,i}.T_{n,j},h(Y_{m,j},K_{m,j},ID_{i},ID_{S_{m}}) )\chi_{x_{i,m}}\). _Message 3._\(P_{j}\to S_{n}:((C_{j,m1},c_{j,m21}.s_{j,m},a_{j,n})\chi_{x,n},T_{i,m})\). _Message 4._\(S_{n}\to P_{j}:(b_{n,j}.G,b_{n,j}.Y_{m,j},h(Y_{n,j},K_{m,j},ID_{j},ID_{S_{n}}) )\chi_{y,n}\). Some logical rules provided  
\(S_{13}\): Based on A6, \(S_{12}\) and the rule of the protocol, we obtain \(P_{i}\mid\equiv\left(P_{i}\overset{R_{i,m}}{\leftrightarrow}S_{m}\right)\) (**G2** achieved).