From Computationally-Proved Protocol Specifications to Implementations and Application to SSH (bibtex)
by David Cadé, Bruno Blanchet
Abstract:
This paper presents a novel technique for obtaining implementations of security protocols, proved secure in the computational model. We formally specify the protocol to prove, we prove this specification using the computationally-sound protocol verifier CryptoVerif, and we automatically translate it into an implementation in OCaml using a new compiler that we have implemented. We applied this approach 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. We explain these proofs, as well as an extension of CryptoVerif needed for the proof of secrecy of the session keys. The secrecy of messages sent over the SSH tunnel cannot be proved due to known weaknesses in SSH with CBC-mode encryption.
Reference:
From Computationally-Proved Protocol Specifications to Implementations and Application to SSH (David Cadé, Bruno Blanchet), In Journal of Wireless Mobile Networks, Ubiquitous Computing, and Dependable Applications (JoWUA), Innovative Information Science & Technology Research Group (ISYOU), volume 4, 2013. (Special issue ARES'12)
Bibtex Entry:
@Article{CadeBlanchetJoWUA13,
  author = 	 {David Cad{\'e} and Bruno Blanchet},
  title = 	 {From Computationally-Proved Protocol Specifications to Implementations and Application to {SSH}},
  journal = 	 {Journal of Wireless Mobile Networks, Ubiquitous Computing, and Dependable Applications (JoWUA)},
  year = 	 2013,
  volume = 	 4,
  number = 	 1,
  pages = 	 {4--31},
  month = 	 mar,
  publisher = {Innovative Information Science \& Technology Research Group (ISYOU)},
  abstract = {This paper presents a novel technique for obtaining implementations
  of security protocols, proved secure in the computational model.
  We formally specify the protocol to prove, we prove this specification
  using the computationally-sound protocol verifier CryptoVerif, and 
  we automatically translate it into an implementation in
  OCaml using a new compiler that we have implemented. 
  We applied this approach 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. We explain these proofs, as well as an extension 
  of CryptoVerif needed for the proof of secrecy of the session keys.
  The secrecy of messages sent over the SSH tunnel
  cannot be proved due to known weaknesses in SSH with CBC-mode
  encryption.},
  x-language = {EN},
  x-audience = {international},
  note = {Special issue ARES'12},
  url = {http://prosecco.gforge.inria.fr/personal/bblanche/publications/CadeBlanchetJoWUA13.html}
}
Powered by bibtexbrowser