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.


Seminar homepage:


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.


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

E-mail/Courrier électronique : (remove trap-)