## 4 Security Analysis and Simulation Verification
### Formal Analysis of Protocol Security
#### 4.1.1 Detailed Steps for Formal Security Analysis
: _Let \(E(a,b)\) be the elliptic curve with initial parameters \(a,b\), \(P\) be the base point on the elliptic curve, and \(k\) be the scalar that is used for scalar multiplication of the elliptic curve. We use Event2 to represent the event: known \(P,R=k\cdot P\), unconditional output \(k\)._  
**Definition 3**. : _Set \(E_{sk}(. )\) as the symmetric encryption operation. \(a\) is the input value of the symmetric encryption operation and \(b\) is the output value of the symmetric encryption operation. Use Event3 to represent the event: known \(b=E_{sk}(a)\), unconditional output \(a\)._  
**Definition 4**. : _Set \(k\) as the long-term key of the protocol entity. We use Event4 to represent the event: unconditional output \(k\)._  
**Definition 5**. : _Let Event5 represent the attacker successfully capturing the temporary state of the session between protocol entities and obtaining the temporary information of the session._We analyze the probability of occurrence of \(Event1\), \(Event2\), \(Event3\), \(Event4\), \(Event5\):  
Let \(Adc_{\text{C}}^{H}(t_{1})\) be the probability that \(Event1\) occurs at least once in polynomial time \(t_{1}\). According to the irreversible property of the one-way hash function, \(Adc_{\text{C}}^{H}(t_{1})\leq\varepsilon_{1}\), where \(\varepsilon_{1}\) is a real number with a negligible size. Let \(Adc_{\text{C}}^{ECDLP}(t_{2})\) be the probability that \(Event2\) occurs at least once in polynomial time \(t_{2}\). From the problem of the discrete logarithm of the elliptic curve, we obtain \(Adc_{\text{C}}^{ECDLP}(t_{2})\leq\varepsilon_{2}\), where \(\varepsilon_{2}\) is a real number with a negligible size. Let \(Adc_{\text{E}}^{H}(t_{3})\) be the probability that \(Event3\) occurs at least once in polynomial time \(t_{3}\). It follows that \(Adc_{\text{C}}^{E}(t_{3})\leq\varepsilon_{3}\), where \(\varepsilon_{3}\approx 1/2^{len(sk)}\) (\(len(sk)\) denotes the value of the key length); \(\varepsilon_{3}\) is a real number whose size can be ignored if the key length is greater than 128 bits. Let \(Adc_{K}^{H}(t_{4})\) be the probability that \(Event4\) occurs at least once in polynomial time \(t_{4}\). From this, it follows that if \(\varepsilon_{4}\approx 1/2^{len(k)}\) (\(len(k)\) represents the value of the key length), \(\varepsilon_{4}\) is a real number whose size can be ignored if the long-term key length is greater than 128 bits. Let \(Adc_{\text{C}}^{SR}(t_{5})\) be the probability that \(Event5\) occurs at least once in polynomial time \(t_{5}\). When analyzing the proposed protocol against attacks on known session-specific temporary information, it is assumed that the temporary session information of the two protocol units is leaked to the attacker, that is, \(Adc_{\text{C}}^{SR}(t_{5})=1\). Let \(Event6\) represent the following event: Attack C successfully implements a known session-specific temporary information attack on the proposed protocol. If attacker C successfully implements a known session-specific temporary information attack, the possible attack implementation paths are as follows:  
1. \(Event5\) occurs and the temporary session information \(r_{a}\) is obtained. 2. Retrieve messages transmitted through the public channel:\(E_{ya-xa}(ID_{A}),Eax,Eay,\)\(Ha,TS_{a}\). 3. \(Event4\) occurs; obtain \(H(ID_{A}||ID_{B})\) and decrypt the message to obtain \(N_{a},ID_{A}\). 4. Determine the message transmitted through the public channel: \(E_{yb-xb}(ID_{B}),Ebx,\)\(Eby,Hb,TS_{b}\). 5. Decrypt the message to obtain \(N_{b},ID_{B}\). 6. The session key is obtained by calculation: \(SSK_{AB}=H(r_{a}\cdot ID_{A}\cdot N_{b})\). As \(Event4\) and \(Event5\) are independent of one another, \(Event4\) and \(Event5\) occur at least once when \(Event6\) occurs. If \(Adc_{\text{C}}^{SSK}(t_{6})\) represents the probability that \(Event6\) occurs at least once in polynomial time \(t_{6}\), we obtain \(Adc_{\text{C}}^{SSK}(t_{6})\leq\varepsilon_{4}\cdot 1\).