BlanchetOakland06

Bruno Blanchet Back to publications

Bruno Blanchet. A Computationally Sound Mechanized Prover for Security Protocols. In IEEE Symposium on Security and Privacy, pages 140-154, Oakland, California, May 2006.

Get the paper

.ps.gz, 162 Kb, .pdf, 261 Kb

Links

Extended version available as ePrint Report 2005/401, http://eprint.iacr.org/2005/401

Slides of the talk.

Abstract

We present a new mechanized prover for secrecy properties of cryptographic protocols. In contrast to most previous provers, our tool does not rely on the Dolev-Yao model, but on the computational model. It produces proofs presented as sequences of games; these games are formalized in a probabilistic polynomial-time process calculus. Our tool provides a generic method for specifying security properties of the cryptographic primitives, which can handle shared- and public-key encryption, signatures, message authentication codes, and hash functions. Our tool produces proofs valid for a number of sessions polynomial in the security parameter, in the presence of an active adversary. We have implemented our tool and tested it on a number of examples of protocols from the literature.

Bibtex


@INPROCEEDINGS{BlanchetOakland06,
  AUTHOR = {Bruno Blanchet},
  TITLE = {A Computationally Sound Mechanized Prover for Security Protocols},
  BOOKTITLE = {IEEE Symposium on Security and Privacy},
  PAGES = {140-154},
  YEAR = 2006,
  ADDRESS = {Oakland, California},
  MONTH = MAY
}

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