## 5 Security Analysis
### Formal Security Proof
#### 5.1.2 Security Proof  
**Theorem 1**. : _Let \(Adv_{\mathcal{P},\mathcal{D}}^{AKA}(\mathcal{A})\) denote the advantage of a PPT adversary \(\mathcal{A}\) in compromising the semantic security of \(\mathcal{P}\) within a limited time \(t\). Given that \(\mathcal{A}\) makes \(q_{h}\) hash queries, \(q_{e}\) execute queries, and \(q_{s}\) send queries, we have:_  
\[Adv_{\mathcal{P},\mathcal{D}}^{AKA}(\mathcal{A})\leq 2C^{\prime}\cdot q_{s}^{s \prime}+\Delta\]  
_where \(\Delta=\frac{\left(q_{i}+q_{h}+q_{h}^{2}\right)}{2^{l-1}}+\frac{2\left(q_{i}+q _{e}\right)^{2}}{p}+2q_{h}Adv_{\mathcal{A}}^{ECCH}(t^{\prime})\), where \(\mathcal{D}\) represents the password space that follows [PERSON]'s law [34] based on a probability distribution. The parameters \(s^{\prime}\) and \(C^{\prime}\) are related to [PERSON]'s law, \(1\) denotes the bit length of the hash value, \(p\) is a large prime number, and \(t^{\prime}\leq t+(q_{s}+q_{e}+1)T_{c}\), where \(T_{c}\) is the time required for an ECC point multiplication operation._  
Proof. : The detailed proof involves a sequence of games from \(Game_{0}\) to \(Game_{5}\). Let \(Pr[E_{i}]\) represent the probability that \(\mathcal{A}\) successfully guesses \(b\) in the test-query of \(Game_{i}\), for \(i=0,\ 1,\ 2,\ 3,\ 4,\ 5\). Game \(E_{0}\). This game simulates a real attack in the context of a random oracle. At the start, a bit \(b\) is chosen, thus:  
\[Adv_{\mathcal{P},\mathcal{D}}^{AKA}(\mathcal{A})=|2 Pr[E_{0}]-1|\]  
Game \(E_{1}\). This game models the random oracle \(H\) and a hash list \(\Lambda_{\mathcal{H}}\). Furthermore, this game is indistinguishable from the actual execution of the protocol, i.e., game \(E_{0}\), as all oracles simulate a real attack. Thus, we have:  
\[|Pr[E_{1}]-Pr[E_{0}]|=0\]  
Game \(E_{2}\). This game, like game \(E_{1}\), models all types of queries and terminates under two conditions [35]: (1) a crash from the hash query output and (2) a crash from various records \(((M_{2},K_{1},K_{2},t_{u}),(K_{3},M_{3}))\). According to the birthday paradox, we have:  
\[|Pr[E_{2}]-Pr[E_{1}]|\leq\frac{q_{h}^{2}}{2^{l+1}}+\frac{(q_{s}+q_{e})^{2}}{2p}\]  
Game \(E_{3}\). This game is modeled similarly to game \(E_{2}\), but the protocol is aborted if A correctly guesses the authentication parameter \(M_{3}\) without querying the random oracle. Additionally, this game is difficult to distinguish from game \(E_{2}\) unless the correct authentication parameter is rejected by \(U^{i}\) or \(S^{j}\). Hence, we have:  
\[|Pr[E_{3}]-Pr[E_{2}]|\leq\frac{q_{s}}{2^{l}}\]  
Game \(E_{4}\). In this game, the session key \(SK\) is obtained without initiating the corresponding random oracle query. Similarly, this game is hard to distinguish from game unless \(\mathcal{A}\) queries the random oracle \(\mathcal{H}\) on \(\big{(}K\|ID_{i}^{*}\|V_{i}^{*}\big{)}\), where \(K=ECCDH(K_{1},K_{3})=abP\)[35]. Therefore, we have:  
\[|Pr[E_{4}]-Pr[E_{3}]|\leq q_{h}Adv_{\mathcal{A}}^{ECCDH}\big{(}t^{\prime}\big{)}+ \frac{q_{h}}{2^{l}}\]  
Game \(E_{5}\). This game is similar to game \(E_{4}\), with the additional execution of the test query. If \(\mathcal{A}\) initiates a hash \(\mathcal{H}\) query with \(\big{(}abP\|ID_{i}^{*}\|V_{i}^{*}\big{)}\), game \(E_{5}\) is aborted. Accordingly, \(SK\) can be obtained by \(\mathcal{A}\) initiating the \(\mathcal{H}\) query with a probability of \(\frac{q_{h}^{2}}{2^{l+1}}\). Alternatively, through a smart-card-loss attack and a corrupt \(U^{i}\) oracle, \(\mathcal{A}\) can try to get \(U^{i}\)'s password and compromise the session key. Using \"fuzzy verifier + honeywords\", \(\mathcal{A}^{\prime}\)s chance of guessing the password correctly is no more than \(C^{\prime}\cdot q_{\mathrm{s}}^{s\prime}\)[24]. To break forward security and obtain the session key, the chance of obtaining \(abP\) is at most \(\frac{(q_{g}+q_{\epsilon})^{2}}{2p}\).