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.
If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.
% BibTex
@inproceedings{BraghinLR21,
author = {Chiara Braghin and
Mario Lilli and
Elvinia Riccobene},
editor = {Alexander Raschke and
Dominique M{\'{e}}ry},
title = {Towards ASM-Based Automated Formal Verification of Security Protocols},
booktitle = {Rigorous State-Based Methods - 8th International Conference, {ABZ}
2021, Ulm, Germany, June 9-11, 2021, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {12709},
pages = {17--33},
publisher = {Springer},
year = {2021},
url = {https://doi.org/10.1007/978-3-030-77543-8\_2},
doi = {10.1007/978-3-030-77543-8\_2},
timestamp = {Tue, 15 Jun 2021 17:24:03 +0200},
biburl = {https://dblp.org/rec/conf/asm/BraghinLR21.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}