43 Pages
English

Introduction Assumptions On Shoup's lemma The proof Conclusion

-

Gain access to the library to view online
Learn more

Description

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


Subjects

Informations

Published by
Reads 10
Language English
IntroductionAssmutpoisnnOhSuopemslThmaroepCoofulcnnoisonlBBur,ENSNRIAet(IanchpyrCniEKEO)SRNC,20ryuaanfJriVeto1/12
Automatically Verified Mechanized Proof of One-Encryption Key Exchange
35
January 2012
´ INRIA,EcoleNormaleSup´erieure,CNRS,Paris
Bruno Blanchet blanchet@di.ens.fr
itnosAuspmitnoOsIntroducnoCfoorpnoisulcsuphonSheaTmmlelaoBhencunBr5
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.
Motivation
nuarifJa22/3y201CniEKEO)reVotpyrA,RIINt(RSCNS,EN
CrinKEOEriVetoypE,AIRNI()SRNC,SN
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
auyrJfna/3530221BrunoBlanchetItnorudtcoiisnocnulfooCroepThmaemslpouhSnOsnoitpmussAn
)OEKEinCENS,CNRS(tNIIR,ABoalcneh
CryptoVerif background: Indistinguishability
Definition (Indistinguishability) We writeGpVG0when, for all evaluation contextsCacceptable forG andG0with public variablesVand all distinguishersD,
5
|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.
01y2/324aJfirauntpyrreVonurBucodontitrInOsnoohSnussAitpmelmmpusrpooTaehclusfConion