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

https://hal.inria.fr/hal-00863392
Contributor : Ben Smyth <>
Submitted on : Wednesday, September 18, 2013 - 5:37:56 PM
Last modification on : Friday, May 25, 2018 - 12:02:06 PM

Links full text

Identifiers

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⟩

Share

Metrics

Record views

327