Skip to Main content Skip to Navigation
Theses

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 :
Theses
Complete list of metadata

Cited literature [51 references]  Display  Hide  Download

https://hal.inria.fr/tel-01112630
Contributor : Bruno Blanchet <>
Submitted on : Tuesday, February 3, 2015 - 12:36:59 PM
Last modification on : Thursday, March 5, 2020 - 4:53:10 PM
Long-term archiving on: : Wednesday, May 27, 2015 - 4:06:08 PM

File

Identifiers

  • HAL Id : tel-01112630, version 1

Collections

Citation

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

Share

Metrics

Record views

212

Files downloads

250