Introduction Calculus Proof technique Example proof Conclusion

De
Publié par

Introduction Calculus Proof technique Example proof Conclusion CryptoVerif: A Computationally Sound Mechanized Prover for Cryptographic Protocols Bruno Blanchet CNRS, Ecole Normale Superieure, INRIA, Paris June 2009 Bruno Blanchet (CNRS, ENS, INRIA) CryptoVerif June 2009 1 / 38

  • cryptographic primitives

  • proofs can

  • proof technique

  • bitstrings cryptographic primitives

  • approach allows

  • direct approach

  • dolev-yao model

  • automatic proof


Publié le : mardi 19 juin 2012
Lecture(s) : 34
Source : di.ens.fr
Nombre de pages : 39
Voir plus Voir moins
IntroductionCaluculPsorfoethcineEqumpxaprlefCoolcnooisunteC(nahconlBBurA)CrINRIENS,NRS,002enuJfireVotpy
Bruno Blanchet
June 2009
CryptoVerif: A Computationally Sound Mechanized Prover for Cryptographic Protocols
´ CNRS,EcoleNormaleSupe´rieure,INRIA,Paris
8/391
IortntcudethcinuqEeaxpmelionCalculusProofonfCooprniousclnu2e00293/8
Two models for security protocols: Computational model: messages are bitstrings cryptographic primitives are functions from bitstrings to bitstrings the adversary is a probabilistic polynomial-time Turing machine Proofs are done manually. Formal model(so-called “Dolev-Yao model”): cryptographic primitives are ideal blackboxes messages are terms built from the cryptographic primitives the adversary is restricted to use only the primitives Proofs can be done automatically. Our goal: achieveautomatic provabilityunder the realisticcomputational assumptions.
Introduction
RIA)CryptoVerifJtehcRNC(NE,SNI,SBnoruanBl
C(RNhctelBnauronBVetofJrie2un9300NE,SNI,S)AIRpyrC3/8
Two approaches for the automatic proof of cryptographic protocols in a computational model: Indirect approach: 1) Make a Dolev-Yao proof. 2) Use a theorem that shows the soundness of the Dolev-Yao approach with respect to the computational model. Pioneered by Abadi and Rogaway; pursued by many others. Direct approach: Design automatic tools for proving protocols in a computational model. Approach pioneered by Laud.
Introduction
clusionproofConEeaxpmelethcinuqsPluofronCiocualortntcudI
00493/8
The indirect approach allows more reuse of previous work, but it has limitations: Hypotheseshave to be added to make sure that the computational and Dolev-Yao models coincide. Theallowed cryptographic primitivesare often limited, and only ideal, not very practical primitives can be used. Using the Dolev-Yao model is actually a (big)detour; The computational definitions of primitives fit the computational security properties to prove. They do not fit the Dolev-Yao model. We decided to focus on the direct approach.
Advantages and drawbacks
CryptoVerifJune2InooftusPriqueechncuitrtdocllunoaCConcroofplepExamnoulis(CNRS,ENS,INRIA)BuronlBnahcte
ionCfnolcsupmelrpootnorIhcetfooraxEeuqinnCioctdusPlucualRNC(tehcNI,SNE,SBanBlnorunu2e00593/8
We have implemented anautomatic prover: provessecrecyandcorrespondenceproperties. provides agenericmethod for specifying properties of cryptographic primitiveswhich handles MACs (message authentication codes), symmetric encryption, public-key encryption, signatures, hash functions, . . . works forNsessions(polynomial in the security parameter), with an active adversary. gives a bound on theprobabilityof an attack (exact security).
An automatic prover
RIA)CryptoVerifJ
693/2e008
As in Shoup’s and Bellare&Rogaway’s method, the proof is asequence of games: 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. Between consecutive games, the difference of probability of success of an attack is negligible. The last game is“ideal” security property is obvious from the: the form of the game. (The advantage of the adversary is typically 0 for this game.)
Produced proofs
BrunoBlanchCrA)toypriVeunfJC(te,SRN,SNEIRNIioctdurontIoisunCfoolcnoxampleprchniqueEPsorfoetCnlaucul
niousntIlaCnulucudoroitcchniqueEsProofteooCfnolcaxpmelrp
Process calculus for games
83
Games are formalized in aprocess calculus: It is adapted from the pi calculus. The semantics ispurely probabilistic(no non-determinism). All processes run inpolynomial time: polynomial number of copies of processes, length of messages on channels bounded by polynomials. This calculus is inspired by: the calculus of [Lincoln, Mitchell, Mitchell, Scedrov, 1998], the calculus of [Laud, 2005].
oVerifJune20097/E,SNI,RNAIC)yrtpnclaoBunRSCNt(herB
83/
x0kfresh
0 AB:e={xk}xk,mac(e,xmk)
x0kshould remain secret.
Asends toBa fresh keyxk0encrypted under authenticated encryption, implemented as encrypt-then-MAC.
BrunoBlanchet(CNR,SNE,SNIIR)ArCpytoVerifJune20098prlefCooeEqumpxaaxEnelpmlcnooisunCalctioroduInthcinfoetPsorucul
ioctalnCntIduroetfoinhculucorPsoofCleprxampqueEnsuoinolcCNt(henclaoBunBryrC)AIRNI,SNE,SRJune2009ptoVerif
xk0fresh
AB:e={xk0}xk,mac(e,xmk)
/983
Example (initialization)
Initialization of keys: 1The processQ0waits for a message on channelstartto start running. The adversary triggers this process. 2Q0generates encryption and MAC keys,xkandxmkrespectively, using the key generation algorithmskgenandmkgen. 3Q0returns control to the adversary by the outputchi. QAandQBrepresent the actions ofAandB(see next slides).
Q0=start();newxr:keyseed;letxk:key=kgen(xr)in newxr0:mkeyseed;letxmk:mkey=mkgen(xr0)inchi; (QA|QB)
er).ametyparuritsecenihtimlaylonpos(metinnrubeanclocotorpehT]n,1xesbyi[ies,indenestcnponerrpsefAeo!i:1olRAcB.nnlelBnauronmesssthenchaageo0xyekhsednesdnakchsscerofrsaseooaevdreasyr3.hTpegeissentoncAbythregghwdemaneassehe2TocprsiesristuqinhcetfoorPsulonfCooprlempxaeEIalcuionCductntroclusion,SNI,SNEC(RNhcterifJtoVeCrypRIA)
AB:e={xk0}xk,mac(e,xmk)xk0fresh
QA= !incA();newx0k:key;newxr00:coins; letxm:bitstring=enc(k2b(xk0),xk,xr00)in cAhxm,mac(xm,xmk)i
Example (role ofA)
83/019002enu
sPluofronCiocualortntcudIclusionEproofConEeaxpmelethcinuq(rlempxa)fBeool83/
AB:e={x0k}xk,mac(e,xmk)x0kfresh
QB= !i0ncB(x0m:bitstring,xma:macstring); ifverify(x0m,xmk,xma)then leti(k2b(x0k0)) =dec(x0m,xk)incBhi
Role ofB: 1ncopies, as forQA. 2The processQBwaits for the message on channelcB. 3It verifies the MAC, decrypts, and stores the key inx0k0.
02en1190eroVJuif)CIAptryE,SNI,RNeh(tNCSRunoBlancBr
Soyez le premier à déposer un commentaire !

17/1000 caractères maximum.