43 Pages

Introduction Assumptions On Shoup's lemma The proof Conclusion


Gain access to the library to view online
Learn more


Introduction Assumptions On Shoup's lemma The proof Conclusion Automatically Verified Mechanized Proof of One-Encryption Key Exchange Bruno Blanchet INRIA, Ecole Normale Superieure, CNRS, Paris January 2012 Bruno Blanchet (INRIA, ENS, CNRS) OEKE in CryptoVerif January 2012 1 / 35

  • automatically verified

  • property obvious

  • encrypted key

  • ?? pn

  • cryptoverif

  • exchange

  • evaluation contexts

  • ecole normale



Published by
Reads 10
Language English
Automatically Verified Mechanized Proof of One-Encryption Key Exchange
January 2012
´ INRIA,EcoleNormaleSup´erieure,CNRS,Paris
Bruno Blanchet blanchet@di.ens.fr
OEKE (One-Encryption Key Exchange)[Bresson, Chevassut, Pointcheval, CCS’03]: Variant of EKE (Encrypted Key Exchange) A password-based key exchange protocol. A non-trivial protocol. It took some time before getting a computational proof of this protocol. Our goal: Mechanize, and automate as far as possible, its proof using the automatic computational protocol verifierCryptoVerif. This is an opportunity forseveral interesting extensionsof CryptoVerif.
Gamen p2. . .pnProperty negligible negligible obvious
Proofs by sequences of games
Proofs in the computational model are typically proofs by sequences of games [Shoup, Bellare&Rogaway]: The first game is thereal protocol. One goes from one game to the next by syntactic transformations or by applying the definition of security of a cryptographic primitive. The difference of probability between consecutive games is negligible. The last game is“ideal”: the security property is obvious from the form of the game. (The advantage of the adversary is 0 for this game.)
Game 0←→Game 1 Protocolp1 to prove negligible
CryptoVerif background: Indistinguishability
Definition (Indistinguishability) We writeGpVG0when, for all evaluation contextsCacceptable forG andG0with public variablesVand all distinguishersD,
|Pr[C[G] :D]Pr[C[G0] :D]| ≤p(C,D).
The gameGinteracting with an adversary (evaluation context)Cis denotedC[G]. C[G] may execute events, collected in a sequenceE. AdistinguisherDtakes as inputEand returnstrueorfalse. Example:De(E) =trueif and only ife∈ E.Deis abbreviatede. Pr[C[G] :D] is the probability thatC[G] executesEsuch that D(E) =true.