# 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.2 Security Properties Analysis  
In this section, we analyzed the security properties of the proposed schemes. Table 2 summarizes all the security properties. Figure 11: The message exchange of the S-assist-always D2S2D authentication. Figure 12: OFMC checks the security of the S-assist-always D2S2D authentication. Mutual authentication between the initiator and the responder: Mutual authentication between a device and a server in the D2S anonymous authentication; mutual authentication between the two devices in the S-assist-always D2S2D authentication, in the S-assist-once-a-while D2S2D authentication, and in the direct D2D authentication. From the protocol descriptions, we could see that the initiator \(D_{i}\) always updates its pseudonym \(PN\) in each session. This random and fresh \(PN\) simultaneously functions as a pseudonym and as a random challenge to the responders. In all the protocols, the responders (\(S\) in the D2S anonymous authentication and \(D_{\overline{i}}\) in the other protocols) all need to send their responses, which are based on the secret key and the fresh challenge \(PN\). Likewise, the responders also send its own random challenges \(Y\) to the initiators (\(D_{i}\)), which are required to send their responses accordingly. These are the classic challenge-response mechanisms. As long as the secret keys are secure and the challenges are random and fresh, this ensures the mutual authentication between the initiator and the responder. Authentication of the server to the initiator in the S-assist-assist-once-a-while D2S2D authentication, the aliquots (\(D_{i}\)) sends \(PN\) as a pseudonym and as a fresh challenge on which the server should generate a proper response, using the secret key and the challenge. This ensures the authentication of the server to the initiator. We also note here that our schemes do not provide the authentication of the initiator to the server, as the server does not send any challenge to the initiator to respond. Fortunately, this does not compromise the security between the initiator and the responder. Anonymity of the devices: In all the proposed protocols, the communicating devices always use the updated pseudonyms in the transmissions. This ensures the anonymity. Unlinkability among devices' successful connections: In all the proposed protocols, the initiator \(D_{i}\) always generates its pseudonym as \(PN=h_{2}(N_{i})\) and updates its seed \(N_{i}=h_{1}(N_{i})\), where \(h_{1}\) and \(h_{2}\) are two independent one-way hashing functions. The preimage resistance property of the one-way hashes ensures the unlinkability of the initiator. Regarding the responder \(D_{\overline{i}}\)'s pseudonyms, the server finds \(D_{i}^{\prime}\)'s current pseudonym \(PN_{\overline{i},\overline{k}}\) in its local pseudonym vectors to connect \(D_{\overline{i}}\), and then updates the seed and pseudonym for the next session; this \(PN_{\overline{i},\overline{k}}\) may lag behind the active pseudonym at \(D_{\overline{i}}\)s side, due to possible attacks or unreliable transmissions. Fortunately the lag-behind of \(PN_{\overline{i},\overline{k}}\) at the server's side also implies that this \(PN_{\overline{i},\overline{k}}\) in the previous sessions does not result in