## 6 Formal Security Verification Using AVISPA  
This section shows the resilience of the proposed scheme (LDAKM-EIoT) against replay and man-in-the-middle attacks based on the formal security verification. We applied the broadly-accepted \"Automated Validation of Internet Security Protocols and Applications (AVISPA)\" tool [52] to achieve this goal. There are four backends, namely \"on-the-fly mode-checker (OFMC)\", \"constraint-logic based attack searcher (CL-AtSe)\", \"SAT (Boolean satisfiability problem) based model checker (SATMC)\", and \"tree automata based on automatic approximations for the analysis of security protocols (TA4 SP)\", which are integrated with the AVISPA tool. These backends help in automatic execution analysis of the security protocols. The \"High-Level Protocol Specification Language (HLPSL)\" helps in converting the high level implementation of the the security protocols into the \"Intermediate Format (IF)\" using the HLPSL2 IF translator. HLPSL defines the roles for all the involved participating entities in a protocol, which are termed as the basic roles. The compulsory roles, known as \"session\" and \"goal and environment\", consist of the composition of the sessions along with globally defined constants, respectively. The IF is provided as input to one of the four backends to produce the \"Output Format (OF)\", which explicitly explains under what conditions the protocol becomes \"safe\", \"unsafe\", or \"inconclusive\". The precise discussion on AVISPA and its HLPSL is available in [52]. The AVISPA tool is one of the widely used formal security verification tools. Researchers working in the authentication domain frequently use this software tool to validate the security of authentication protocols [1; 2; 3; 46; 48; 53].  
In our implementation of the proposed scheme (LDAKM-EIoT) under HLPSL, we defined four basic roles: (a) the role for the \(TA\), (b) the role for an IoT device \(D_{i}\), (c) the role for the edge node \(EN\), and (d) the role for a cloud server \(CS_{j}\). Apart from these basic roles, we had two compulsory roles (\"session\" and \"goal and environment\"). We applied the \"SPAN (Security Protocol ANimator for AVISPA)\" [54] for simulating LDAKM-EIoT. The backends that we covered were OFMC and CL-AtSe, because they support the bitwise XOR operation. Therefore, we excluded the simulation results under other backends (i.e., SATMC and TA4 SP) from the simulation part, because they did not currently support XOR operation, and the results would be under these backends \"inconclusive\". Figure 4 shows the simulation results under the OFMC and CL-AtSe backends. The summary of these backends helped us to predict the security of a designed scheme against replay and man-in-the-middle attacks. Under the OFMC backend, the simulation took 1019 milliseconds, while traversing 129 visited nodes at a depth of 20 plies. On the other hand, under the CL-Atse backend, 256 states were analyzed, and out of those states, 124 states were reachable with 0.58 s of translation time and 0.05 s of computation. The provided simulation results assured that LDAKM-EIoT was safe against the replay and man-in-the-middle attacks.