Skip to Main content Skip to Navigation
Journal articles

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.
Document type :
Journal articles
Complete list of metadata
Contributor : Ben Smyth Connect in order to contact the contributor
Submitted on : Wednesday, September 18, 2013 - 5:37:56 PM
Last modification on : Friday, January 21, 2022 - 3:15:20 AM

Links full text




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⟩



Record views