# Secure and Efficient Authentication Scheme in IoT Environments
## 4 Cryptoanalysis of the Proposed Protocol
### Formal Security Validation Using the AVISPA Tool
The last three roles represent the execution environment of the first two roles. Figure 4 depicts the specific role performed by the agent. Upon receiving the start signal, the device \(U\) (i.e., _ED\({}_{i}\)_) updates its state from 0 to 1. This state is expressed (_Pass1\({}^{\prime}\)_, _G4\({}^{\prime}\)_) > (i.e., _<\(l_{i}\)_, _P\({}_{k}\)_> ) securely to the server through a secure channel (_SND_); we call this the registration phase. The transmission channel _< SND_, _RCV_ >, which is an unreliable channel, is used for the message transmission of the Dolev-Yao-type threat model; it enables an attacker to modify or delete the contents of transmitted messages. Afterward, in response, \(U\) receives the message _<Cid\({}^{\prime}\)_, _CK\({}^{\prime}\)_> (i.e., _<CID\({}_{i}\)_, _CK\({}^{\prime}\)_> ) from the server securely with the help of the secure RCV channel. During thelogin phase, \(U\) sends a message \(<\)_Cid\({}^{\prime}\)_, \(P1^{\prime}\)_, \(P2^{\prime}\)_ > (i.e., \(<\)_CID\({}_{i}\)_, \(X_{i}\)_, \(Y_{i}\)_>) to the server via the public open channel (see Figure 5). Figure 4: Role specification for IoT devices. Figure 5: Role specification for server. Subsequently, the server responds with a message \(<\)T\({}^{\prime}\), \(P3^{\prime}\), \(P4^{\prime}\)\(>\) (i.e., \(<\)T, \(X_{j}\), \(Y_{j}\)\(>\)) to \(U\) via the public open channel. Finally, \(ED_{i}\) replies with the message \(<\)Vi\(>\) (i.e., \(<\)C \(>\) ) to the server via the public open channel. A knowledge declaration situated at the top of each role is used to specify the initial knowledge of the intruder. The immediate-reaction transition is of the form \(X=|>Y\), which relates an event \(X\) to an action \(Y\). The declaration witness \(<\)\(U\), \(S\), \(seq2\), \(Cid^{\prime}\). \(P1^{\prime}\).\(P2^{\prime}\)\(>\) is generated by \(U\), where the \(seq2\) indicates the message sequence (i.e., message \(<\)_alice_bob_Cid\({}^{\prime}\).\(P1^{\prime}\).\(P2^{\prime}\)\(>\)_ from [PERSON] to [PERSON]) and \(<\)\(P1^{\prime}\), \(P2^{\prime}\)\(>\) is freshly generated for the server (S). Subsequently, again, another declaration request \(<\)\(S\), \(U\), \(seq5\), \(T^{\prime}\).\(P3^{\prime}\).\(P4^{\prime}\)\(>\) shows \(U\)\(S\) acceptance of the random nonce \(<\)\(P3^{\prime}\),\(P4^{\prime}\)\(>\) generated for \(ED_{i}\) by the server, where seq5 indicates the message sequence (i.e., message \(<\)_bob_alice_T\({}^{\prime}\).\(P3^{\prime}\).\(P4^{\prime}\)\(>\) from [PERSON] to [PERSON]). Similarly, we executed the role of the server during the registration phase. Finally, as depicted in Figure 6, we implemented the role of the session, goal, and environment of the proposed scheme. All these roles are the instances with solid arguments in the role session. In the HLPSL protocol, the intruder (i) is likewise interested in the execution of protocol in a concrete session. Furthermore, we defined many secret goals and nine authentication goals. For example, the secret goal (secrecy_of_k1) indicates that \(ID_{i}\) and \(Psw_{i}\) are kept secret from the device \(U\) only. The authentication goal: authentication on seq2 (i.e., authentication_on alice_bob_Cid\({}^{\prime}\).\(P1^{\prime}\).\(P2^{\prime}\)) means that \(U\) generates \(<\)\(Cid^{\prime}\).\(P1^{\prime}\).\(P2^{\prime}\)\(>\), where secret \(N1^{\prime}\) hidden inside \(<\)\(P1^{\prime}\),\(P2^{\prime}\)\(>\) is only known to \(U\). When the server receives \(<\)\(Cid^{\prime}\).\(P1^{\prime}\).\(P2^{\prime}\)\(>\) from other messages from the same \(U\), the server performs a strong authentication for the devices based on \(<\)\(P1^{\prime}\),\(P2^{\prime}\)\(>\). For analyzing the protocol, we selected widely accepted CL-AtSe and OFMC backend for the execution tests. Both CL-AtSe and OFMC backends analyze whether the legal agents can execute the specific scheme by searching for the passive intruder. Subsequently, backend results provide the intruders with the knowledge of some typical sessions among the legitimate agents.