Sciweavers

Share
CSFW
2007
IEEE

Computationally Sound Mechanized Proofs of Correspondence Assertions

10 years 5 months ago
Computationally Sound Mechanized Proofs of Correspondence Assertions
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.
Bruno Blanchet
Added 02 Jun 2010
Updated 02 Jun 2010
Type Conference
Year 2007
Where CSFW
Authors Bruno Blanchet
Comments (0)
books