Common use of Security Simulation Using AVISPA Tool Clause in Contracts

Security Simulation Using AVISPA Tool. [16] In this subsection, we perform the security verification simulations for the proposed scheme using the AVISPA tool. It is a software tool and quite popular for performing automated verification of Internet security protocols and applications. The tool is widely used in industry and academia. For verification, the tool integrates backend servers, such as On-the-Fly Model Checker (OFMC) and Constraint-Logic-based Attack Searcher (Cl-AtSe). The AVISPA uses a high-level security protocol specification language (HLPSL). The HLPSL specifies the roles of each actor (e.g., SM and SP). These roles are as follows: (i) Basic role reports what initial information can be used by the SP and SM and how the conversions are being happening in the protocol; (ii) Composition role reports a session where the SP and SM are communicating together; (iii) Environment role provides details the global parameters, sessions and an attacker knowledge in the key agreement phase in the proposed protocol. In security verification, the tool utilizes the Xxxxx-Xxx model [24], which is represented as the channel(dy). We developed HLPSL script for the proposed scheme (i.e., key agreement phase). The SP and SM basic roles are shown in Figure 6. The results of the security verification presented in Figure 7 show that the proposed scheme is secure and SAFE from attacks using the (OFMC) backend. Precisely, Table 1 summaries the results from the AVISPA tool that the proposed key agreement achieved confidentiality and authentication. In addition, it is safe from MITM and replay attacks with a bounded number of sessions. role ServiceProvider(SM, SP : agent, K, SK : symmetric_key, SPp : public_key, H : hash_func, RCV, SND : channel (dy) ) played_by XX xxx= local State : nat, idA, idB, : text, M0,M1,M2 : message, H : hash_func Const SM_r1, SP_r2: protocol_id, sub1, sub2: protocol_id, init State := 0 transition