Security

From Computationally-Proved Protocol Specifications to Implementations and Application to SSH

Download Now Date Added: Mar 2013
Format: PDF

This paper presents a novel technique for obtaining implementations of security protocols, proved secure in the computational model. The authors formally specify the protocol to prove, they prove this specification using the computationally-sound protocol verifier CryptoVerif, and they automatically translate it into an implementation in OCaml using a new compiler that they have implemented. They applied this approach to the SSH Transport Layer protocol: they proved the authentication of the server and the secrecy of the session keys in this protocol and verified that the generated implementation successfully interacts with OpenSSH.