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 have previously implemented a compiler that takes a specification of the protocol in the input language of the computational protocol verifier CryptoVerif and translates it into an OCaml implementation. 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 2nd Conference on Principles of Security and Trust (POST 2013) (David Basin, John Mitchell, eds.), Springer Verlag, volume 7796, 2013.
Bibtex Entry:
@string{lncs="Lecture Notes on Computer Science"}
@string{spv="Springer Verlag"}
@InProceedings{CadeBlanchet12b,
  author = 	 {David Cad{\'e} and Bruno Blanchet},
  title = 	 {Proved Generation of Implementations from Computationally-Secure Protocol Specifications},
  booktitle = {2nd Conference on Principles of Security and Trust (POST 2013)},
  pages = 	 {63--82},
  year = 	 2013,
  editor = 	 {David Basin and John Mitchell},
  volume = 	 7796,
  series = 	 lncs,
  address = 	 {Rome, Italy},
  month = 	 mar,
  publisher = spv,
  abstract = {In order to obtain implementations of security protocols proved secure
in the computational model, we have previously implemented a compiler
that takes a specification of the protocol in the input language of
the computational protocol verifier CryptoVerif and translates
it into an OCaml implementation. 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.},
  x-language = {EN},
  x-audience = {international},
  x-town = {Rome},
  x-country = {IT},
  url = {http://prosecco.gforge.inria.fr/personal/bblanche/publications/CadeBlanchetPOST13.html}
}
Powered by bibtexbrowser