Towards ASM-Based Automated Formal Verification of Security Protocols

In the security protocols domain, formal verification is more and more highly demanded to guarantee security assurance: humans increasingly depend on the use of connected devices in their daily life, so they must be protected against possible threats and accidents. However, formal verification, and in general the use of formal methods, is slowed by myths and misconceptions, mainly due to their mathematical base, which discourages many designers or engineers from their adoption. In this paper, we pose the basis for the long-term development of an ASM-based user-friendly framework for the formal verification of security protocols. We introduce a mathematical-based set of templates to formalise common patterns in security protocols and a set of security properties. These templates facilitate the protocol formal verification by providing built-in functions and domains, as well as transition rules and property schema, to be customised according to the specific protocol to be verified. The effectiveness of this approach is shown by means of their application to a number of well-known cryptographic security protocols.