# Provably Secure ECC-Based Anonymous Authentication and Key Agreement for IoT
## 5 Security Analysis
### Formal Proof
#### 5.1.2 Formal Security Analysis
**\(\mathcal{A}\) will query the public key before an identity is used in any other queries, and all queries are different. \(\mathcal{C}\) answers the queries issued by \(\mathcal{A}\) as follows: **(1)**: \(PKReveal(ID_{i})\). \(\mathcal{A}\) submits an identity \(ID_{i}\), \(\mathcal{C}\) picks at random \(k_{i}\in Z_{q}^{*}\), computes \(PK_{i}=k_{i}\cdot P\), then returns \(PK_{i}\) and adds \((ID_{i},k_{i},PK_{i})\) to the list \(L_{U}\). \begin{table}
\begin{tabular}{l c c c c c} \hline \hline  & \(E1\) & \(E2\) & \(E3\) & \(E4\) & \(E5\) & \(E6\) \\ \hline \(\prod_{I,I}^{E}\) & & & & & \(\times\) & \(\times\) \\ \hline Ephemeral secret keys of \(ID_{I}(u_{2})\) & \(\times\) & \(\times\) & & & \(\times\) & \\ \hline Ephemeral secret keys of \(ID_{I}(v_{2})\) & \(\times\) & & \(\times\) & & & \\ \hline Secret value of \(ID_{I}(u_{1})\) & & & \(\times\) & \(\times\) & & \(\times\) \\ \hline Secret value of \(ID_{I}(v_{1})\) & & \(\times\) & & \(\times\) & \(\times\) & \(\times\) \\ \hline \hline \end{tabular} \(\times\): the session does not exit or \(\mathcal{A}\) does not obtain the parameter.  
\end{table} 
Table 2: Complementary events. \(\mathcal{A}\) submits a tuple \(PK^{\prime}_{i}=k^{\prime}_{i}\cdot P\) for \(ID_{i}\), \(\mathcal{C}\) replaces \(PK_{i}\) with \(PK^{\prime}_{i}\), and update \((ID_{i},k_{i},PK_{i})\) with \((ID_{i},*,K^{\prime}_{i})\) in the list \(L_{U}\), where \(*\) can be the secret value \(k^{\prime}_{i}\) or be the symbol \(\bot\). \(SK Reveal(ID_{i})\). \(\mathcal{A}\) submits an identity \(ID_{i}\), \(\mathcal{C}\) looks up \((ID_{i},k_{i},PK_{i})\) in the list \(L_{U}\) and returns \(k_{i}\). If \(\mathcal{A}\) has replaced the public key \(PK_{i}\) and has not submitted a new one, \(\mathcal{C}\) will refuse to respond. \(ESReval(\prod_{i,j}^{m})\). \(\mathcal{A}\) submits a session \(\prod_{i,j}^{s}\), then \(\mathcal{C}\) processes as follows: * If \(\prod_{i,j}^{s}=\prod_{I,J}^{S}\) or \(\prod_{i,j}^{s}=\prod_{I,I}^{E}\), then \(\mathcal{C}\) fails and stops. * If not, \(\mathcal{C}\) selects \(x_{i},x_{j}\in Z_{q}^{*}\) at random and appends \((ID_{i},ID_{j},s,x_{i},\)\(x_{j})\) to \(L_{W}\). \(SSKReval(\prod_{i,j}^{m})\). \(\mathcal{A}\) submits a session \(\prod_{i,j}^{s}\), and \(\mathcal{C}\) processes as follows: If \(\mathcal{A}\) has replaced the public key \(PK_{i}\) (or \(PK_{j}\) ) and did not submit the new secret value \(PK^{\prime}_{i}\) (or \(PK^{\prime}_{j}\) ), then \(\mathcal{C}\) may refuse to reply, else \(Case\) 1: If \(\prod_{i,j}^{s}=\prod_{I,J}^{S}\) or \(\prod_{i,j}^{s}=\prod_{I,I}^{E}\), then \(\mathcal{C}\) fails and stops. \(Case\) 2 : If \(\mathcal{A}\) has made \(ESReval(\prod_{i,j}^{m})\) for \(\prod_{i,j}^{s},C\) will look up \((ID_{i},ID_{j},s,x_{i},x_{j})\) in \(L_{W}\), \((ID_{i},k_{i},PK_{i})\), or \((ID_{j},k_{j},PK_{j})\) in \(L_{U}\), then figures out the session key according to the AKA scheme. \(Case\) 3 : Else, \(\mathcal{C}\) selects \(x_{i},x_{j}\in Z_{q}^{*}\) at random and appends \((ID_{i},ID_{j},\)\(s,x_{i},x_{j})\) to \(L_{W}\), then proceeds as in case 2. \(\mathcal{Send}(\prod_{i,j}^{s},M)\). \(\mathcal{C}\) will answer the query as below. * If \((\prod_{i,j}^{s},M)=(\prod_{I,J}^{S},\bot)\), \(\mathcal{C}\) looks up \((ID_{I},k_{I},PK_{I})\) in \(L_{U}\) and then returns \(k_{I}u_{2}P\). * If \((\prod_{i,j}^{s},M)=(\prod_{I,J}^{E},\bot)\), \(\mathcal{C}\) looks up \((ID_{J},k_{J},PK_{I})\) in \(L_{U}\) and then returns \(k_{I}v_{2}P\). * If \(\prod_{i,j}^{s}\
eq\prod_{I,J}^{S}\) and \(\prod_{i,j}^{s}\
eq\prod_{I,I}^{E}\), \(\mathcal{C}\) looks up \((ID_{i},k_{i},PK_{i})\) in \(L_{U}\) and processes as follows: * If \(\mathcal{A}\) has made \(ESReval(\prod_{i,j}^{m})\) for \(\prod_{i,j}^{s}\), \(\mathcal{C}\) looks up \((ID_{i},ID_{j},s,\)\(x_{i},x_{j})\) in \(L_{W}\), then computes and returns \(A_{i}\). * If not, \(\mathcal{C}\) randomly selects \(x_{i},x_{j}\in Z_{q}^{*}\) and calculates and returns \(A_{i}\), then appends \((ID_{i},ID_{j},s,x_{i},x_{j})\) to \(L_{W}\).