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.

Towards ASM-Based Automated Formal Verification of Security Protocols / C. Braghin, M. Lilli, E. Riccobene (LECTURE NOTES IN ARTIFICIAL INTELLIGENCE). - In: Rigorous State-Based Methods / [a cura di] A. Raschke, D. Méry. - [s.l] : Springer Science and Business Media Deutschland GmbH, 2021. - ISBN 978-3-030-77542-1. - pp. 17-33 (( Intervento presentato al 8. convegno International Conference on Rigorous State-Based Methods tenutosi a Virtual, Online nel 2021 [10.1007/978-3-030-77543-8_2].

Towards ASM-Based Automated Formal Verification of Security Protocols

C. Braghin
Primo
;
M. Lilli
Secondo
;
E. Riccobene
Ultimo
2021

Abstract

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.
Abstract state machines; Cryptographic protocols; Security assurance
Settore INF/01 - Informatica
Book Part (author)
File in questo prodotto:
File Dimensione Formato  
ABZ2021_paper8.pdf

accesso riservato

Tipologia: Pre-print (manoscritto inviato all'editore)
Dimensione 402.31 kB
Formato Adobe PDF
402.31 kB Adobe PDF   Visualizza/Apri   Richiedi una copia
Braghin2021_Chapter_TowardsASM-BasedAutomatedForma.pdf

accesso riservato

Tipologia: Publisher's version/PDF
Dimensione 554.01 kB
Formato Adobe PDF
554.01 kB Adobe PDF   Visualizza/Apri   Richiedi una copia
Pubblicazioni consigliate

Caricamento pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/2434/919536
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
  • ???jsp.display-item.citation.isi??? ND
social impact