Automatically Verified Mechanized Proof of One-Encryption Key Exchange
The authors 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 paper was also an opportunity to implement several important extensions of CryptoVerif, useful for proving many other protocols. They have indeed extended CryptoVerif to support the computational Diffie-Hellman assumption. They 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.