Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, EpiSciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
Skip to Main content Skip to Navigation

Proved Implementations of Cryptographic Protocols in the Computational Model

Abstract : The goal of this work is to obtain implementations of security protocols proved in the computational model. We implemented a compiler that takes as input a specification of a protocol in the input language of the protocol verifier CryptoVerif and compiles it into an implementation in OCaml. We proved the secrecy of exchanged keys and authentication of the server in the SSH (Secure SHell) key exchange protocol, and used our compiler on this protocol. We proved that this compiler is correct: if an adversary can break a security property on the generated code with a probability p, then there exists an adversary that can break this property on the specification with the same probability p. Hence, if a specification is proved secure in the computational model by CryptoVerif, then the generated implementation is also secure.
Document type :
Complete list of metadata

Cited literature [51 references]  Display  Hide  Download
Contributor : Bruno Blanchet Connect in order to contact the contributor
Submitted on : Tuesday, February 3, 2015 - 12:36:59 PM
Last modification on : Friday, January 21, 2022 - 3:15:36 AM
Long-term archiving on: : Wednesday, May 27, 2015 - 4:06:08 PM



  • HAL Id : tel-01112630, version 1



David Cadé. Proved Implementations of Cryptographic Protocols in the Computational Model. Cryptography and Security [cs.CR]. Paris 7, 2013. English. ⟨tel-01112630⟩



Record views


Files downloads