Formal verification of security protocol implementations: a survey

Abstract : Automated formal verification of security protocols has been mostly focused on analyzing high-level abstract models which, however, are significantly different from real protocol implementations written in programming languages. Recently, some researchers have started investigating techniques that bring automated formal proofs closer to real implementations. This paper surveys these attempts, focusing on approaches that target the application code that implements protocol logic, rather than the libraries that implement cryptography. According to these approaches, libraries are assumed to correctly implement some models. The aim is to derive formal proofs that, under this assumption, give assurance about the application code that implements the protocol logic. The two main approaches of model extraction and code generation are presented, along with the main techniques adopted for each approach.
Type de document :
Article dans une revue
Formal Aspects of Computing, Springer Verlag, 2014, 26 (1), pp.99-123. 〈10.1007/s00165-012-0269-9〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00863392
Contributeur : Ben Smyth <>
Soumis le : mercredi 18 septembre 2013 - 17:37:56
Dernière modification le : vendredi 25 mai 2018 - 12:02:06

Lien texte intégral

Identifiants

Collections

Citation

Matteo Avalle, Alfredo Pironti, Riccardo Sisto. Formal verification of security protocol implementations: a survey. Formal Aspects of Computing, Springer Verlag, 2014, 26 (1), pp.99-123. 〈10.1007/s00165-012-0269-9〉. 〈hal-00863392〉

Partager

Métriques

Consultations de la notice

114