Paper 2007/128

Computationally Sound Mechanized Proofs of Correspondence Assertions

Bruno Blanchet

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.

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 2 fixes Definition 4, updates Definition 2 to use the same notations, and provides other minor updates.

Metadata
Available format(s)
PDF
Category
Cryptographic protocols
Publication info
Published elsewhere. Major revision. CSF'07 (IEEE Computer Security Foundations Symposium)
DOI
10.1109/CSF.2007.16
Keywords
cryptographic protocolsautomatic verificationcomputationally soundcorrespondence assertionsauthentication
Contact author(s)
bruno blanchet @ inria fr
History
2017-06-06: revised
2007-04-04: received
See all versions
Short URL
https://ia.cr/2007/128
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2007/128,
      author = {Bruno Blanchet},
      title = {Computationally Sound Mechanized Proofs of Correspondence Assertions},
      howpublished = {Cryptology ePrint Archive, Paper 2007/128},
      year = {2007},
      doi = {10.1109/CSF.2007.16},
      note = {\url{https://eprint.iacr.org/2007/128}},
      url = {https://eprint.iacr.org/2007/128}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.