International Association for Cryptologic Research

International Association
for Cryptologic Research


Paper: Computationally Sound Mechanized Proofs of Correspondence Assertions

Bruno Blanchet
Search ePrint
Search Google
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.
  title={Computationally Sound Mechanized Proofs of Correspondence Assertions},
  booktitle={IACR Eprint archive},
  keywords={cryptographic protocols / cryptographic protocols, automatic verification, computationally sound, correspondence assertions, authentication},
  note={The conference version of this paper is to appear at CSF'07 (IEEE Computer Security Foundations Symposium) 13607 received 4 Apr 2007},
  author={Bruno Blanchet},