# Provably Secure ECC-Based Anonymous Authentication and Key Agreement for IoT
## 5 Security Analysis
### Formal Proof
#### 5.1.2 Formal Security Analysis  
At first, three empty lists are created to hold the query and the corresponding answers. \(L\): input-output pairs of the hash function. Instead of being randomly chosen by \(\mathcal{C}\), the real hash function computes the outputs. To complete the safety proof, \(\mathcal{C}\) needs to record the mapping between the inputs and outputs. \(L_{U}\): Tuple \((ID_{i},k_{i},PK_{i})\) for storing the queries-answers of \(PKReveal(ID_{i})\), \(PKReplace(ID_{i})\), and \(SKR Reveal(ID_{i})\). \(L_{w}\): Tuple \((ID_{i},ID_{j},s,x_{i},x_{j})\) for storing the queries-answers of \(ESReveal(\prod_{i,j}^{s})\). To continue, it is essential to clarify a few fundamental configurations. Suppose that \(\mathcal{A}\) is activating no more than \(n_{1}\) honest parties, and each party is engaged in no more than sessions. Assume that \(\mathcal{A}\) selects the \(\prod_{I,J}^{S}\) as the test session. \(\mathcal{A}\) can distinguish a test session key from a random string in the three ways below:  
**A1. Guessing. **\(\mathcal{A}\) guesses the session key correctly. **A2. Key replication. **\(\mathcal{A}\) creates a mismatched session that has the same session key as \(\prod_{I,J}^{S}\). So \(\mathcal{A}\) is able to fetch the session key by querying the mismatched session. **A3. Forging. ** The value of \(h(ID_{i}\|ID_{j}\|B_{i}\|C_{i})\) is computed at some point by \(\mathcal{A}\). Theorem 1: _Since the ECDL or ECDL problem is intractable, the advantage of \(\mathcal{A}\) against the AKA scheme in the eCK model is negligible._  
Proof: Since the session key \(SSK_{i}\in Z_{q}^{*}\), there is only a \(\frac{1}{q-1}\) chance of guessing the correct \(SSK_{i}\) in the **guessing** attack. The hash function should yield the same results for different input values in order to prevent the **key replication** attack. The probability of success of a **key duplication** attack is negligible. The analysis of the **forging attack** is shown below. Consider the tuple \((P,u_{1}P,u_{1}u_{2}P,v_{1}P,v_{1}v_{2}P)\) as an example of the ECDL problem, in which the ephemeral keys \(x_{s}\) and \(x_{sp}\) are denoted by \(u_{2}\) and \(v_{2}\), and the long-term keys \(k_{s}\) and \(k_{sp}\) are represented by \(u_{1}\) and \(v_{1}\). If \(\mathcal{A}\) is successful in **forging attack** with non-negligible probability, ECDH\((u_{1}u_{2}P,v_{1}P)=u_{1}u_{2}v_{1}v_{1}P\) and ECDH\((u_{1}u_{2}P,v_{1}v_{2}P)=u_{1}u_{2}v_{1}v_{1}P\) can be computed by \(\mathcal{C}\) using \(\mathcal{A}\). First, \(\mathcal{C}\) creates a test session \(\prod_{I,J}^{S}\) by randomly selecting \(S\in\{1,n_{2}\}\) and \(I,J\in\{1,n_{1}\}(I\
eq I)\). Therefore, \(\mathcal{C}\) has no higher chance of correctly guessing the test session \(\prod_{I,J}^{S}\) than \(\frac{1}{n_{1}^{2}-n_{2}}\). Let \(\prod_{J,I}^{E}\) be the matching session of \(\prod_{IJ}^{S}\). There are six complementary events to consider as shown in Table 2. E1: \(\mathcal{A}\) does not obtain the ephemeral secret keys of \(ID_{I}(u_{2})\) and \(ID_{J}(v_{2})\). E2: \(\mathcal{A}\) does not obtain the ephemeral secret key of \(ID_{I}(u_{2})\) and secret value of \(ID_{I}(v_{1})\). E3: \(\mathcal{A}\) does not obtain the ephemeral secret keys \(ID_{J}(v_{2})\) and secret value of \(ID_{I}(u_{1})\). E4: \(\mathcal{A}\) does not obtain the secret values of \(ID_{I}(u_{1})\) and \(ID_{I}(v_{1})\). E5: There is no matching session for \(\prod_{J,J}^{S}\). \(\mathcal{A}\) obtains parameters similar to E2. E6: There is no matching session for \(\prod_{I,J}^{S}\). \(\mathcal{A}\) obtains parameters similar to E4. At least one event in the set, \(\{E1\wedge A3,E2\wedge A3,E3\wedge A3,E4\wedge A3,E5\wedge A3,E6\wedge A3\}\), happens with non-negligible probability if \(\mathcal{A}\) succeeds in faking attack with non-negligible probability. 1. **Analysis of E1** **(1) Setup. **\(\mathcal{C}\) sends \((E(a,b),p,q,P,P,h(\cdot))\) to the \(\mathcal{A}\). 2. **Query.