BlanchetLink05

Bruno Blanchet Back to publications

Bruno Blanchet. A Computationally Sound Automatic Prover for Cryptographic Protocols. In Workshop on the link between formal and computational models, Paris, France, June 2005.

Links

Workshop homepage: http://www.loria.fr/~cortier/workshop.html

Abstract

We present an automatic tool for proving cryptographic protocols secure in a computational model. The produced proofs are sequences of games, following Shoup's proof technique. This tool handles any number of sessions of the protocol (specified as a variable N), in the presence of an active adversary. It allows using realistic definitions for primitives (for instance, encryption does not need to be length concealing). Currently, it proves secrecy for protocols using macs and stream ciphers; extensions to other security properties and primitives are planned.

Bibtex


@INPROCEEDINGS{BlanchetLink05,
  AUTHOR = {Bruno Blanchet},
  TITLE = {A Computationally Sound Automatic Prover for Cryptographic Protocols},
  BOOKTITLE = {Workshop on the link between formal and computational models},
  YEAR = 2005,
  ADDRESS = {Paris, France},
  MONTH = JUN
}

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