BlanchetCSF07
Bruno Blanchet
Back to publications
Bruno Blanchet.
Computationally Sound Mechanized Proofs of Correspondence
Assertions.
In 20th IEEE Computer Security Foundations Symposium (CSF'07),
pages 97-111, Venice, Italy, July 2007. IEEE.
Copyright
© IEEE.
Get the paper
.pdf, 221 Kb
Links
Extended version available as Cryptology ePrint Archive, Report 2007/128.
Slides of the talk.
Abstract
We present a new mechanized prover for showing correspondence
assertions for cryptographic protocols in the computational model.
Correspondence assertions are useful in particular for establishing
authentication.
Our technique produces proofs by sequences of games, as standard in
cryptography. These proofs are valid for a number of sessions
polynomial in the security parameter, in the presence of an active
adversary. Our technique can handle a wide variety of cryptographic
primitives, including shared- and public-key encryption, signatures,
message authentication codes, and hash functions. It has been
implemented in the tool CryptoVerif and successfully tested on
examples from the literature.
Bibtex
@INPROCEEDINGS{BlanchetCSF07,
AUTHOR = {Bruno Blanchet},
TITLE = {Computationally Sound Mechanized Proofs of Correspondence Assertions},
BOOKTITLE = {20th IEEE Computer Security Foundations Symposium (CSF'07)},
PAGES = {97--111},
YEAR = 2007,
ADDRESS = {Venice, Italy},
MONTH = JUL,
ORGANIZATION = {IEEE}
}
E-mail/Courrier électronique : Bruno.Blanchet@trap-inria.fr (remove trap-)