Paper 2012/173

Automatically Verified Mechanized Proof of One-Encryption Key Exchange

Bruno Blanchet, French Institute for Research in Computer Science and Automation, École Normale Supérieure - PSL, French National Centre for Scientific Research
Abstract

We present a mechanized proof of the password-based protocol One-Encryption Key Exchange (OEKE) using the computationally-sound protocol prover CryptoVerif. OEKE is a non-trivial protocol, and thus mechanizing its proof provides additional confidence that it is correct. This case study was also an opportunity to implement several important extensions of CryptoVerif, useful for proving many other protocols. We have indeed extended CryptoVerif to support the computational Diffie-Hellman assumption. We have also added support for proofs that rely on Shoup's lemma and additional game transformations. In particular, it is now possible to insert case distinctions manually and to merge cases that no longer need to be distinguished. Eventually, some improvements have been added on the computation of the probability bounds for attacks, providing better reductions. In particular, we improve over the standard computation of probabilities when Shoup's lemma is used, which allows us to improve the bound given in a previous manual proof of OEKE, and to show that the adversary can test at most one password per session of the protocol. In this paper, we present these extensions, with their application to the proof of OEKE. All steps of the proof are verified by CryptoVerif. This document is an updated version of a report from 2012. In the 10 years between 2012 and 2022, CryptoVerif has made a lot of progress. In particular, the probability bound obtained by CryptoVerif for OEKE has been improved, reaching an almost optimal probability: only statistical terms corresponding to collisions between group elements or between hashes are overestimated by a small constant factor.

Note: v2 updates the report with changes in CryptoVerif, improvements in the probability bounds (the bound for OEKE is now almost optimal), and minor fixes.

Metadata
Available format(s)
PDF
Category
Cryptographic protocols
Publication info
Published elsewhere. This is the full version of a paper to appear at CSF'12 (IEEE Computer Security Foundations Symposium). The full version adds all appendices.
Keywords
Automatic proofs Formal methods Provable security Protocols Password-based authentication
Contact author(s)
bruno blanchet @ inria fr
History
2022-06-27: revised
2012-04-11: received
See all versions
Short URL
https://ia.cr/2012/173
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2012/173,
      author = {Bruno Blanchet},
      title = {Automatically Verified Mechanized Proof of One-Encryption Key Exchange},
      howpublished = {Cryptology ePrint Archive, Paper 2012/173},
      year = {2012},
      note = {\url{https://eprint.iacr.org/2012/173}},
      url = {https://eprint.iacr.org/2012/173}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.