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-)