In order to prove the security of OEKE protocol, CryptoVerif has been extended to handle proofs based on the computational Difﬁe-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 efﬁcient password-based key exchange, CCS’03].
Post a Comment