Cryptology ePrint Archive: Report 2007/128
Computationally Sound Mechanized Proofs of Correspondence Assertions
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
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.
Category / Keywords: cryptographic protocols / cryptographic protocols, automatic verification, computationally sound, correspondence assertions, authentication
Publication Info: The conference version of this paper is to appear at CSF'07 (IEEE Computer Security Foundations Symposium)
Date: received 4 Apr 2007
Contact author: blanchet at di ens fr
Available format(s): Postscript (PS) | Compressed Postscript (PS.GZ) | PDF | BibTeX Citation
Note: This is the full version of the paper. Compared to the conference version, this version adds appendices, which contain details on the semantics of the calculus, the proof engine we use for reasoning on games, the proofs of our results, and our experiments.
Version: 20070404:095542 (All versions of this report)
Discussion forum: Show discussion | Start new discussion
[ Cryptology ePrint archive ]