Proved Generation of Implementations from Computationally Secure Protocol Specifications (bibtex)

by David Cadé, Bruno Blanchet

Abstract:

In order to obtain implementations of security protocols proved secure in the computational model, we previously proposed the following approach: we write a specification of the protocol in the input language of the computational protocol verifier CryptoVerif, prove it secure using CryptoVerif, then generate an OCaml implementation of the protocol from the CryptoVerif specification using a specific compiler that we have implemented. However, until now, this compiler was not proved correct, so we did not have real guarantees on the generated implementation. In this paper, we fill this gap. We prove that this compiler preserves the security properties proved by CryptoVerif: if an adversary has probability $p$ of breaking a security property in the generated code, then there exists an adversary that breaks the property with the same probability $p$ in the CryptoVerif specification. Therefore, if the protocol specification is proved secure in the computational model by CryptoVerif, then the generated implementation is also secure.

Reference:

Proved Generation of Implementations from Computationally Secure Protocol Specifications (David Cadé, Bruno Blanchet), In Journal of Computer Security, volume 23, 2015.

Bibtex Entry:

@Article{CadeBlanchetJCS14, author = {David Cad{\'e} and Bruno Blanchet}, title = {Proved Generation of Implementations from Computationally Secure Protocol Specifications}, journal = {Journal of Computer Security}, year = 2015, volume = 23, number = 3, pages = {331--402}, abstract = {In order to obtain implementations of security protocols proved secure in the computational model, we previously proposed the following approach: we write a specification of the protocol in the input language of the computational protocol verifier CryptoVerif, prove it secure using CryptoVerif, then generate an OCaml implementation of the protocol from the CryptoVerif specification using a specific compiler that we have implemented. However, until now, this compiler was not proved correct, so we did not have real guarantees on the generated implementation. In this paper, we fill this gap. We prove that this compiler preserves the security properties proved by CryptoVerif: if an adversary has probability $p$ of breaking a security property in the generated code, then there exists an adversary that breaks the property with the same probability $p$ in the CryptoVerif specification. Therefore, if the protocol specification is proved secure in the computational model by CryptoVerif, then the generated implementation is also secure.} }

Powered by bibtexbrowser