# A Novel Mobile Communications Authentication Scheme with Roaming Service and User Anonymity
## 4 BAN-Logic Analysis
### Authentication Proof Based on BAN-logic  
We use the rules of BAN-logic to represent the authentication phase in our proposed scheme and describe these messages as follows:  
1. \(\text{m}_{\text{V1}}\). MU\(\rightarrow\)FA: \(((<\)ID\({}_{\text{MU}}\)\(>\)H\({}_{\text{I}}\)(X\({}_{\text{I}}\)\(\mid\) 1 \(\text{T}_{\text{MU}}\)), <X\({}_{\text{I}}\), H\({}_{\text{I}}\)(ID\({}_{\text{MU}}\)\(\mid\) 1 \(\text{N}\)\(\mid\) 1 \(\text{W}_{\text{i}}\))\(>\)H\({}_{\text{2}}\)(PW\({}_{\text{MU}}\)\(\oplus\)\({}_{\text{n}}\)), H\({}_{\text{3}}\)(W\({}_{\text{i}}\)), \(W_{\text{i}}\), \(X\), ID\({}_{\text{HA}}\))\(|_{\text{EC}}\)
2. \(\text{m}_{\text{V2}}\). FA\(\rightarrow\)HA: \(((<\)ID\({}_{\text{MU}}\)\(>\)H\({}_{\text{I}}\)(X\({}_{\text{I}}\)\(\mid\) 1 \(\text{T}_{\text{MU}}\)), <X\({}_{\text{I}}\), H\({}_{\text{II}}\)(ID\({}_{\text{MU}}\)\(\mid\) 1 \(\text{N}\)\(\mid\) 1 \(\text{W}_{\text{i}}\))\(>\)H\({}_{\text{2}}\)(PW\({}_{\text{MU}}\)\(\oplus\)\({}_{\text{n}}\)), H\({}_{\text{3}}\)(W\({}_{\text{i}}\)), \(W_{\text{i}}\), \(X\), Y)\(|_{\text{R}}|_{\text{SK}_{\text{HF}}}\)
3. \(\text{m}_{\text{V3}}\). HA\(\rightarrow\)FA: \(((\text{W}_{\text{i}}\), \(X\), Y, ID\({}_{\text{HA}}\), ID\({}_{\text{EA}}\))\(|_{\text{SK}_{\text{HF}}}\)
4. \(\text{m}_{\text{V4}}\). FA\(\rightarrow\)MU:\(\{\text{TCert}_{\text{MU}}\)\(<\)MU\(<\)-SK\(\rightarrow\)FA>  
To analyze our proposed scheme, we made the following assumptions without loss of generality:  
1. MU believes X. 2. MU believes X\({}_{\text{I}}\). 3. MU believes A. 4. FA believes Y. 5. FA believes R\({}_{\text{i}}\). 6. HA believes W\({}_{\text{i}}\). 7. MU believes MU\(<\)=H(N)=>HA. 8. HA believes MU\(<\)=H(N)=>HA. 9. FA believes FA \(<\)=SK\({}_{\text{HF}}\)=>HA. 10. HA believes FA \(<\)=SK\({}_{\text{HF}}\)=>HA. 11. MU believes MU\(\leftarrow\)-SK.\(\rightarrow\)FA. 12. FA believes (MU controls MU\(\leftarrow\)-SK.\(\rightarrow\)FA). 13. HA believes (MU controls MU\(\leftarrow\)-SK.\(\rightarrow\)FA). 14. HA believes (MU controls ID\({}_{\text{MU}}\)). 15. ID\({}_{\text{MU}}\) is known only to user. 16. MU believes TCert\({}_{\text{MU}}\). 17. MU believes ID\({}_{\text{MU}}\). 18. FA believes ID\({}_{\text{FA}}\). 19. HA believes ID\({}_{\text{HA}}\). We show the processes of the proofs as follows:  
1. By \(\text{m}_{\text{V1}}\), A3, and A4, we apply the freshness rule to derive  
\[(<\)ID\({}_{\text{MU}}\)\(>\)H\({}_{\text{H}_{\text{I}}\)(X\({}_{\text{I}}\)\(\mid\) 1 \(\text{T}_{\text{MU}}\)), <X\({}_{\text{I}}\), H\({}_{\text{I}}\)(ID\({}_{\text{MU}}\)\(\mid\) 1 \(\text{N}\)\(\mid\) 1 \(\text{W}_{\text{i}}\))\(>\)H\({}_{\text{2}}\)(PW\({}_{\text{MU}}\)\(\oplus\)\({}_{\text{n}}\)), H\({}_{\text{3}}\)(W\({}_{\text{i}}\)), \(X\), ID\({}_{\text{HA}}\)). (Statement 1)By \(\rm{m}_{V1}\), A1, and A6, we apply the nonce verification rule to derive  
\[\rm{FA}\]  
believes that MU said  
\[\rm{(<ID_{MU}>_{H_{1}(X_{1}\mid\mid T_{MU})},<X_{1},H_{1}(ID_{MU}\mid\mid N\mid \mid W_{i})>_{H_{2}(PW_{MU}\oplus n_{A}),H_{3}(W_{i})},ID_{HA})}.\] (Statement 2)  
3. By \(\rm{m}_{V2}\) and A10, we apply the message meaning rule to derive  
\[\rm{HA}\]  
believes that FA said  
\[\rm{(<ID_{MU}>_{H_{1}(X_{1}\mid\mid T_{MU})},<X_{1},H_{1}(ID_{MU}\mid\mid N \mid\mid W_{i})>_{H_{2}(PW_{MU}\oplus n_{A}),H_{3}(W_{i})},W_{i},X,Y)_{[R_{i}]}}.\] (Statement 3)  
4. By \(\rm{m}_{V2}\), A1, A4, A5, and A6, we apply the nonce verification rule to derive  
\[\rm{HA}\]  
believes that FA believes  
\[\rm{(<ID_{MU}>_{H_{1}(X_{1}\mid\mid T_{MU})},<X_{1},H_{1}(ID_{MU}\mid\mid N \mid\mid W_{i})>_{H_{2}(PW_{MU}\oplus n_{A}),H_{3}(W_{i})})}.\] (Statement 4)  
5. By Statement 4, we break the conjunction to obtain  
\[\rm{HA}\]  
believes that FA believes  
\[\rm{HA}\]  
believes that FA believes  
\[\rm{HA}\]  
believes that FA believes  
\[\rm{(<ID_{MU}>_{H_{1}(X_{1}\mid\mid T_{MU})},<X_{1},H_{1}(ID_{MU}\mid\mid N \mid\mid W_{i})>_{H_{2}(PW_{MU}\oplus n_{A}),H_{3}(W_{i})}}.\] (Statement 6)  
6.