CadeBlanchetARES12

Bruno Blanchet Back to publications

David Cadé and Bruno Blanchet. From Computationally-proved Protocol Specifications to Implementations. In 7th International Conference on Availability, Reliability and Security (AReS 2012), pages 65-74, Prague, Czech Republic, August 2012. IEEE.

Copyright

Get the paper

.pdf, 277 Kb

Abstract

This paper presents a novel framework for proving specifications of security protocols in the computational model and generating runnable implementations from such proved specifications. We rely on the computationally-sound protocol verifier CryptoVerif for proving the specification, and we have implemented a compiler that translates a CryptoVerif specification into an implementation in OCaml. We have applied this compiler to the SSH Transport Layer protocol: we 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. The secrecy of messages sent over the SSH tunnel cannot be proved due to known weaknesses in SSH with CBC-mode encryption.

Bibtex


@INPROCEEDINGS{CadeBlanchetARES12,
  AUTHOR = {David Cad{\'e} and Bruno Blanchet},
  TITLE = {From Computationally-proved Protocol Specifications to Implementations},
  BOOKTITLE = {7th International Conference on Availability, Reliability and Security (AReS 2012)},
  PAGES = {65--74},
  YEAR = 2012,
  ADDRESS = {Prague, Czech Republic},
  MONTH = AUG,
  PUBLISHER = {IEEE}
}

E-mail/Courrier électronique : Bruno.Blanchet@trap-inria.fr (remove trap-)