# A Secure and Efficient Three-Factor Authentication Protocol in Global Mobility Networks
## 6 Security Analysis
### Authentication Proof Using BAN Logic
#### 6.3.1 Rules of BAN Logic  
The rules of BAN logic are summarized as follows.  
\begin{table}
\begin{tabular}{c c} \hline \hline
**Notation** & **Description** \\ \hline \(A\)\(|\equiv\)\(B\) & \(A\)**believes** & that \(B\) \\ \hline \(\#\)\(B\) & \(B\) is updated and **fresh** \\ \hline \(A\)\(\lhd\)\(B\) & \(A\)**sees** that \(B\) \\ \hline \(A\)\(|\sim\)\(B\) & \(A\) once **said**\(B\) \\ \hline \(A\)\(\Rightarrow\)\(B\) & \(A\)**controls** that \(B\) \\ \hline \(<\)\(B\)\(>_{W}\) & \(B\) is **combined** with \(W\) \\ \hline \(\{B\}_{K}\) & \(B\) is **encrypted** utilizing symmetric key \(K\) \\ \hline \(A\)\(\bigtimes\)\(P\) & \(A\) and \(P\) can make secure contact utilizing \(K\) as the **shared secret key** \\ \hline \(SK\) & Session key used in communication session \\ \hline \hline \end{tabular}
\end{table}
Table 4: Notations used for BAN logic.  
\begin{table}
\begin{tabular}{c c c c c} \hline \hline
**Security features** & **[PERSON] et al. [6]** & **[PERSON] et al. [8]** & **[PERSON] et al. [15]** & **[PERSON] et al. [16]** & **Ours** \\ \hline User anonymity & \(\times\) & \(\times\) & \(\circ\) & \(\circ\) & \(\circ\) \\ \hline User friendliness & \(\circ\) & \(\circ\) & \(\circ\) & \(\circ\) & \(\circ\) \\ \hline Mutual authentication & \(\times\) & \(\circ\) & \(\circ\) & \(\times\) & \(\circ\) \\ \hline Insider attack & \(\circ\) & \(\circ\) & \(\circ\) & \(\circ\) & \(\circ\) \\ \hline Replay attack & \(\circ\) & \(\times\) & \(\circ\) & \(\times\) & \(\circ\) \\ \hline Perfect forward secrecy attack & \(\circ\) & \(\circ\) & \(\circ\) & \(\circ\) & \(\circ\) \\ \hline Session key disclosure attack & \(\times\) & \(\times\) & \(\circ\) & \(\times\) & \(\circ\) \\ \hline Masquerade attack & \(\times\) & \(\circ\) & \(\circ\) & \(\times\) & \(\circ\) \\ \hline \hline \end{tabular}
\end{table}
Table 3: Security features compared to existing schemes.  
1. Message meaning rule : \[\frac{A\bigm{|}\equiv A\stackrel{{\mathcal{K}}}{{\leftrightarrow}}P, \quad A\lhd\left\{B\right\}_{K}}{A\bigm{|}\equiv P\bigm{|}\sim B}\]
2. Nonce verification rule : \[\frac{A\bigm{|}\equiv\#(B),\quad A\bigm{|}\equiv P\bigm{|}\sim B}{A\bigm{|} \equiv P\bigm{|}\equiv B}\]
3. Jurisdiction rule : \[\frac{A\bigm{|}\equiv P\bigm{|}\Longrightarrow B,\quad A\bigm{|}\equiv P\bigm{|} \equiv B}{A\bigm{|}\equiv B}\]
4. Freshness rule : \[\frac{A\bigm{|}\equiv\#(B)}{A\bigm{|}\equiv\#(B,W)}\]
5. Belief rule : \[\frac{A\bigm{|}\equiv(B,W)}{A\bigm{|}\equiv B}\]  
6.3.2. Goals  
To analyze mutual authentication, we define the goals of our protocol as below.  
1. \(MU\bigm{|}\equiv(MU\stackrel{{\mathcal{SK}}}{{\longleftrightarrow}}FA)\)
2. \(FA\bigm{|}\equiv(MU\stackrel{{\mathcal{SK}}}{{\longleftrightarrow}}FA)\)
3. \(MU\bigm{|}\equiv FA\bigm{|}\equiv(MU\stackrel{{\mathcal{SK}}}{{ \longleftrightarrow}}FA)\)
4. \(FA\bigm{|}\equiv MU\bigm{|}\equiv(MU\stackrel{{\mathcal{SK}}}{{ \longleftrightarrow}}FA)\).  
6.3.3. Idealized Forms  
The idealized form of messages of our protocol are as below.  
1. \(MU\to FA\): \((RID_{i},ID_{MU},R_{MU})_{X_{i}}\)
2. \(FA\to HA\): \((RID_{i},ID_{MU},R_{MU},X_{i},R_{FA},ID_{FA})_{K_{FH}}\)
3. \(HA\to FA\): \((ID_{MU},ID_{FA},R