## 4 Security Analysis and Simulation Verification
### Formal Analysis of Protocol Security  
#### 4.1.1 Detailed Steps for Formal Security Analysis  
Mutual Authentication  
Rules of BAN logic are as follows:  
1. **Message meaning rule**: If the entity U believes that K is a shared key between the entities U and V, and U receives a message encrypted with K, then the entity U believes that [PERSON] has sent a message M, the formulas are as follows:\(U|\equiv U\stackrel{{ K}}{{\longleftrightarrow}}V,U\triangleleft\{M\}_{K} \mapsto U|\equiv V|\sim M\)
2. **Checking freshness rule**: If the entity U believes that the message M was sent by [PERSON] and is fresh, then the entity U believes that the entity V trusts the message M. The formulas are as follows: \(U|\equiv\#(M),U|\equiv V|\sim M\mapsto U|\equiv V|\equiv M\). 3. **Arbitration rule**: If the entity U believes that the entity V has control over the message M, and the entity U believes that [PERSON] trusts the message M, then the entity U trusts the message M. The formulas are as follows: \(U|\equiv V\Rightarrow M,U|\equiv V|\equiv M\mapsto U|\equiv M\). \begin{table}
\begin{tabular}{c c} \hline \hline
**Notation** & **Description** \\ \hline \(U|\equiv M\) & Entity \(U\) believes the statement \(M\) \\ \(U\triangleleft M\) & Entity \(U\) receives message \(M\) \\ \(U|\sim M\) & Entity \(U\) once sent message \(M\) \\ \(U\Rightarrow M\) & Entity \(U\) has control over message \(M\) \\ \(\#(M)\) & Message \(M\) is fresh \\ \((M)_{N}\) & The message is composed of \(M\) and \(N\) \\ \((M,N)\) & \(M,N\) is part of the message \((M,N)\) \\ \(\{M,N\}_{K}\) & \(M,N\) is encrypted by the key \(K\) \\ \(U\stackrel{{ K}}{{\longleftrightarrow}}V\) & \(U\) and \(V\) communicate using the key \(K\) \\ \hline \hline \end{tabular}
\end{table} 
Table 2: Some notations used in the BAN logic. **(d)**: **Fresh-connections rule**: If the entity U believes that the message M is fresh, then the entity U also believes that the message simply concatenated by M and N is also fresh. The formulas are as follows: \(U|\equiv\#(M)\mapsto U|\equiv\#(M,N)\). **(e)**: **Trust rule**: If the entity U trusts a message that is simply a concatenation of the messages M and N, then the entity U believes this message M. The formulas are as follows: \(U|\equiv(M,N)\mapsto U|\equiv M\). **(f)**: **Sending rule**: If the entity U believes that the entity V has sent a message connected by M and N, then the entity U believes that V has sent the message M. The formulas are as follows: \(U|\equiv V|\sim(M,N)\mapsto U|\equiv V|\sim M\). From the execution process of the authentication-key negotiation phase of the protocol, it can be observed that protocol entity B realizes the authentication of protocol entity A through verification \(H_{a}\). This process requires correct calculation of \(N_{a}\), because \(N_{a}\) is composed of message combinations \(r_{a},ID_{A}\). Therefore, if protocol entity B wishes to authenticate protocol entity A, it must trust the message \(r_{a},ID_{A}\). Similarly, if protocol entity A wishes to authenticate protocol entity B, it must trust the message \(r_{b},ID_{B}\). Therefore, the two-way authentication proof objectives of this protocol are as follows:  
**Goal 1**: \(B|\equiv A|\equiv\langle r_{a}\rangle_{IDA}\) (protocol entity B believes that protocol entity A trusts the message \(\langle r_{a}\rangle_{IDA}\)). **Goal 2**: \(A|\equiv B|\equiv\langle r_{b}\rangle_{IDB}\) (protocol entity B believes that protocol entity A trusts the message). **Goal 3**: \(B|\equiv\langle r_{a}\rangle_{IDA}\) (protocol entity B trusts the message \(\langle r_{a}\rangle_{IDA}\)). **Goal 4**: \(A|\equiv\langle r_{b}\rangle_{IDB}\) (protocol entity A trusts the message \(\langle r_{b}\rangle_{IDB}\)). This protocol can be formally expressed as follows:  
**Step 1**: \(A\to B:E_{yu-xa}(ID_{A})\), \(Eax\), \(Eay\), \(TS_{a}\), \(H_{a}\):  
\(\{E_{yu-xa}(ID_{A}),(\langle r_{a}\rangle_{IDA})_{yu-xa},TS_{a},H_{a}\}\).