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

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.

Provided by: INRIA Topic: Security Date Added: Mar 2013 Format: PDF

Find By Topic