Automatic Analysis of One-Encryption Key Exchange

Last day of the CSF conference in Harvard, Bruno Blanchet gave a talk concerning the automatic proof of the password-based protocol One-Encryption Key Exchange (OEKE). The proof has been carried out by using Blanchet's tool CryptoVerif.

In order to prove the security of OEKE protocol, CryptoVerif has been extended to handle proofs based on the computational Diffie-Hellman assumption and Shoup’s lemma.

In particular, for applications of Shoup’s lemma, he showed how to improve over the standard computation of probabilities. The idea is that of avoiding to count several times those probabilities that correspond to the same execution. This technique resulted in a proof of OEKE with a better reduction factor compared with  a previous manual proof in [Bresson, Chevassut, Pointcheval, Security proofs for an efficient password-based key exchange, CCS’03].