# Provably Secure ECC-Based Anonymous Authentication and Key Agreement for IoT
## 5 Security Analysis
### Formal Proof
#### 5.1.2 Formal Security Analysis
* If \(M=(A_{j},*)\), \(\mathcal{C}\) accepts \(\prod_{i,j}^{s}\
eq\prod_{I,J}^{S}\). \(\mathcal{C}\) accepts \(\prod_{i,j}^{s}\
eq\prod_{I,J}^{S}\). \(\mathcal{C}\) looks up \((ID_{i},k_{i},PK_{i})\) in \(L_{U}\) and \(K^{\prime}_{j}\)), \(\mathcal{A}\) would have had to commit the new secret value \(k^{\prime}_{i}\) (or \(K^{\prime}_{j}\)) to \(\mathcal{C}\); since \(\mathcal{C}\) is unable to generate the session key if he does not know the secret values for \(ID_{i}\) and \(ID_{j}\). The responses of \(\mathcal{C}\) to \(Test(\prod_{i,j}^{s})\) are as follows: * If \(\prod_{i,j}^{s}\
eq\prod_{I,J}^{S},C\) fails and stops. * If \(\prod_{i,j}^{s}=\prod_{I,J}^{S}\), \(\mathcal{C}\) randomly chooses \(SSK_{i}\in Z_{q}^{*}\) and sends it back to \(\mathcal{A}\). * **Solve ECDH problems**. To win the game by forging attack, \(\mathcal{A}\) would have to calculate \(h(ID_{i}\|ID_{j}\|B_{i}\|C_{I})\), where \(B_{I}=k_{J}k_{I}u_{2}P\) and \(D_{I}=k_{J}k_{I}u_{2}v_{2}P\). \(\mathcal{C}\) finds \(k_{I}\) and \(k_{j}\) in \(L_{U}\) and computes \(B_{I}\) and \(D_{I}\) by solving the ECDH problem. * **Probability**. If it is possible for \(\mathcal{C}\) to properly guess the test session \(\prod_{i,J}^{S}\), \(\mathcal{C}\) will not fail in the query phase. Thus, \(\mathcal{C}\) is able to calculate \(B_{I}=\text{ECDH}(k_{I}P,k_{I}u_{2}P)\) and \(D_{I}=\text{ECDH}(k_{I}v_{2}P,k_{I}u_{2}P)\) with probability \(\frac{1}{n_{1}^{2}n_{2}}Adv_{AKA}(A)\) if \(\mathcal{A}\) wins in the game with advantage \(Adv_{AKA}(A)\). * **Analysis of E2** * **Setup**. Same as that in the analysis of E1. **Query. **\(\mathcal{C}\) responds to the queries from \(\mathcal{A}\) as those in the analysis of E1 except for the \(PKReveal(ID_{i})\), \(SKReveal(ID_{i})\), \(ESReval(\prod_{ij}^{n})\), and \(Send(\prod_{ij,i^{\prime}}^{n}M)\). **(1)**\(PKReveal(ID_{i})\). \(\mathcal{A}\) submits an identity \(ID_{k}\), \(\mathcal{C}\) will respond to the query as follows:  
* If \(ID_{k}=ID_{I}\), \(\mathcal{A}\) computes \(K_{I}=v_{1}P\), returns \(v_{1}P\), and adds \((ID_{J},\bot,v_{1}P)\) to the list \(L_{U}\). * If not, \(\mathcal{C}\) randomly selects \(k_{k}\in Z_{q}^{*}\) and calculates \(PK_{k}=k_{k}P\), then returns \(PK_{k}\) and adds \((ID_{k},k_{k},PK_{k})\) in \(L_{U}\). **(2)**\(SKReveal(ID_{i})\). If \(ID_{i}=ID_{J}\), \(\mathcal{C}\) will fail and stop. If not, \(\mathcal{C}\) looks up \((ID_{i},k_{i},PK_{i})\) in \(L_{U}\) and returns \(k_{i}\). **(3)**\(ESReval(\prod_{ij}^{n})\). \(\mathcal{C}\) will respond to the query as follows:  
* If \(\prod_{i,j}^{s}=\prod_{IJ}^{s}\) or \(\prod_{i,j}^{s}=\prod_{IJ}^{E}\), \(\mathcal{C}\) randomly chooses \(x_{I}\in Z_{q}^{*}\) and returns \((\bot,x_{I})\), then appends \((ID_{I},ID_{I},s,\bot,x_{I})\) to \(L_{W}\). * If not, \(\mathcal{C}\) randomly chooses \(x_{i},x_{j}\in Z_{q}^{*}\) and returns \((x_{i},x_{j})\), then appends \((ID_{i},ID_{j},s,x_{i},x_{j})\) to \(L_{W}\). **(4)**\(Send(\prod_{i,j}^{s}M)\). \(\mathcal{C}\) will respond to the query as follows:  
* If \((\prod_{i,j}^{s},M)=(\prod_{IJ,J}^{s}\bot)\), \(\mathcal{C}\) looks up \((ID_{I},k_{I},PK_{I})\) in \(L_{U}\) and returns \((k_{1}u_{2}P)\). * If \((\prod_{i,j^{\prime}}^{s},M)=(\prod_{IJ,L}^{E}\bot)\), \(\mathcal{C}\) looks up \((ID_{J},\bot,v_{1}P)\) in \(L_{U}\), and \((ID_{I},ID_{J},s,\bot,x_{I})\) in \(L_{W}\), then sends \((v_{1}x_{j}P)\) back. * Otherwise, the analysis is the same as for E1. **(3)**\(\;\)**Solve ECDH problems. ** To win the game by forging attack, \(\mathcal{C}\) must compute \(h(ID_{I}\|ID_{I}\|B_{I}\|C_{I})\), where \(B_{I}=k_{J}k_{I}u_{2}P\) and \(C_{I}=k_{I}u_{2}v_{1}x_{J}P\). \(\mathcal{C}\) finds \(k_{I}\) in the list \(L_{U}\) and \((\bot,x_{J})\) in the list \(L_{W}\) to compute \(B_{I}\) and \(C_{I}\) by solving ECDH problems. **(4)**\(\;\)**Probability. ** If it is possible for \(\mathcal{C}\) to properly guess the test session \(\prod_{IJ,J}^{s}\), \(\mathcal{C}\) will not fail in the query phase.