## 4 Security Analysis and Simulation Verification
### Formal Analysis of Protocol Security
#### 4.1.1 Detailed Steps for Formal Security Analysis
**Step 2**: \(B\to A:E_{yb-xb}(ID_{B})\), \(Ebx\), \(Eby\), \(TS_{b}\), \(H_{b}\):  
\(\{E_{yb-xb}(ID_{B}),(\langle r_{b}\rangle_{IDB})_{yb-xb},TS_{b},H_{b}\}\). The following basic assumptions are made for the authentication scheme of the protocol:  
**Assumption 1**. : \(B|\equiv\#(\langle r_{a}\rangle_{IDA})\) _(protocol entity B believes in the freshness of the message \(\langle r_{a}\rangle_{IDA}\))._  
**Assumption 2**. : \(A|\equiv\#(\langle r_{b}\rangle_{IDB})\) _(protocol entity A believes in the freshness of the message \(\langle r_{b}\rangle_{IDB}\))._  
**Assumption 3**. : \(B|\equiv B\stackrel{{ H(ID_{A}||ID_{B})}}{{\longleftrightarrow}}A\) _(protocol entity B believes that the key \(H(ID_{A}||ID_{B})\) is shared by \(A\) and \(B\) (note: according to the definition of the protocol registration phase, \(y_{a}-x_{a}=y_{b}-x_{b}=H(ID_{A}||ID_{B})\))._  
**Assumption 4**. : \(A|\equiv A\stackrel{{ H(ID_{A}||ID_{B})}}{{\longleftrightarrow}}B\) _(protocol entity A believes that the key \(H(ID_{A}||ID_{B})\) is shared by \(A\) and \(B\))._  
**Assumption 5**. : \(B|\equiv A\Rightarrow\langle r_{a}\rangle_{IDA}\) _(protocol entity B believes that A has control over the message \(\langle r_{a}\rangle_{IDA}\))._  
**Assumption 6**. : \(A|\equiv B\Rightarrow\langle r_{b}\rangle_{IDB}\) _(protocol entity A believes that B has control over the message \(\langle r_{b}\rangle_{IDB}\))._  
Combined with step 1, we obtain conclusion 1:  
**Conclusion 1**: \(B\triangleleft E_{yu-xa}(ID_{A})\)_, \(Eax\), \(Eay\), \(TS_{a}\), \(H_{a}\):\(\{E_{ya-xa}(ID_{A}),(\langle r_{a}\rangle_{IDA})_{yu-xa},TS_{a},H_{a}\}\). The combination of conclusion 1, assumption 3, and the rule of the meaning of the message results in conclusion 2:  
**Conclusion 2**: \(B|\equiv A|\sim\{E_{yu-xa}(ID_{A}),(\langle r_{a}\rangle_{IDA})_{yu-xa}\,TS_{a},H_{a}\}\). Combining conclusion 2 and the transmission rules, we obtain conclusion 3:  
**Conclusion 3**: \(B|\equiv A\sim\langle r_{a}\rangle_{IDA}\). Combining conclusion 3, assumption 1, and the freshness-checking rule results in conclusion 4:  
**Conclusion 4**: \(B|\equiv A|\equiv\langle r_{a}\rangle_{IDA}\). **(Goal 1 achieved)**. By combining conclusion 4, assumption 5, and the arbitration rule, we obtain conclusion 5:  
**Conclusion 5**: \(B|\equiv\langle r_{a}\rangle_{IDA}\)**(Goal 3 achieved)**. Combined with step 2, we obtain conclusion 6:  
**Conclusion 6**: \(A\trianglelefteq E_{yb-xb}(ID_{B})\), \(Ebx\), \(Eby\), \(TS_{b}\), \(H_{b}\):  
\(\{E_{yb-xb}(ID_{B}),(\langle r_{a}\rangle_{IDB})_{yb-xb},TS_{b},H_{b}\}\). The combination of conclusion 6, assumption 4, and the message-meaning rule yields conclusion 7. **Conclusion 7**: \(A|\equiv B|\sim\{E_{yb-xb}(ID_{B}),(\langle r_{b}\rangle_{IDB})_{yb-xb},TS_{b},H_{b}\}\). Combining conclusion 7 and the transfer rules, we obtain conclusion 8:  
**Conclusion 8**: \(A|\equiv B\sim\langle r_{b}\rangle_{IDB}\). By combining conclusion 8 and assumption 2, and the checking of freshness rule, we obtain conclusion 9:  
**Conclusion 9**: \(A|\equiv B|\equiv\langle r_{b}\rangle_{IDB}\)**(Goal 2 achieved)**. The combination of conclusion 9, assumption 6, and the arbitration rule yields conclusion 10:  
**Conclusion 10**: \(A|\equiv B|\equiv\langle r_{b}\rangle_{IDB}\). **(Goal 4 achieved)**. In summary, the proposed protocol can achieve secure mutual two-way authentication. Anti-Attack Against Known Session-Specific Temporary Information  
The security of the session key is not compromised if session-specific temporary information is leaked. Before formally analyzing the protocol against attacks on known session-specific temporary information, the following definition is introduced:  
**Definition 1**. : _Let \(H(. )\) denote a one-way hash function, be the input value of the one-way hash function, and be the output value of the one-way hash function. We use Event1 to represent the event: known \(b=H(a)\), unconditional output \(a\)._  
**Definition 2**.