# Provably Secure ECC-Based Anonymous Authentication and Key Agreement for IoT
## 5 Security Analysis
### Formal Proof
#### 5.1.1 Security Model  
**Participants**. There are \(n\) participants in the proposed protocol \(\mathbb{P}\), which are uniformly denoted by the set \(F=\{F_{1},\ldots,F_{n}\}\), and each participant may have \(i\) instances involved in distinct, possibly concurrent executions of \(\mathbb{P}\), where \(n\) and \(i\) are polynomial numbers. **Sessions**. Let \(\prod_{i,j}^{m}\) denote the \(m\)th protocol session running between entity \(F_{i}\) and intended partner entity \(F_{j}\). A session \(\prod_{i,j}^{m}\) is _accepted_ if it has computed a session key \(SK_{i,j}^{m}\)  
Figure 4: Authentication model. Figure 3: Authentication and key agreement of proposed protocol. with a session identifier of \(sid_{i,j}^{m}=(ID_{i},ID_{j},X_{i},X_{j})\), where \(X_{i}\) is the outgoing information of \(F_{i}\), and \(X_{j}\) is the outgoing information of \(F_{j}\). **Adversary**. Firstly, the adversary \(\mathcal{A}\) has complete control of the communicating network. Namely, \(\mathcal{A}\) is able to eavesdrop on, alter, ascertain, and inject communication messages \(M_{s}\) and \(M_{sp}\). Secondly, \(\mathcal{A}\) can have knowledge of the participant's long-term private key \(k_{s}\) (\(k_{sp}\)) and ephemeral secret \(x_{s}\) (\(x_{sp}\)) but not both. Thirdly, \(\mathcal{A}\) allows replacing the participant's public key \(PK_{s}\) (\(PK_{sp}\)). Finally, \(\mathcal{A}\) can obtain the session key \(SSK_{s}\) (\(SSK_{sp}\)) held by the participant. \(\mathcal{A}\) can interact with \(\prod_{i,j}^{m}\) with the following Oracle queries:  
(1) \(ESReveal(\prod_{i,j}^{m})\). \(\mathcal{A}\) can obtain the ephemeral secrets of \(F_{i}\) with the query. (2) \(PKReplace(ID_{i})\). \(\mathcal{A}\) replaces the public key of \(F_{i}\) using this query. (3) \(PKReveal(ID_{i})\). \(\mathcal{A}\) is available with this query for the public key of \(F_{i}\). (4) \(SKReveal(ID_{i})\). By running the query, \(\mathcal{A}\) is able to obtain the long-term private keys of \(F_{i}\), while the public key of \(F_{i}\) has not yet been replaced. (5) \(SSKReveal(\prod_{i,j}^{m})\). Returns \(\bot\) if session \(\prod_{i,j}^{m}\) was not _accepted_. If not, it returns the session key that \(\prod_{i,j}^{m}\) holds. (6) \(Send(\prod_{i,j}^{m}M)\). \(\mathcal{A}\) represents \(F_{i}\) sending the message \(M\) to \(F_{i}\) in session \(\prod_{i,j}^{m}\) then receiving a reply from \(F_{i}\) according to \(\mathbb{P}\). (7) \(Test(\prod_{i,j}^{m})\). The query does not simulate the adversary's ability, but it simulates the indistinguishability between real session keys and random keys. Input session \(\prod_{i,j}^{m}\) must be fresh. As a challenger, \(\mathcal{C}\) tosses a coin \(b\in\{0,1\}\). If \(b=0\), \(\mathcal{C}\) returns the session key held by \(\prod_{i,j}^{m}\); if \(b=1\), \(\mathcal{C}\) returns a random key from the distribution of the session key. **Matching session**. If \(\prod_{i,j}^{m}\) and \(\prod_{j,i}^{m}\) have the same session \(sid\), then \(\prod_{j,i}^{m}\) is said to be a matching session for \(\prod_{i,j}^{m}\). **Freshness**. Let \(\prod_{i,j}^{m}\) denote an _accepted_ session between honest participants \(F_{i}\) and \(F_{j}\) if \(\prod_{i,j}^{m}\) and \(\prod_{i,j}^{m}\) are matching sessions. \(\prod_{i,j}^{m}\) is fresh if all the following conditions do not hold:  
(1) \(\mathcal{A}\) issues \(SSKReveal(\prod_{i,j}^{m})\) or \(SSKReveal(\prod_{j,i}^{m})\) queries if \(\prod_{j,i}^{m}\) exists. (2) The matching session \(\prod_{i,j}^{m}\) exists. \(\mathcal{A}\) makes \(SKR reveal(ID_{i})\) and \(ESReveal(\prod_{i,j}^{m})\) queries, or \(SKR reveal(ID_{j})\) and \(ESReveal(\prod_{j,i}^{m})\) queries. (3) The matching session \(\prod_{i,j}^{m}\) does not exist. \(\mathcal{A}\) makes \(SKR Reveal(ID_{i})\) and \(ESReveal(\prod_{i,j}^{m})\), or \(SKR Reveal(ID_{j})\) queries. A game simulates the security of an AKA protocol. In the game, \(\mathcal{A}\) can issue multiple queries in any order.