# Two-Level-Composite-Hashing Facilitating Highly Efficient Anonymous IoT and D2D Authentication
## 5 Security Analysis and Performance Evaluation
### The Formal Protocol Verification in AVSIPA and Security Analysis
#### 5.1.1 Security Properties Verification in AVISPA  
Our schemes consist of four main protocols--anonymous D2S authentication, S-assist-always anonymous D2S2D authentication, S-assist-once-a-while anonymous D2S2D authentication, and direct D2D anonymous authentication. In the HLPSL specification, we define three roles: \"server\" for the server, \"device1\" for the device in the D2S authentication and for the initiator in the D2S2D authentication, and \"device 2\" for the responder in the D2S2D authentication and for the responder in the direct D2D authentication. AVISPA supports the Dolev-Yao channels, where the intruder may divert sent messages and send new ones impersonating other agents. AVISPA can verify authentication and session key privacy, but it does not support verification of anonymity and unlinkability. Here, we use it to verify mutual authentication, session key privacy, and forward secrecy. Mutual authentication can be modeled using the predicate \"authentication_on\", and session key privacy can be modeled using the predicate \"secrecy_of\". To model the forward secrecy, we let each instance (server and device) run two successive sessions in their respective HLPSL specifications to have two session keys; let the intruder have the secrets of the second session, and then verify whether the intruder can derive the secret keys of the first session. The goal is to verify that, even if the intruder has the secrets of the 2 nd session, the goals of authentication and session key privacy of the 1 st session are still achieved in AVISPA verification. Basically, our HLPSL for the four protocols can be classified as two kinds: one kind is the specification of one session with the goals of \"authentication_on\" of the mutual authentication and \"secrecy_of\" of the session keys, and the other kind is the specification of two successive sessions with the security goals of the 1 st session. The main differences among the specifications of the four protocols include the different shared keys used, the number of entities in the protocols (two parties in the D2S authentication and in the direct D2D authentication, and three parties in the D2S2D authentication). Therefore, in the following, we will introduce and discuss some results, but omit similar others to keep the presentation clear and focused. Verification on the Two-Party D2S Authentication  
Figure 7 shows the protocol simulation of the D2S authentication, where \"device d-3\" and \"server s-4\" exchange messages and accomplish the authentication. Figure 8 shows the result of the OFMC verifier on the D2S authentication; the result of the OFMC on the D2S authentication is \"SAFE\"--no successful attacks can be plotted. Next, we examined the forward secrecy of the D2S authentication. Figure 9 shows the message flow, where \"device d-3\" and \"server s-4\" accomplished two runs of authentications, and the intruder knew the secrets of the 2 nd session; the result shows that OFMC verifier could not plot any successful attacks on the 1 st session. The result was \"SAFE\" in Figure 10.  
Figure 8: The result of On-the-Fly-Model-Checker (OFMC) on the D2S authentication. Figure 10: The result of OFMC on two D2S authentication sessions. Figure 9: The message sequences of two successive D2S authentications. Verification on the Three-Party S-Assist-Always D2S2D Authentication  
Figure 11 shows the message exchange of the S-assist-always D2S2D authentication, where \"device d-3\" and \"device d-5\" accomplished authentication via the help of \"server s-4\". OFMC checks \"SAFE\" on the protocol in Figure 12. The same results could be derived for the forward secrecy of the two-session cases. The specifications of the S-assist-once-a-while D2S2D authentication were similar to those of the S-assist-always D2S2D authentication, except the shared keys used are different and the identifications (pseudonym) are different.