# A Secure and Efficient Three-Factor Authentication Protocol in Global Mobility Networks
## 6 Security Analysis
### Authentication Proof Using BAN Logic
#### 6.3.5 Proof Using BAN Logic  
The proof then proceeds as below:  
**Step 1:**: According to \(Msg_{1}\), we obtain the following  
\[(S_{1}):FA\lhd(RID_{i},ID_{MU},R_{MU})_{X_{i}}.\]
**Step 2:**: Utilizing \(S_{1}\) and \(A_{1}\) with the \"message meaning rule\", the following is obtained  
\[(S_{2}):FA\mid\equiv MU\mid\sim(RID_{i},ID_{MU},R_{MU})_{X_{i}}.\]
**Step 3:**: Now, using \(S_{2}\) and \(A_{2}\) with the \"freshness rule\", the following is obtained  
\[(S_{3}):FA\mid\equiv\#(RID_{i},ID_{MU},R_{MU})_{X_{i}}.\]
**Step 4:**: Utilizing \(S_{2}\) and \(S_{3}\) with the \"nonce verification rule\", we obtain  
\[(S_{4}):FA\mid\equiv MU\mid\equiv(RID_{i},ID_{MU},R_{MU})_{X_{i}}.\]
**Step 5:**: Utilizing \(S_{4}\) and the \"belief rule\", we obtain  
\[(S_{5}):FA\mid\equiv MU\mid\equiv(R_{MU})_{X_{i}}.\]
**Step 6:**: According to \(Msg_{2}\), we obtain  
\[(S_{6}):HA\lhd(RID_{i},ID_{MU},R_{MU},X_{i},R_{FA},ID_{FA})_{K_{FH}}.\]
**Step 7:**: Utilizing the \(S_{6}\) and \(A_{3}\) with the \"message meaning rule\", the following is obtained  
\[(S_{7}):HA\mid\equiv FA\mid\sim(RID_{i},ID_{MU},R_{MU},X_{i},R_{FA},ID_{FA})_{ K_{FH}}.\]
**Step 8:**: Now, using \(S_{7}\) and \(A_{4}\) with the \"freshness rule\", we obtain  
\[(S_{8}):HA\mid\equiv\#(RID_{i},ID_{MU},R_{MU},X_{i},R_{FA},ID_{FA})_{K_{FH}}.\]
**Step 9:**: Utilizing \(S_{7}\) and \(S_{8}\) with the \"nonce verification rule\", the following is obtained  
\[(S_{9}):HA\mid\equiv FA\mid\equiv(RID_{i},ID_{MU},R_{MU},X_{i},R_{FA},ID_{FA}) _{K_{FH}}.\]
**Step 10:**: According to \(Msg_{3}\), we obtain  
\[(S_{10}):FA\lhd(ID_{FA},R_{FA},R_{MU})_{K_{FH}}.\]
**Step 11:**: Utilizing \(S_{10}\) and \(A_{5}\) with the \"message meaning rule\", the following is obtained  
\[(S_{11}):FA\mid\equiv HA\mid\sim(ID_{FA},R_{FA},R_{MU})_{K_{FH}}.\]
**Step 12:**: Now, using \(S_{11}\) and \(A_{6}\) with the \"freshness rule\", we obtain  
\[(S_{12}):FA\mid\equiv\#(ID_{FA},R_{FA},R_{MU})_{K_{FH}}.\]
**Step 13:**: Utilizing \(S_{11}\) and \(S_{12}\) with the \"nonce verification rule\", the following is obtained  
\[(S_{13}):FA\mid\equiv HA\mid\equiv(ID_{FA},R_{FA},R_{MU})_{K_{FH}}.\]Step 14:According to \(Msg_{4}\), we could obtain  
\[(S_{14}):MU\lhd(ID_{MUL},R_{MU},R_{FA},(MU\xleftrightarrow{SK}FA))_{X_{i}}.\]  
Step 15:Utilizing \(S_{14}\) and \(A_{7}\) with the \"message meaning rule\", we obtain  
\[(S_{15}):MU\mid\equiv FA\mid\sim(ID_{MU},R_{MU},R_{FA},(MU\xleftrightarrow{ SK}FA))_{X_{i}}.\]  
Step 16:Now, using \(S_{15}\) and \(A_{8}\) with the \"freshness rule\", the following is obtained  
\[(S_{16}):MU\mid\equiv\#(ID_{MU},R_{MU},R_{FA},(MU\xleftrightarrow{SK}FA))_{X_{ i}}.\]  
Step 17:Utilizing \(S_{15}\) and \(S_{16}\) with the \"nonce verification\", we obtain  
\[(S_{17}):MU\mid\equiv FA\mid\equiv(ID_{MU},R_{MU},R_{FA},(MU\xleftrightarrow{ SK}FA))_{X_{i}}.\]  
Step 18:Utilizing \(S_{17}\) and the belief rule, we obtain  
\[(S_{18}):MU\mid\equiv FA\mid\equiv(MU\xleftrightarrow{SK}FA).\qquad\textbf{( Goal 3)}\]  
Step 19:Now, using \(S_{18}\) and \(A_{9}\) with the \"jurisdiction rule\", the following is obtained  
\[(S_{19}):MU\mid\equiv(MU\xleftrightarrow{SK}FA).\qquad\textbf{( Goal 1)}\]  
Step 20:Because of \(SK=h(R_{MU}||R_{FA})\), from the \(S_{5}\), \(S_{9}\), \(S_{13}\) and \(S_{17}\) we obtain  
\[(S_{20}):FA\mid\equiv MU\mid\equiv(MU\xleftrightarrow{SK}FA).\qquad\textbf{( Goal 4)}\]  
Step 21:Utilizing \(S_{19}\) and \(A_{10}\) with the \"jurisdiction rule\", we obtain  
\[(S_{21}):FA\mid\equiv(MU\xleftrightarrow{SK}FA).\qquad\textbf{( Goal 2)}\]  
Based on goals 1 to 4, we proved that \(MU\), \(FA\), and \(HA\) are securely mutually authenticated. We assessed that the proposed scheme ensured mutual authentication between \(MU\), \(FA\), and \(HA\).