Security Protocol Verification: Symbolic and Computational Models

Bruno Blanchet

Description

Niveau: Supérieur, Doctorat, Bac+8
Security Protocol Verification: Symbolic and Computational Models Bruno Blanchet INRIA, Ecole Normale Superieure, CNRS, Paris Abstract. Security protocol verification has been a very active research area since the 1990s. This paper surveys various approaches in this area, considering the verification in the symbolic model, as well as the more recent approaches that rely on the computational model or that ver- ify protocol implementations rather than specifications. Additionally, we briefly describe our symbolic security protocol verifier ProVerif and sit- uate it among these approaches. 1 Security Protocols Security protocols are programs that aim at securing communications on in- secure networks, such as Internet, by relying on cryptographic primitives. Se- curity protocols are ubiquitous: they are used, for instance, for e-commerce (e.g., the protocol TLS [109], used for https:// URLs), bank transactions, mobile phone and WiFi networks, RFID tags, and e-voting. However, the de- sign of security protocols is particularly error-prone. This can be illustrated for instance by the very famous Needham-Schroeder public-key protocol [160], in which a flaw was found by Lowe [147] 17 years after its publication. Even though much progress has been made since then, many flaws are still found in current security protocols (see, e.

• physical attacks


• syntactic secrecy


• protocol satisfies


• equivalences can


• protocol


• split into


• security protocols


• attacks introduce


• can easily


• public key

Sujets

• Needham
• Blanchet
• Protocol
• Public-key cryptography

Informations

• Publié par: profil-zyak-2012
• Nombre de lectures: 15
• Langue: English

Extrait

SecurityProtocolVerification: SymbolicandComputationalModels BrunoBlanchet INRIA,E ´ coleNormaleSup´erieure,CNRS,Paris [e-mail] Abstract.Securityprotocolverificationhasbeenaveryactiveresearch areasincethe1990s.Thispapersurveysvariousapproachesinthisarea, consideringtheverificationinthesymbolicmodel,aswellasthemore recentapproachesthatrelyonthecomputationalmodelorthatver- ifyprotocolimplementationsratherthanspecifications.Additionally,we brieflydescribeoursymbolicsecurityprotocolverifierProVerifandsit- uateitamongtheseapproaches. 1SecurityProtocols Securityprotocolsareprogramsthataimatsecuringcommunicationsonin- securenetworks,suchasInternet,byrelyingoncryptographicprimitives.Se- curityprotocolsareubiquitous:theyareused,forinstance,fore-commerce (e.g.,theprotocolTLS[109],usedfor https:// URLs),banktransactions, mobilephoneandWiFinetworks,RFIDtags,ande-voting.However,thede- signofsecurityprotocolsisparticularlyerror-prone.Thiscanbeillustrated forinstancebytheveryfamousNeedham-Schroederpublic-keyprotocol[160], inwhichaflawwasfoundbyLowe[147]17yearsafteritspublication.Even thoughmuchprogresshasbeenmadesincethen,manyflawsarestillfound incurrentsecurityprotocols(see,e.g., http://www.openssl.org/news/ and http://www.openssh.org/security.html ).Securityerrorscanhaveserious consequences,resultinginlossofmoneyorlossofconfidenceofusersinthesys- tem.Moreover,securityerrorscannotbedetectedbyfunctionalsoftwaretesting becausetheyappearonlyinthepresenceofamaliciousadversary.Automatic toolscanthereforebeveryhelpfulinordertoobtainactualguaranteesthat securityprotocolsarecorrect.Thisisareasonwhytheverificationofsecurity protocolshasbeenaveryactiveresearchareasincethe1990s,andisstillvery active.Thissurveyaimsatsummarizingtheresultsobtainedinthisarea.Due tothelargenumberofpapersonsecurityprotocolverificationandthelimited space,wehadtoomitmanyofthem;webelievethatwestillpresentrepre- sentativesofthemainapproaches.Additionally,Sect.2.2brieflydescribesour symbolicverificationtoolProVerif. 1.1AnExampleofProtocol Weillustratethenotionofsecurityprotocolwiththefollowingexample,asim- plifiedversionoftheDenning-Saccopublic-keykeydistributionprotocol[108].

2BrunoBlanchet Message1.A→B:{{k} sk A } pk B kfresh Message2.B→A:{s} k Asusual, A → B : M meansthat A sendsto B themessage M ;{ M } sk denotes thesignatureof M withthesecretkey sk (whichcanbeverifiedwiththepublic keypk);{M} pk denotesthepublic-keyencryptionofmessageMunderthepublic keypk(whichcanbedecryptedwiththecorrespondingsecretkeysk);{M} k denotestheshared-keyencryptionofmessageMunderkeyk(whichcanbe decryptedwiththesamekeyk).Inthisprotocol,theprincipalAchoosesafresh key k ateachrunoftheprotocol.Shesignsthiskeywithhersigningkey sk A , encryptstheobtainedmessagewiththepublickeyofherinterlocutor B ,and sendshimthemessage.When B receivesit,hedecryptsit(withhissecretkey sk B ),verifiesthesignatureof A ,andobtainsthekey k .Havingverifiedthis signature, B isconvincedthatthekeywaschosenby A ,andencryptionunder pk B guaranteesthatonly B coulddecryptthemessage,so k shouldbeshared between A and B .Then, B encryptsasecret s underthesharedkey k .Only A shouldbeabletodecryptthemessageandobtainthesecrets. Ingeneral,intheliterature,asintheexampleabove,theprotocolsarede- scribedinformallybygivingthelistofmessagesthatshouldbeexchangedbe- tweentheprincipals.Nevertheless,onemustbecarefulthatthesedescriptions areonlyinformal:theyindicatewhathappensintheabsenceofanadversary. However,anadversarycancapturemessagesandsendhisownmessages,sothe sourceandthetargetofamessagemaynotbetheexpectedone.Moreover, thesedescriptionsleaveimplicittheverificationsdonebytheprincipalswhen theyreceivemessages.Sincetheadversarymaysendmessagesdifferentfrom theexpectedones,andexploittheobtainedreply,theseverificationsarevery important:theydeterminewhichmessageswillbeacceptedorrejected,and maythereforeprotectornotagainstattacks.Formalmodelsofprotocols,such as[5,7,72,117]makeallthisprecise. Althoughtheexplanationabovemayseemtojustifyitssecurityinformally, thisprotocolissubjecttoanattack: Message1.A→C:{{k} sk A } pk C Message1’.C(A)→B:{{k} sk A } pk B Message2.B→C(A):{s} k Inthisattack, A runstheprotocolwithadishonestprincipal C .Thisprincipal getsthefirstmessageoftheprotocol{{k} sk A } pk C ,decryptsitandre-encrypts itunderthepublickeyofB.Theobtainedmessage{{k} sk A } pk B corresponds exactlytothefirstmessageofasessionbetweenAandB.Then,Csendsthis messageto B impersonating A ;above,wedenoteby C ( A )thedishonestpartic- ipant C impersonating A . B replieswiththesecret s ,intendedfor A ,encrypted under k . C ,havingobtainedthekey k bythefirstmessage,candecryptthis messageandobtainthesecret s . Theprotocolcaneasilybefixed,byaddingtheidentityof B tothesigned message,whichyieldsthefollowingprotocol: