BlanchetDagstuhl07

Bruno Blanchet Back to publications
Bruno Blanchet. CryptoVerif: A Computationally Sound Mechanized Prover for Cryptographic Protocols. In Dagstuhl seminar Formal Protocol Verification Applied, October 2007.

Links

Seminar homepage: http://www.dagstuhl.de/07421/

Abstract

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

Bibtex


@INPROCEEDINGS{BlanchetDagstuhl07,
  AUTHOR = {Bruno Blanchet},
  TITLE = {Crypto{V}erif: A Computationally Sound Mechanized Prover for Cryptographic Protocols},
  BOOKTITLE = {Dagstuhl seminar "Formal Protocol Verification Applied"},
  YEAR = 2007,
  MONTH = OCT
}


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