BlanchetTDSC07

Bruno Blanchet Back to publications
Bruno Blanchet. A Computationally Sound Mechanized Prover for Security Protocols. IEEE Transactions on Dependable and Secure Computing, 5(4):193-207, October-December 2008. Special issue IEEE Symposium on Security and Privacy 2006. Electronic version available at http://doi.ieeecomputersociety.org/10.1109/TDSC.2007.1005.

Copyright

© IEEE.

Get the paper

.ps.gz, 471 Kb, .pdf, 789 Kb

Abstract

We present a new mechanized prover for secrecy properties of security 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-key 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


@ARTICLE{BlanchetTDSC07,
  AUTHOR = {Bruno Blanchet},
  TITLE = {A Computationally Sound Mechanized Prover for Security Protocols},
  JOURNAL = {IEEE Transactions on Dependable and Secure Computing},
  YEAR = 2008,
  VOLUME = 5,
  NUMBER = 4,
  PAGES = {193--207},
  MONTH = OCT # {--} # DEC,
  NOTE = {Special issue IEEE Symposium on Security and Privacy 2006. Electronic version available at http://doi.ieeecomputersociety.org/10.1109/TDSC.2007.1005.}
}


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