Verified interoperable implementations of security protocols

KarthikeyanBhargavan∗

C´edricFournet∗AndrewD.Gordon∗

StephenTse†

∗Microsoft

Research

Abstract

Wepresentanarchitectureandtoolsforverifyingim-plementationsofsecurityprotocols.Ourimplementations

canrunwithbothconcreteandsymbolicimplementationsofcryptographicalgorithms.Theconcreteimplementationisforproductionandinteroperabilitytesting.Thesymbolicimplementationisfordebuggingandformalverification.WedevelopourapproachforprotocolswritteninF#,adi-alectofML,andverifythembycompilationtoProVerif,aresolution-basedtheoremproverforcryptographicpro-tocols.Weestablishthecorrectnessofthiscompilationscheme,andweillustrateourapproachwithprotocolsforWebServicessecurity.

1.Introduction

Thedesignandimplementationofcodeinvolvingcryp-tographyremainsdangerouslydifficult.Theproblemistoverifythatanactiveattacker,possiblywithaccesstosomecryptographickeysbutunabletoguessothersecrets,can-notthwartsecuritygoalssuchasauthenticationandse-crecy[33];ithasmotivatedaseriousresearcheffortontheformalanalysisofcryptographicprotocols,startingwithDolevandYao[16]andeventuallyleadingtoeffectivever-ificationtools.Hence,itisnowfeasibletoverifyabstractmodelsofprotocolsagainstdemandingthreatmodels.

Still,aswithmanyformalmethods,agapremainsbe-tweenprotocolmodelsandtheirimplementations.Distill-ingacryptographicmodelisdelicateandtimeconsum-ing,sothatverifiedprotocolstendtobeshortandtoab-stractmanypotentiallytroublesomedetailsofimplementa-tioncode.Atbest,themodelanditsimplementationarere-latedduringtediousmanualcodereviews.Evenif,atsomepoint,themodelfaithfullycoversthedetailsoftheprotocol,itishardtokeepitsynchronizedwithcodeasitisdeployedandused.Hence,despiteverificationoftheabstractmodel,securityflawsmayappearinitsimplementation.

Ourthesisisthattoverifyproductioncodeofsecurityprotocolsagainstrealisticthreatmodelsisanachievablere-Toappearintheproceedingsofthe19thIEEEComputerSecurityFoundationsWork-shop(CSFW2006),July5–7,2006,Venice,Italy.󰀁

cIEEE2006.†University

ofPennsylvania

searchgoal.Thepresentpaperadvancesinthisdirection

bycontributinganewapproachtoderivingautomaticallyverifiablemodelsfromcode.Wedemonstrateitsapplica-tion,ifnottoproductioncode,atleasttocodeconstitutingaworkingreferenceimplementation—onesuitableforin-teroperabilitytestingwithefficientproductionsystemsbutitselfoptimizedforclaritynotperformance.

OurprototypetoolsanalyzecryptographicprotocolswritteninF#[39],adialectofML.F#isagoodfitforourpurposes:ithasasimpleformalsemantics;itsdatatypesof-feraconvenientwayofprogrammingoperationsonXML,importantforourmotivatingapplicationarea,webservicessecurity.Semantically,F#isnotsofarfromlanguageslikeJavaorC#,andweexpectourtechniquescouldbeadaptedtosuchlanguages.WerunF#programsontheCommonLanguageRuntime(CLR),andrelyonthe.NETFrame-worklibrariesfornetworkingandcryptographicfunctions.Thediagramabovedescribesournewlanguage-basedapproach,whichderivesverifiablemodelsfromexecutablecode.Weprefernottotackletheconverseproblem,turningaformalmodelintocode,as,thoughfeasible,itamountstolanguagedesignandimplementation,whichgenerallyisharderandtakesmoreengineeringeffortthanmodelextrac-tionfromanexistinglanguage.Besides,modernprogram-mingenvironmentsprovidebettertoolsupportforwritingcodethanforwritingmodels.

Westrivetosharemostofthecode,syntacticallyandse-mantically,betweentheimplementationanditsmodel.Ourapproachismodular,asillustratedbythediagram:wewriteapplicationcodedefiningprotocolsagainstrestrictivetypedinterfacesdefiningtheservicesexposedbytheunderlying

cryptographic,networking,andotherlibraries.Further,wewritedistinctversionsoflibrarycodeonlyforafewcorein-terfaces,suchasthosefeaturingcryptographicalgorithms.Forexample,cryptographicoperationsareonanabstracttypebytes.Weprovidedualconcreteandsymbolicimple-mentationsofeachoperation.Forinstance,theconcreteimplementationofbytesissimplyasbytearrays,subjecttoactualcryptographictransformsprovidedbythe.NETFramework.Ontheotherhand,thesymbolicimplemen-tationdefinesbytesasalgebraicexpressionssubjecttoab-stractrewritinginthestyleofDolevandYao,andassumedtobeasafeabstractionoftheconcreteimplementation.Weformalizetheactiveattackerasanarbitraryprograminoursourcelanguage,abletocallinterfacesdefinedbytheapplicationcodeandalsothelibrariesforcryptographyandnetworking.Ourverificationgoalsaretoshowsecrecyandauthenticationpropertiesinthefaceofallsuchattackers.Accordingly,wecanadaptourthreatmodelbydesigningsuitableinterfacesforthebenefitoftheattacker.Theappli-cationcodeimplementsfunctionsforeachroleinthepro-tocol,sotheattackercancreatemultipleinstancesof,say,initiatorsandresponders,aswellasmonitorandsendnet-worktrafficand,insomemodels,createnewprincipalsandcompromisesomeoftheircredentials.

Givendualimplementationsforsomelibraries,wecancompileandexecuteprogramsbothconcretelyandsymbol-ically.Thissupportsthefollowingtasks:

(1)Toobtainareferenceimplementation,weexecuteap-plicationcodeagainstconcretelibraries.Weusethereferenceimplementationforinteroperabilitytestingwithsomeotheravailable,black-boximplementation.Experimentaltestingisessentialtoconfirmthattheprotocolcodeisfunctionallycorrect,andcompleteforatleastafewbasicscenarios.(Otherwise,itissurpris-inglyeasytoendupwithamodelthatdoesnotsupportsomeproblematicfeatures.)(2)Toobtainasymbolicprototype,weexecutethesame

applicationcodeagainstsymboliclibraries.Thisal-lowsbasictestinganddebugging,especiallyfortheexpectedmessageformats.Thoughthisguaranteesneitherwireformatinteroperabilitynoranysecurityproperties,itispragmaticallyusefulduringtheinitialstagesofcodedevelopment.(3)Toperformformalverification,werunourmodelex-tractiontool,calledfs2pv,toderiveadetailedfor-malmodelfromtheapplicationcodeandsymboliclibraries.Ourmodelsareinavariantofthepical-culus[30,1]acceptedbyProVerif[13,12].ProVerifcompilesourmodelstologicalclausesandrunsares-olutionsemi-algorithmtoprovepropertiesautomati-cally.Incaseasecuritypropertyfails,ProVerifcanoftenconstructanexplicitattack[4].

2

Thefs2pv/ProVeriftoolchainisapplicableinprincipletoabroadrangeofcryptographicprotocols,butourmoti-vatingexamplesarethosebasedontheWS-Security[32]standardforsecuringSOAP[23]messagessenttoandfromXMLwebservices.WS-SecurityprescribeshowtosignandencryptpartsofSOAPmessages.WSE[28]isanimplementationofsecurityprotocolsbasedonWS-Secu-rity.PreviousanalysesofpicalculusmodelsextractedfromWSEbyhandhaveuncoveredattacks[9,10],buttherehasbeennopreviousattempttocheckconformancebetweenthesemodelsandcodeautomatically.Totesttheviabilityofournewapproach,wehavedevelopedaseriesofreferenceimplementationsofsimplewebservicesprotocols.TheyarebothtestedtobeinteroperablewithWSEandverifiedviaourtoolchain.Theresearchchallengeindevelopingtheseimplementationsistoconfrontatoncethedifficultyofprocessingstandardwireformats,suchasWS-Security,andthedifficultyofextractingverifiablemodelsfromcode.Ourmodelextractiontool,fs2pv,acceptsanexpressivefirst-ordersubsetofF#wedubF,withprimitivesforcom-municationsandconcurrency.Ithasasimpleformalse-manticsfacilitatingmodelextraction,butdisallowshigher-orderfunctionsandsomeimperativefeatures.Theapplica-tioncodeandthesymboliclibrariesmustbewithinF,buttheconcretelibrariesareinunrestrictedF#,withcallstotheplatformlibraries.Formally,wedefinetheattackertobeanarbitraryFprogramwellformedwithrespecttoare-strictiveattackerinterfaceimplementedbytheapplicationcode.Theattackercanonlyinteractwiththeapplicationcodeviathisinterface,whichissuppliedexplicitlytothemodelextractiontoolalongwiththeapplicationcode.Al-thoughwecompiletothepicalculusforverification,thepropertiesprovedcanbeunderstoodindependentlyofthepicalculus.WeprovetheoremstojustifythatverificationwithProVerifimpliespropertiesofsourceprogramsdefinedintermsofF.Theprincipaldifficultyintheproofsarisesfromrelatingtheattackermodelsatthetwolevels.

SincesecuritypropertieswithintheDolev-Yaomodelareundecidable,andwerelyonanautomaticverifier,thereiscorrectcodewithinFthatfailstoverify.Acostofourmethod,then,isthatwemustadoptaprogrammingdisci-plinewithinFsuitableforautomaticverification.Forex-ample,weavoidcertainusesofrecursion.Theinitialper-formanceresultsforourprototypetoolsareencouraging,asmuchoftheperformanceisdeterminedbytheconcreteli-braries;nonetheless,thereisatensionbetweenefficiencyofexecutionandfeasibilityofverification.Toaidthelatter,fs2pvchoosesbetweenarangeofpotentialsemanticsforeachFfunctiondefinition(basedonabstractions,rewriterules,relations,andprocesses).

Ourmethodreliesonexplicitinterfacesdescribinglow-levelcryptographicandcommunicationlibraries,andonsomeembeddedspecificationsdescribingtheintendedse-

curityproperties.Modelextractiondirectlyanalyzesap-plicationcodeusingtheseinterfacesplusthecodeofthesymboliclibraries,whileignoringthecodeoftheconcretelibraries.Hence,ourmethodcandiscoverbugsintheappli-cationcode,butnotinthetrustedconcretelibraries.

Atpresent,wehaveassessedourmethodonlyonnewcodewrittenbyourselvesinthisstyle.Manyexistingpro-tocolimplementationsrelyonwelldefinedinterfacespro-vidingcryptographicandotherservices,soweexpectourmethodwilladapttoexistingcodebases,butthisremainsfuturework.

Ingeneral,thederivationofsecuritymodelsfromcodeamountstotranslatingthesecurity-criticalpartsofthecodeandsafelyabstractingtherest.Givenanarbitraryprogram,thistaskcanhardlybeautomated—somehelpfromthepro-grammerisneeded,atleasttoasserttheintendedsecurityproperties.Furtherworkmaydiscoverhowtocomputesafeabstractionsdirectlyfromthecodeofconcretelibraries.Fornow,weclaimthebenefitofsymbolicverificationofarefer-enceimplementationisworththecostofaddingsomesecu-rityassertionsinapplicationcodeandadoptingaprogram-mingdisciplinecompatiblewithverification.

Insummary,ourmaincontributionsareasfollows:(1)Anarchitectureandlanguagesemanticstosupportex-tractionofverifiableformalmodelsfromimplementa-tioncodeofsecurityprotocols.(2)Aprototypemodelextractorfs2pvthattranslatesfrom

FtoProVerif.Thistoolisoneofthefirsttoextractverifiablemodelsfromworkingprotocolimplementa-tions.Moreover,tothebestofourknowledge,itisthefirsttoextractmodelsfromcodethatusesastan-dardmessageformat(WS-Security)andhenceinter-operateswithotherimplementations(WSE).(3)Theoremsjustifyingmodelextraction:low-levelprop-ertiesprovedbyProVerifofamodelextractedbyfs2pvimplyhigh-levelpropertiesexpressedintermsofF.(4)Referenceimplementationsofsometypicalwebser-vicessecurityprotocolsandmechanisms,bothfor-mallyverifiedandtestedforinteroperability.Ourimplementationismodular,sothatmostcodeisex-pressedinreusablelibrariesthatgiveaformalseman-ticstoinformalwebservicessecurityspecifications.Section2informallyintroducesmanyideasofthepaperinthecontextofasimplemessageauthenticationprotocol.Section3definesoursourcelanguage,F,asasubsetofF#,andformalizesourdesiredsecurityproperties.Section4outlinesourtechniquesformodelextraction,andstatesourmaintheorems.Section5summarizesourexperienceinwritingandverifyingcodeforwebservicessecurityproto-cols.Section6concludes.

3

Acompanionreport[11]providesadditionaltechnicaldetails,includingdefinitionsforthesource(F)andtarget(picalculus)languages,theformaltranslation,andallproofs.

2.ASimpleMessageAuthenticationProtocol

Weillustrateourmethodonaverysimple,adhocproto-colexample.Section5discussesmoreinvolvedexamples.TheprotocolOurexampleprotocolhastworoles,aclientthatsendsamessage,andaserverthatreceivesit.Forthesakeofsimplicity,weassumethatthereisonlyoneprinci-palAactingasaclient,andonlyoneprincipalBactingasaserver.(Furtherexamplessupportarbitrarilymanyprinci-palsineachrole.)

Ourgoalhereisthattheserverauthenticatethemes-sage,eveninthepresenceofanactiveattacker.Tothisend,werelyonapassword-basedmessageauthenticationcode(MAC).Theprotocolconsistsofasinglemessage:

A→B:HMACSHA1{nonce}[pwdA|text]|

RSAEncrypt{pkB}[nonce]|textTheclientactingforprincipalAsendsasinglemessagetexttotheserveractingforB.TheclientandservershareA’spasswordpwdA,andtheclientknowsB’spublickeypkB.Toauthenticatethemessagetext,theclientusestheone-waykeyedhashalgorithmHMAC-SHA1tobindthemes-sagewithpwdAandafreshlygeneratedvaluenonce.Sincethepasswordislikelytobeaweaksecret,thatis,asecretwithlowentropy,itmaybevulnerabletoofflinedictionaryattacksiftheMAC,themessagetext,andthenonceareallknown.Toprotectthepasswordfromsuchguessingattacks,theclientencryptsthenoncewithpkB.

ApplicationcodeGiveninterfacesCrypto,Net,andPrinsdefiningcryptographicprimitives,communicationopera-tions,andaccesstoadatabaseofprincipalidentities,ourverifiableapplicationcodeisamodulethatimplementsthefollowingtypedinterface.pkB:rsakeyclient:str→unitserver:unit→unit

ThevaluepkBisthepublicencryptionkeyfortheserver.Callingclientwithastringparametershouldsendasinglemessagetotheserver,whilecallingservercreatesanin-stanceoftheserverrolethatawaitsasinglemessage.

InF#,str→unitisthetypeoffunctionsfromthetypestr,whichisanabstracttypeofstringsdefinedbytheCryptointerface,totheemptytupletypeunit.TheCryptointerfacealsoprovidestheabstracttypersakeyofRSAkeys.

Theexportedfunctionsclientandserverrelyonthefol-lowingfunctionstomanipulatemessages.

letmacnoncepasswordtext=Crypto.hmacsha1nonce

(concat(utf8password)(utf8text))letmaketextpkpassword=letnonce=mkNonce()in(macnoncepasswordtext,

Crypto.rsaencryptpknonce,text)letverify(m,en,text)skpassword=

letnonce=Crypto.rsadecryptskeninifnot(m=macnoncepasswordtext)thenfailwith\"badMAC\"

Thefirstfunction,mac,takesthreearguments—anonce,asharedpassword,andthemessagetext—andcomputestheirjointcryptographichashusingsomeimplementationoftheHMAC-SHA1algorithmprovidedbythecrypto-graphiclibrary.AsusualindialectsofML,typesmaybeleftimplicitincode,buttheyarenonethelessverifiedbythecompiler;machastypebytes→str→str→bytes.Thefunctionsconcatandutf8providedbyCryptoperformcon-catenationofbytearraysandanencodingofstringsintobytearrays.

Thetwootherfunctionsdefinemessageprocessing,forsendersandreceivers,respectively.Functionmakecreatesamessage:itgeneratesafreshnonce,computestheMAC,andalsoencryptsthenonceunderthepublickeypkoftheintendedreceiver,usingthersaencryptalgorithm.There-sultingmessageisatriplecomprisingtheMAC,theen-cryptednonce,andthetext.Functionverifyperformstheconversesteps:itdecryptsthenonceusingtheprivatekeyskd,recomputestheMACand,iftheresultingvaluedif-fersfromthereceivedMAC,throwsanexception(usingthefailwithprimitive).

Althoughfairlyhigh-level,ourcodeincludesenoughde-tailstobeexecutable,suchasthedetailsofparticularalgo-rithms,andthenecessaryutf8conversionsfromstrings(forpasswordandtext)tobytearrays.

Inthefollowingcodedefiningprotocolroles,werelyoneventstoexpressintendedsecurityproperties.Eventsroughlycorrespondtoassertionsusedfordebuggingpur-poses,andtheyhavenoeffectontheprogramexecution.Here,wedefinetwokindsofevents,Send(text)tomarktheintenttosendamessagewithcontenttext,andAccept(text)tomarktheacceptanceoftextasgenuine.Accordingly,clientusesaprimitivefunctionlogtologaneventofthefirstkindbeforesendingthemessage,andserverlogsaneventofthesecondkindafterverifyingthemessage.Hence,ifourprotocoliscorrect,weexpecteveryAccept(text)eventtobeprecededbyamatchingSend(text)event.Suchacor-respondencebetweeneventsisacommonwayofspecifyingauthentication.

Theclientcodereliesonthenetworkaddressoftheserver,thesharedpassword,andtheserver’spublickey:

4

letaddress=S\"http://server.com/pwdmac\"letpwdA=Prins.getPassword(S\"A\")letpkB=Prins.getPublicKey(S\"B\")typeEv=Sendofstr|Acceptofstr

letclienttext=log(Send(text));

Net.sendaddress(marshall(maketextpkBpwdA))Here,thefunctiongetPasswordretrievesA’spasswordfromthepassworddatabase,andgetPublicKeyextractsB’spub-lickeyfromthelocalX.509certificatedatabase.Thefunc-tionSisdefinedbyCrypto;theexpressionS\"A\",forexam-ple,isanabstractstringrepresentingtheliteral\"A\".Thefunctionclientthenrunstheprotocolforsendingtext;itbuildsthemessage,thenusesNet.send,anetworkingfunc-tionthatpoststhemessageasanHTTPrequesttoaddress.Symmetrically,thefunctionserverattemptstoreceiveasinglemessagebyacceptingamessageandverifyingitscontent,usingB’sprivatekeyfordecryption.letskB=Prins.getPrivateKey(S\"B\")letserver()=

letm,en,text=unmarshall(Net.acceptaddress)inverify(m,en,text)skBpwdA;log(Accept(text))Thefunctionsmarshallandunmarshallserializeanddeserializethemessagetriple—theMAC,theencryptednonce,andthetext—asastring,usedhereasasimplewireformat.(Wepresentanexampleoftheresultingmessagebelow.)Thesefunctionsarealsopartoftheverifiedappli-cationcode;weomittheirdetails.

ConcreteandsymboliclibrariesTheapplicationcodelistedabovemakesuseofaCryptolibraryforcryptographicoperations,aNetlibraryfornetworkoperations,andaPrinslibraryofferingaccesstoaprincipaldatabase.TheconcreteimplementationsoftheselibrariesareF#modulescontain-ingfunctionsthatarewrappersaroundthecorrespondingplatform(.NET)cryptographicandnetworkoperations.Toobtainacompletesymbolicmodeloftheprogram,wealsodevelopsymbolicimplementationsoftheselibrariesasF#moduleswiththesameinterfaces.Thesesymbolicli-brariesarewithintherestrictedsubsetFwedefineinthenextsection,andrelyonasmallmodulePidefiningnamecreation,channel-basedcommunication,andconcurrencyinthestyleofthepicalculus.FunctionsPi.sendandPi.recvallowmessagepassingonchannels,functionsPi.nameandPi.changeneratefreshnamesandchannels,andafunctionPi.forkrunsitsfunctionargumentinparallel.ThemembersofPiareprimitiveinthesemanticsofF.ThePimoduleiscalledfromthesymboliclibrariesduringsymbolicevalu-ationandformalverification;itisnotcalleddirectlyfromapplicationcodeandplaysnopartintheconcreteimple-mentation.

moduleCrypto//concretecodeinF#openSystem.Security.Cryptographytypebytes=byte[]

typersakey=RSAofRSAParameters...

letrng=newRNGCryptoServiceProvider()letmkNonce()=

letx=Bytearray.make16inrng.GetBytesx;x...

lethmacsha1kx=

newHMACSHA1(k).ComputeHashx...

letrsa=newRSACryptoServiceProvider()letrsakeygen()=...letrsapub(RSAr)=...

letrsaencrypt(RSAr)(v:bytes)=...letrsadecrypt(RSAr)(v:bytes)=rsa.ImportParameters(r);rsa.Decrypt(v,false)

ThelistingsaboveshowthetwoimplementationsoftheCryptointerface.Theconcreteimplementationde-finesbytesasprimitivearraysofbytes,andessentiallyforwardsallcallstostandardcryptographiclibrariesofthe.NETplatform.Incontrast,thesymbolicimplemen-tationdefinesbytesasanalgebraicdatatype,withsym-bolicconstructorsandpatternmatchingforrepresentingcryptographicprimitives.Thisinternalrepresentationisaccessibleonlyinthislibraryimplementation.Forin-stance,hmacsha1isimplementedasafunctionthatbuildsanHmacSha1(k,x)term;sincenoinversefunctionispro-vided,thisabstractlydefinesaperfect,collision-freeone-wayfunction.Moreinterestingly,RSApublickeyencryp-tionsarerepresentedbyRsaEncryptterms,decomposedonlybyafunctionrsadecryptthatcanverifythatthevaliddecryptionkeyisprovidedalongwiththeencryptedterm.Similarly,theconcreteimplementationofNetcontainsfunctions,suchassendandaccept,thatcallintotheplat-form’sHTTPlibrary(System.Net.WebRequest),whereasthesymbolicimplementationofthesefunctionssimplyen-queuesanddequeuesmessagesfromasharedbufferimple-mentedwiththePimoduleasachannel.WeoutlinethesymbolicimplementationofNetbelow.moduleNet//symboliccodeinF...

lethttpchan=Pi.chan()letsendaddressmsg=

Pi.sendhttpchan(address,msg)letacceptaddress=

let(addr,msg)=Pi.recvhttpchaninifaddr=addressthenmsgelse...

5

moduleCrypto//symboliccodeinFtypebytes=

|NameofPi.name

|HmacSha1ofbytes∗bytes|RsaKeyofrsakey|RsaEncryptofrsakey∗bytes...

andrsakey=PKofbytes|SKofbytes...

letfreshbyteslabel=Name(Pi.namelabel)letmkNonce()=freshbytes\"nonce\"...

lethmacsha1kx=HmacSha1(k,x)...

letrsakeygen()=SK(freshbytes\"rsa\")letrsapub(SK(s))=PK(s)

letrsaencryptst=RsaEncrypt(s,t)

letrsadecrypt(SK(s))e=matchewith|RsaEncrypt(pke,t)whenpke=PK(s)→t|→failwith\"rsa_decryptfailed\"

Thefunctionsendaddsamessagetothechannelhttpchanandthefunctionacceptremovesamessagefromthechannel.

Inthisintroductoryexample,wehaveafixedpopula-tionoftwoprincipals,sothevaluesforA’spasswordandB’skeypaircansimplyberetrievedfromthethirdinterfacePrins:theconcreteimplementationofPrinsbindsthemtoconstants;itssymbolicimplementationbindsthemtofixednamesgeneratedbycallingPi.name.Ingeneral,aconcreteimplementationwouldretrievekeysfromtheoperatingsys-temkeystore,orprompttheuserforapassword.Thesym-bolicversionimplementsadatabaseofpasswordsandkeysusingachannelkepthiddenfromtheattacker.

Next,wedescribehowtobuildbothaconcretereferenceimplementationandasymbolicprototype,inthesenseofSection1.

ConcreteexecutionTotestthattheprotocolrunscor-rectly,weruntheF#compilerontheFapplicationcode,theconcreteF#implementationsofCrypto,Net,andPrins,togetherwiththefollowingtop-levelF#codetoobtainasingleexecutable,sayrun.Dependingonitscommandlineargument,thisexecutablerunsinclientorservermode:domatchSys.argv.(1)with

|\"client\"→client(SSys.argv.(2))|\"server\"→server()

|→printf\"Usage:runclienttxt\\n\";

printf\"or:runserver\\n\"ThelibraryfunctioncallSys.argv.(n)returnsthenthar-gumentonthecommandline.Asanexample,wecanexe-

cutethecommandrunclientHionsomemachine,executerunserveronsomeothermachinethatlistensonaddress,andobservetheprotocolruntocompletion.Thisrunoftheprotocolinvolvesourconcreteimplementationof(HTTP-based)communicationssendingandreceivingtheencodedstring“FADCIzZhW3XmgUABgRJj1KjnWy...”.

SymbolicexecutionToexperimentwiththeprotocolcodesymbolically,weruntheF#compilerontheFapplica-tioncode,thesymbolicFimplementationsofCrypto,Net,andPrins,andtheF#implementationofthePiinterface,togetherwiththefollowingtop-levelFcode,thatconve-nientlyrunsinstancesoftheclientandoftheserverwithinasingleexecutable.

doPi.fork(fun()→client(S\"Hi\"))doserver()

ThecommunicatedmessageprintsasfollowsHMACSHA1{nonce3}[pwd1|’Hi’]|

RSAEncrypt{PK(rsasecret2)}[nonce3]|’Hi’wherepwd1,rsasecret2,andnonce3arethesymbolicnamesfreshlygeneratedbythePimodule.Thismessagetracerevealsthestructureoftheabstractbytearraysinthecommunicatedmessage,andhenceismoreusefulforde-buggingthantheconcretemessagetrace.Wehavefounditusefultotestapplicationcodebysymbolicexecution(andevensymbolicdebugging)beforetestingthemconcretelyonanetwork.

ModellingtheopponentWeintroduceourlanguage-basedthreatmodelforprotocolsdevelopedinF.(Section3describestheformaldetails.)

LetSbetheFprogramthatconsistsoftheapplicationcodeplusthesymboliclibraries.TheprogramS,whichlargelyconsistsofcodesharedwiththeconcreteimplemen-tation,constitutesourformalmodeloftheprotocol.

LetObeanyFprogramthatiswellformedwithrespecttotheinterfaceexportedbytheapplicationcode(inthiscase,thevaluepkBandthefunctionsclientandserver),plustheinterfacesCryptoandNet.Bywellformed,wemeanthatOonlyusesexternalvaluesandcallsexternalfunctionsexplicitlylistedintheseinterfaces.Moreover,OcancallalltheoperationsinthePiinterface,astheseareprimitivesavailabletoallFprograms.WetaketheprogramOtorepre-sentapotentialattackerontheformalmodelSoftheproto-col,acounterparttoanactiveattackeronaconcreteimple-mentation.(TreatinganattackerasanarbitraryFprogramdevelopstheideaofanattackerbeinganarbitraryparallelprocess,asinthespicalculus[2].)

GivingOaccesstotheCryptoandNetinterfaces,butnotPrins,correspondstotheDolev-Yao[16]modelofanattackerabletoperformsymboliccryptography,and

6

monitorandsendnetworktraffic,butunabletoaccessprincipals’credentialsdirectly.Inparticular,Net.sendenablestheattackertosendanymessagetotheserverwhileNet.acceptenablestheattackertointerceptanymes-sagesenttotheserver.ThefunctionsCrypto.rsaencryptandCrypto.rsadecryptenableencryptionanddecryptionwithkeysknowntotheattacker;Crypto.rsakeygenandCrypto.mkNonceenablethegenerationoffreshkeysandnonces;Crypto.hmacsha1enablesMACcomputation.

GivingOaccesstoclientandserverallowsittocreatearbitrarilymanyinstancesofprotocolroles,whileaccesstopkBletsOencryptmessagesfortheserver.(Wecanenrichtheinterfacetogivetheopponentaccesstothesecretcre-dentialsofsomeprincipals,andtoallowthegenerationofarbitrarilymanyprincipalidentities.)SincepwdA,skB,andlogarenotincludedintheattackerinterface,theattackerhasnodirectaccesstotheprotocolsecretsandcannotlogeventsdirectly.

Formalverificationaimstoestablishsecrecyandauthen-ticationpropertiesforallprogramsSOassembledfromthegivensystemSandanyattackerprogramO.

Inparticular,themessageauthenticationpropertyofourexampleprotocolisexpressedascorrespondences[40]be-tweeneventsloggedbycodewithinS.ForallO,wewantthatineveryrunofSO,everyAccepteventisprecededbyacorrespondingSendevent.Inoursyntax(basedonthatofProVerif),weexpressthiscorrespondenceassertionas:

ev:Accept(x)⇒ev:Send(x)

FormalverificationWecancheckcorrespondencesatruntimeduringanyparticularsymbolicrunoftheprogram;themoreambitiousgoalofformalverificationistoprovethemforallpossiblerunsandattackers.Todoso,werunourmodelextractorfs2pvontheFapplicationcode,thesymbolicFimplementationsofCrypto,Net,andPrins,andtheattackerinterfaceasdescribedabove.TheresultisapicalculusscriptwithembeddedcorrespondenceassertionssuitableforverificationwithProVerif.Inthesimplestcase,Ffunctionscompiletopicalculusprocesses,whiletheat-tackerinterfacedetermineswhichnamesarepublishedtothepicalculusattacker.Forourprotocol,ProVerifimmedi-atelysucceeds.

Conversely,considerforinstanceavariantofthepro-tocolwheretheMACcomputationdoesnotactuallyde-pendonthetextofthemessage—essentiallytransformingtheMACintoasessioncookie:

letmacnoncepasswordtext=hmacsha1nonce(concat(utf8password)(utf8(S\"cookie\")))Fortheresultingscript,ProVerifautomaticallyfindsandreportsanactiveattack,wherebytheattackerinterceptstheclientmessageandsubstitutesanytextfortheclient’stextinthemessage.Experimentally,wecanconfirmtheattack

foundintheanalysis,bywritinginFaninstanceoftheattackerprogramOthatexploitsourinterface.Here,theattackmaybewritten:

dofork(fun()→client(S\"Hi\"));

let(nonce,mac,)=unmarshall(Net.acceptaddress)infork(fun()→server());

Net.sendaddress(marshall(nonce,mac,S\"Foo\"))Thiscodefirststartsaninstanceoftheclient,inter-ceptsitsmessage,startsaninstanceoftheserver,andfor-wardsanamendedmessagetoit.Experimentally,weob-servethattheattacksucceeds,bothconcretelyandsymbol-ically.Attheendofthoseruns,twoeventsSend\"Hi\"andAccept\"Foo\"havebeenemitted,andourauthenticationqueryfails.Oncetheattackisidentifiedandtheprotocolcorrected,thisattackercodemaybeaddedtothetestsuitefortheprotocol.

Inadditiontoauthentication,weverifysecrecyproper-tiesforourexampleprotocol.ViaProVerif[13],wecanquerywhetheraprotocolallowsanattackertoguessaweaksecretandthenverifytheguess—ifso,theattackercanmountanofflineguessingattack.Inthecaseofourpro-tocol,ProVerifshowsthepasswordisprotectedagainstof-flineguessingattacks.Conversely,ifweconsideravariantoftheprotocolthatpassesthenonceintheclear,wefindanattackthatcanalsobewrittenasaconcreteFprogram.

(ifethene1elsee2),equality(e1=e2),sequencing(e1;e2),andotherexpressionscanbederivedwithinthiscoresyn-tax.SyntaxofF:

x,y,zvariablea,bnamefconstructor(uncurried)󰀄function(curried)true,false,tuplenn≥0primitiveconstructorsname,send,recv,log,failwithprimitivefunctionsM,N::=valuexvariableanamef(M1,...,Mn)constructorapplicatione::=expressionMvalue󰀄M1...Mnfunctionapplicationfork(fun()→e)forkaparallelthread

i∈1..nmatchMwith(|Mi→ei)patternmatch

letx=e1ine2sequentialevaluationd::=declaration

types=(|fiofsi1∗...∗simi)i∈1..ndatatypedeclarationletx=evaluedeclarationlet󰀄x1...xn=en>0functiondeclarationS::=d1···dnsystem:listofdeclarationsAsystemSisasequenceofdeclarations.WewritethelistSas∅whenitisempty.Adatatypedeclarationintro-ducesanewtypeanditsconstructors(muchlikeauniontypewithtagsinC);thetypeexpressionss,sijareignoredinF.Avaluedeclarationletx=etriggerstheevaluationofexpressioneandbindstheresulttox.Afunctiondeclara-tionlet󰀄x1...xn=edefinesfunction󰀄withformalparam-etersx1...xnandfunctionbodye.Thesefunctionsmayberecursive.

AvalueMisavariable,aname,oraconstructorappli-cation.Anameisonlyintroducedduringevaluationbytheprimitivenametomodelthegenerationofchannels,keys,andnonces;sourceprogramscontainnofreenames.Ex-pressionsdenotepotentiallyconcurrentcomputationsthatreturnvalues.Primitivefunctionsmostlyrepresentcommu-nicationandconcurrency:name()returnsafreshlygener-atedname;sendMNsendsNonthechannelM;recvMreturnsthenextvaluereceivedonchannelM;logMlogstheeventM;failwithMrepresentsathrownexception;andfork(fun()→e)evaluateseinparallel.(WeneednotmodelexceptionhandlinginFaswerelyonexceptionsonlytorepresentfatalerrors.)If󰀄hasadeclaration,theapplication󰀄M1...MninvokesthebodyofthedeclarationwithactualparametersM1,...,Mn.AmatchMwith(|Mi→ei)i∈1..nrunseifortheleastisuchthatpatternMimatchesthevalueM;ifthepatternMicontainsvariables,theyarebound7

3.FormalizingaSubsetofF#

ThissectiondefinestheuntypedsubsetFofF#inwhichwewriteapplicationcodeandsymboliclibraries.Wedefinethesyntax,sketchthefairlystandardsemantics,anddefinesecurityproperties.Somedetailsarelefttothetechnicalreport[11].

ThelanguageFconsistsof:afirst-orderfunctionalcore;algebraicdatatypeswithpattern-matching(suchasthetypebytesinthesymbolicimplementationofCrypto);afewcon-currencyprimitivesinthestyleofthepicalculus;andasimpletype-freemodulesystemwithwhichweformalizetheattackermodelintroducedintheprevioussection.(Al-thoughwedonotrelyontypesafetyintheformaldefini-tion,FprogramscanbetypecheckedbytheF#compiler.)Inthesyntaxbelow,󰀄rangesoverfunctions(suchasfreshBytesorhmacsha1inCrypto)andfrangesoverdatatypeconstructors(suchasNameorHmacsha1inthetypebytesinCrypto).Functionsandconstructorsareeitherprimitive,orintroducedbyfunctionordatatypedeclarations.Theprimitivesincludethecommunica-tionandconcurrencyfunctionsPi.send,Pi.recv,Pi.name,Pi.forkdescribedintheprevioussection.InF,wetreatPi.chanasasynonymforPi.name;theyhavedifferenttypesbutbothcreatefreshatomicnames.Weomitthe“Pi.”prefixforbrevity.Tuple((e1,...,en)),conditional

ineibymatchingwithM.Iftherearetwoormoreoccur-rencesofavariableinapattern,matchingmustbindeachtothesamevalue.(Strictlyspeaking,F#forbidspatternswithmultipleoccurrencesofthesamevariable.Still,theeffectofanysuchpatterninFcanbehadinF#byrenamingallbutoneoftheoccurrencesandaddingoneormoreequalityconstraintsviaawhenclause.)Finally,letx=e1ine2firstevaluatese1toavalueM,thenevaluatese2{M/x},thatis,theoutcomeofsubstitutingMforeachfreeoccurrenceofxine2.

Next,wesketchtheoperationalsemanticsofFandtheideaofsafetywithrespecttoaquery.Aconfiguration,C,isamultisetofrunningsystemsandloggedevents.Weequipconfigurationswithasmall-stepreductionsemantics:C→C󰀇meansthatCcantakeonesteptoC󰀇.Mostreduc-tionsarisefromevaluationofexpressionswithinsystemsasdescribedabove.

OperationalSemanticsofF:

C::=S|eventM|(C|C󰀇)multisetofeventsandsystemsC≡C󰀇equalityuptolawsthat|isassociativeandcommutative,with∅asneutralelement.

LetC→C󰀇meanthereisacomputationstepfromCtoC󰀇.

󰀇󰀇∗󰀇LetC→∗≡CifandonlyifeitherC≡CorC→C.Weexpressauthenticationandotherpropertiesinterms

ofevent-basedqueries.Thegeneralformofaqueryisev:E⇒ev:B1∨···∨ev:Bn,whichmeansthateveryreach-ableconfigurationcontaininganeventmatchingthepat-ternEalsocontainsaneventmatchingoneoftheBipat-terns.

QueriesandSafety:

Aqueryqiswrittenev:E⇒ev:B1∨···∨ev:Bn

forvaluesE,B1,...,Bncontainingnofreenames.Letσstandforasubstitution{M1/x1,...,Mn/xn}.

LetC|=queryev:E⇒ev:B1∨···∨ev:BnifandonlyifC󰀇≡eventBiσ|C󰀇󰀇forsomei∈1..n,wheneverC≡eventEσ|C󰀇.

LetSbesafeforqifandonlyifC|=qwheneverS→∗≡C.Forexample,asystemissafeforqueryev:Accept(x)⇒ev:Send(x)fromSection2ifeveryreachableconfigurationcontainingeventAccept(M)alsocontainseventSend(M).WeintroduceinterfacesItorecordthesetofvalues,con-structors,andfunctionsimportedorexportedbyasystem.Sinceourverificationmethoddoesnotdependontypes,Finterfacesomittypestructureandtrackonlythedistinctionbetweenvalues,constructors,andfunctions,plustheari-tiesofconstructorsandfunctions.ThejudgmentI󰀊S:I󰀇meansSrefersonlytoexternalvalues,constructors,andfunctionslistedinI,andprovidesdeclarationsfortheval-ues,constructors,andfunctionslistedinI󰀇.(Ourtechnical

8

reportcontainsthesimpleinferencerulesforthisjudgment.TheserulesareanabstractionofthetypingrulesofF#forthefragmentweconsider.TheyareautomaticallyenforcedbytheF#compiler.)Interfaces:

µ::=mention

x:val|f:ctorn|󰀄:funnvalue,constructor,orfunctionI::=µ1,...,µninterface(unorderedsequence)

󰀇LetI󰀊S:ImeanSiswellformedgivenI,andexportsI󰀇.Forexample,hereistheFinterfacethatcorrespondsto

thetypedinterfaceimplementedbyapplicationcodeinSec-tion2.

pkB:val,client:fun1,server:fun1

WedefineaPriminterfacetodescribetheFprimitives,wheremisanarbitrarymaximumwidthoftuples:true:ctor0,false:ctor0,(tuplei:ctori)i∈1..m,

failwith:fun1,log:fun1,Pi.name:fun1,Pi.chan:fun1,Pi.send:fun2,Pi.recv:fun1,Pi.fork:fun1

Wedefinearobustsafetyproperty,thatis,safetyinthepresenceofanopponent.Toavoidvacuousfailures,weforbidtheopponentfromloggingevents.IfIisaninterface,anI-opponentisasystemOthatdependsonlyonIandPrim,butnotlog.

FormalThreatModel:OpponentsandRobustSafetyLetS::IpubiffPrim󰀊S:Ipub,IprivforsomeIpriv.

LetObeanI-opponentiffPrim\\log,I󰀊O:I󰀇forsomeI󰀇.LetSberobustlysafeforqandIiff

S::IandSOissafeforqforallI-opponentsO.Hence,settingaverificationproblemforasystemSes-sentiallyamountstoselectingthesubsetIpubofitsinterfacethatismadeavailabletotheopponent.

FortheexampleprotocolinSection2,letSbethesystemthatconsistsofapplicationcodeandsymboliclibraries,andletIpubbethefollowinginterface.

Net.send:fun2,Net.accept:fun1,Crypto.S:fun1,Crypto.iS:fun1,

Crypto.base:fun1,Crypto.ibase:fun1,Crypto.utf8:fun1,Crypto.iutf8:fun1,Crypto.concat:fun1,Crypto.iconcat:fun1,Crypto.concat3:fun1,Crypto.iconcat3:fun1,

Crypto.mkNonce:fun1,Crypto.mkPassword:fun1,Crypto.rsakeygen:fun1,Crypto.rsapub:fun1,Crypto.rsaencrypt:fun2,Crypto.rsadecrypt:fun2,Crypto.hmacsha1:fun2,

pkB:val,client:fun1,server:fun1

OurverificationproblemistoshowthatSisrobustlysafeforev:Accept(x)⇒ev:Send(x)andIpub.

4.MappingF#toaVerifiableModel

WetargetthescriptlanguageofProVerifforverifica-tionpurposes.ProVerifcanestablishcorrespondenceandsecrecypropertiesforprotocolsexpressedinavariantofthepicalculus,whosesyntaxandsemanticsaredetailedinourtechnicalreport.Inthiscalculus,activeattackersarerepresentedasarbitraryprocessesthatruninparal-lel,communicatewiththeprotocolonfreechannels,andperformsymboliccomputations.Givenascriptthatde-finestheprotocol,thecapabilitiesoftheattacker,andsometargetquery,ProVerifgenerateslogicalclausesthenusesaresolution-basedsemi-algorithm.WhenProVerifcom-pletessuccessfully,thescriptisrobustlysafeforthetar-getquery,thatis,thequeryholdsagainstall(picalculus)attackers;otherwise,ProVerifattemptstoreconstructanat-tacktrace.ProVerifmayalsodiverge,orfail,ascanbeexpectedsincequeryverificationinthepicalculusisnotdecidable.(ProVerifisknowntoterminateforthespecialclassoftaggedprotocols[14].However,theprotocolsinourmainapplicationareaofwebservicesrarelyfallinthisclass.)ProVerifisagoodmatchforourpurposes,asitof-fersbothgeneralsoundnesstheoremsandaneffectiveim-plementation.Pragmatically,wealsorelyonpreviouspos-itiveexperienceingeneratinglargeverificationscriptsforProVerif.Inprinciple,however,wemaybenefitfromanyotherverificationtool.

ToobtainaProVerifscript,wetranslateFprogramstopicalculusprocessesandrewriterules.TohelpProVerifsucceed,weuseaflexiblecombinationofseveraltransla-tions.TovalidateourusageofProVerif,wealsoformallyrelatearbitraryattackersinthepicalculustothoseexpress-ibleinF.

Atitscore,ourtranslationmapsfunctionstoprocessesusingtheclassiccall-by-valueencodingfromlambdacal-culustopicalculus[29].Forinstance,wemaytranslatethemacfunctiondeclarationofSection2

letmacnoncepwdtext=

Crypto.hmacsha1nonce(concat(utf8pwd)(utf8text))intotheprocess

!in(mac,(nonce,pwd,text,k));

out(k,Hmacsha1(nonce,Concat(Utf8(pwd),Utf8(text))))Thisprocessisareplicatedinputonchannelmac;eachmessageonmaccarriesthefunctionalarguments(nonce,pwd,text)aswellasacontinuationchannelk.Whenthefunctioncompletes,itsendsbackamessagethatcarriesitsresultonchannelk.Similarly,wetranslatetheserverfunctiondeclarationofSection2into:

!in(server,(arg,kR));

newkX;out(accept,(address,kX));in(kX,xml);

newkM;out(unmarshall,(xml,kM));in(kM,(m,en,text));

9

newkV;out(verify,((m,en,text),sk,pwd,kV));in(kV,());eventEv(Accept(text));out(kR,())

Thisprocessfirstcallsfunctionacceptasfollows:itgen-eratesafreshcontinuationchannelkX;itsendsamessagethatcarriestheargumentaddressandkXonchannelaccept;anditreceivesthefunctionresultxmlonchannelkX.Theprocessthensimilarlycallsthefunctionsunmarshallandverify.Ifbothcallssucceed,theprocessfinallylogstheeventAccept(text)andreturnsan(empty)resultonkR.Ourpicalculusincludesthesametermalgebra—valuesbuiltfromvariables,names,andconstructors—asF,soval-uesareunchangedbythetranslation.Moreover,ourpical-culusincludestermdestructorsdefinedbyrewriterulesonthetermalgebra,andwheneverpossibleafterinlining,ourimplementationmapssimplefunctionstodestructors.Forinstance,weactuallytranslatethemacfunctiondeclarationintothenativeProVerifreduction:

reducmac(nonce,pwd,text)=

HmacSha1(nonce,Concat(Utf8(pwd),Utf8(text)))Bothformulationsofmacareequivalent,butthelatterismoreefficient.Ontheotherhand,complexfunctionswithside-effects,recursion,ornon-determinismaretranslatedasprocesses.Ourtoolalsosupportsathirdpotentialtransla-tionformac,intoaProVerifpredicatedeclaration;predi-catesaremoreefficientthanprocessesandmoreexpressivethanreductions.OurtranslationfirstperformsaggressiveinliningofFfunctions,constantpropagation,andsimilaroptimizations.Itthengloballypicksthebestapplicableformulationforeachreachablefunction,whileeliminatingdeadcode.

Finally,thetranslationgivestothepicalculuscontextthecapabilitiesavailabletoattackersinF.Forexample,thechannelhttpchanrepresentingnetworkcommunicationisexportedtothecontextinaninitializationmessage.Moreinterestingly,everypublicfunctioncodedasaprocessismadeavailableonanexportedchannel.

Forinstance,theserverfunctionisavailabletotheat-tacker;accordingly,wegeneratetheprocess:!in(serverPUB,(arg,kR));out(server,(arg,kR))ThisenablestheattackertotriggerinstancesoftheserverusingthepublicchannelserverPUB.Conversely,theprivatechannelserverisusedonlybythetranslation,sothattheattackercannotinterceptlocalfunctioncalls.

Formally,wedefinetranslationsforexpressionse,dec-larationsd,andsystemsS.ThetranslationE[e](x,P)isaprocessthatbindsvariablextothevalueofeandthenrunsprocessP.ThetranslationsS[d](P)andS[S](P)arepro-cessesthatelaboratedandS,andthenrunprocessP.Atthetoplevel,thetranslation[S::Ipub]isaProVerifscriptthatincludesconstructordefinitionsforthedatatypesinSand

definesaprocessthatelaboratesSandthenexportsIpub.Detailsofthesetranslationsareinthetechnicalreport.Ourmaincorrectnessresultisthefollowing.Theorem1(ReflectionofRobustSafety)IfS::Ipuband[[S::Ipub]]isrobustlysafeforq,thenSisrobustlysafeforqandIpub.

Inthestatementofthetheorem,Sistheseriesofmod-ulesthatdefineoursystem;Ipubisaselectionoftheval-ues,constructors,andfunctionsdeclaredinSthataremadeavailabletotheattacker;qisourtargetsecurityquery;and[S::Ipub]istheProVerifscriptobtainedfromSandIpub.TheproofofTheorem1appearsinourtechnicalreport;itreliesonanoperationalcorrespondencebetweenreduc-tionsonFconfigurationsandreductionsinthepicalculus.Weimplementourtranslationasacommandlinetoolfs2pvthatinterceptscodeaftertheF#compilerfront-end.Thetooltakesasinputaseriesofmoduleimplemen-tationsdefiningSandmoduleinterfacesboundingtheat-tacker’scapabilities,muchlikeIpub.ThetoolreliesonthetypingdisciplineofF#(whichisstrongerthanthescopedis-ciplineofF)toenforcethatS::Ipub.Itthengeneratesthescript[S::Ipub]andrunsProVerif.IfProVerifcompletessuccessfully,itfollowsthat[S::Ipub]isrobustlysafeforq.Hence,byTheorem1,weconcludethatSisrobustlysafeforqandIpub.

Asasimpleexample,recallthesystemSanditsinter-faceIpub,asstatedattheendofSection3.Ourtoolrunssuccessfullyonthisinput,provingthatSisrobustlysafeforthequeryev:Accept(x)⇒ev:Send(x)andIpub.

somequeriesaredesignedtotesttheboundariesoftheat-tackermodelandaremeanttofailduringverification.Fi-nally,thetablegivesthesizeofthelogicalmodelgeneratedbyProVerif(thenumberoflogicalclauses)anditstotalrun-ningtimetoverifyallqueriesfortheprotocol.

Forexample,considerthesimpleauthenticationproto-colofSection2,namedPassword-basedMACinthetables;itsimplementationhas38linesofspecificcode;ProVeriftakeslessthanonesecondtoverifythemessageauthen-ticationqueryandtoverifythattheprotocolprotectsthepasswordfromguessingattacks.Avariantofourimple-mentationforthisprotocol(secondrowofTables1and2)producesthesamemessage,butismoremodularandreliesonmorerealisticlibraries;itsupportsdistributedrunsandenablestheverificationofqueriesagainstactiveattackersthatmayselectivelycorruptsomeprincipalsandgetaccesstotheirkeysandpasswords.

Asabenchmark,wewroteaprogramforthefourmes-sageOtway-Reeskeyestablishmentprotocol[34],withtwoadditionalmessagesafterkeyestablishmenttoprobethese-crecyofmessagepayloadsencryptedwiththiskey.Tocom-pleteaconcrete,distributedimplementation,wehadtocodedetailedmessageformats,leftambiguousinthedescriptionoftheprotocol.Intheprocess,weinadvertentlyenabledatypingattack,immediatelyfoundbyverification.Weex-perimentedwithaseriesof16authenticationandsecrecyqueries;theirverificationtakesafewminutes.

ALibraryforWebServicesSecurityAsalarger,morechallengingcasestudy,weimplementedandverifiedsev-eralwebservicessecurityprotocols.

WebservicesareapplicationsthatexchangeXMLmes-sagesconformingtotheSOAPstandard[23].Tosecuretheseexchanges,messagesmayincludeasecurityheader,definedintheWS-Securitystandard[32],thatcontainssig-natures,ciphertexts,andarangeofsecurityelements,suchastokensthatidentifyparticularprincipals.Hence,eachsecurewebserviceimplementsasecurityprotocolbycom-posingmechanismsdefinedinWS-Security.Previousanal-ysesofsuchWS-Securityprotocolsestablishedcorrectnesstheorems[21,9,7,25,26]anduncoveredattacks[9,10].However,theseanalysesoperatedonmodelsofprotocolsandnotontheirimplementations.Intherestofthissection,wepresentthefirstverificationresultsforthesecurityofinteroperablewebservicesimplementations.

First,wedevelopalibraryinFthatimplementsthefor-matsandmechanismsofthewebservicesmessagingandsecurityspecifications.LikeWSE[28],ourlibraryisapar-tialimplementationofthesespecifications;weselectedfea-turesbasedontheneedtointeroperatewithprotocolsim-plementedbyWSE.Ourlibraryprovidesseveralmodules:•SoapimplementstheSOAPformatsforrequests,re-sponses,andfaults,andtheirexchangeviaHTTP.10

5.VerificationofInteroperableCode

Tovalidateourapproachexperimentally,weimple-mentedaseriesofcryptographicprotocolsandverifiedtheirsecurityagainstdemandingthreatmodels.

Tables1and2summarizeourresultsfortheseprotocols.Foreachprotocol,Table1givestheprogramsizefortheimplementation(inlinesofF#code,excludinginterfacesandcodeforsharedlibraries),thenumberofmessagesex-changed,andthesizeofeachmessage,measuredbothinbytesforconcreterunsandinnumberofconstructorsforsymbolicruns.Table2concernsverification;itgivesthenumberofqueriesandthekindsofsecuritypropertiestheyexpress.Asecrecyqueryrequiresthatapassword(pwd)orkey(key)beprotected;aweak-secrecyqueryfurtherre-quiresthataweaksecret(weakpwd)beprotectedfromaguessingattack.Anauthenticationqueryrequiresthatamessagecontent(msg),itssender(sender),orthewholeexchange(session)beauthentic.Somequeriescanbeveri-fiedeveninthepresenceofattackersthatcontrolsomecor-ruptedprincipals,therebygettingaccesstotheirkeysandpasswords.Notallqueriesholdforallprotocols;infact

ProtocolPassword-basedMAC

Password-basedMACvariantOtway-Rees

WSpassword-basedsigningWSX.509signing

WSpassword-basedMACWSrequest-response

LOCs3875148858585149Implementationmessagesbytes12081238474;140;134;6813835146501620626206;3187

symbols1621

24;40;20;11

39434886;542

Table1.Summaryofexampleprotocols

ProtocolqueriesPassword-basedMAC4Password-basedMACvariant5Otway-Rees16WSpassword-basedsigning5WSX.509signing5WSpassword-basedMAC3WSrequest-response15

SecurityGoalssecrecyauthenticationweakpwdmsgpwdmsg,senderkeymsg,sendernomsg,sendernomsg,senderweakpwdmsg,sendernosession

Verificationclausestime690.8s2132.2s1551m50s4565.3s4602.6s43610.9s50344m45s

insidersnoyesyesyesyesnoyes

Table2.VerificationResults

•WsaddressingimplementstheWS-Addressing[15]headerformats,formessageroutingandcorrelation.•XmldsigandXmlencimplementthestandardsforXMLdigitalsignature[18]andXMLencryption[17],whichprovideflexibleformatsforselectivelysigningandencryptingpartsofanXMLdocument.

•WssecurityimplementstheWS-Securityheaderfor-matandcommonsecuritytokens,suchasusernametokens,encryptedkeys,andX.509certificates.ThesemodulesrelyontheCryptomoduleforcryptographicfunctionsandanewXmlmodule(withdualsymbolicandconcreteimplementations)forrawXMLmanipulation.Applicationswrittenwiththislibraryproduceandcon-sumeSOAPmessagesthatconformtothewebservicesspecifications.Suchapplicationscaninteroperatewithotherconformantwebservices,suchasthosethatuseWSE.Therequirementtoproduceconcrete,interoperable,andverifiablecodeisquitedemanding,butityieldsverypre-ciseexecutablemodelsfortheinformalWS-Securityspec-ifications,moredetailedthananyavailableintheliterature.Forverifiability,weadoptaprogrammingdisciplinethatreducestheflexibilityofmessageformatswhereverpossi-ble.Inparticular,wefixtheorderofheadersinamessageandlimitthenumberofheadersthatcanbesigned.Weavoidhigher-orderfunctions(suchasList.map)andrecur-sionoverlistsandXML,andinsteadinlinethesefunctionsbyhand.

11

Thelibraryconsistsof1200linesofFcode.Wecanquicklywritesecurityprotocolsusingthislibrary,suchasanauthenticationprotocolthatusesapasswordoranX.509certificatetogenerateanXMLdigitalsignature(protocolsWSPassword-basedsigningandWSX.509signinginTa-bles1and2).Only85additionallinesofcodeneedtobewrittentoimplementtheseprotocols;theirverificationtakesafewseconds.

ASimpleAuthenticationProtocoloverWS-SecurityAsacasestudy,weusedourwebserviceslibrarytoim-plementanexistingpassword-basedauthenticationprotocol(WSpassword-basedMAC)takenfromtheWSEsamples.TheprotocolisquitesimilartoPassword-basedMAC,ex-ceptthatthemessageisnowastandards-compliantXMLdocument.ThismessageissentasthebodyofaSOAPenvelopethatincludesaWS-Securitysecurityheaderthatcontainsausernametoken,representingtheclient’sidentity,andanX.509token,representingtheserver’sidentity.Theusernametokenincludesafreshlygeneratednonceused,alongwithasharedpassword,toderiveakeyformessageauthentication.Thisnonceisprotectedbyencryptingtheentireusernametokenwiththeserver’spublickey,usingXMLencryption.ThemessageisauthenticatedbyanXMLdigitalsignaturethatincludesacryptographickeyedhashofthebodyusingakeyderivedfromtheusernametoken.Inearlierwork[10],wewroteanon-executableformalmodelforthisprotocolandanalyzeditwithProVerif.Here,weextractthemodeldirectlyfromafull-fledgedimplemen-

tation.Moreover,weencodeamorerealisticthreatmodelthatenablestheattackertogainaccesstosomepasswordsandkeys.Inparticular,thePrinsmodulehastwoadditionalfunctionsinitsinterface:leakPasswordandleakPrivateKey.TheleakPasswordfunctionisdefinedasfollows:letleakPassword(u:str)=

letpwd=getPassworduinlogLeak(u);pwd

WhentheattackercallsleakPasswordforaprincipalu,thefunctionextractsthepasswordforufromthedatabaseandreturnsittotheattacker;butbeforeleakingthepass-word,thefunctionlogsaneventLeak(u)recordingthattheprincipaluhasbeencompromised.

Weimplementtheclientandserverrolesusingourli-brary,withslightlydifferentSendandAccepteventsfromtheonesinSection2.Toenablesenderauthentication,theclientlogsSend(u,m),whereuistheprincipalthatsendstheXMLmessagem.Similarly,onreceivingthemessage,theserverlogsAccept(u,m).Thedatatypeofeventsandtheauthenticationquerybecomes

typeEv=Sendofstr∗item

|Acceptofstr∗item|Leakofstr

q=ev:Accept(u,m)⇒ev:Send(u,m)∨ev:Leak(u)whereitemisthedatatypeofXMLelements.Thequeryqasksthattheserverauthenticatethemessagemandthesendingprincipalu,unlessuhasbeenleaked.LetWbethesystemthatconsistsoftheclientandservercode,thesymboliclibraries(Crypto,Net,Prins,andXml),andthewebserviceslibrary.LetIpubbetheinterfaceofSection3extendedwiththeitemdatatype.Usingfs2pvandProVerif,weprovethatWisrobustlysafeforqandIpub.Theveri-ficationofmessageandsenderauthenticationtakesonlyafewseconds.AswithPassword-basedMAC,wealsoprovethatthepasswordisprotectedevenifitisaweaksecret.Weexperimentallycheckedthatourconcreteimplemen-tationcomplieswiththewebservicesspecifications:wecanrunourclientwithaWSEserver,andconverselyaccessourserverfromaWSEclient.Manydetailsofourmodelwouldhavebeendifficulttodeterminefromthespecifica-tionsalone,withoutinteroperabilitytesting.Theresultingmessagesexchangedbytheconcreteexecutionarearound6kilobytesinsize,whilethesymbolicexecutionofthepro-tocolgeneratesmessageswith486symbols.TheruntimeperformanceofourconcreteimplementationiscomparabletoWSE,whichisnotsurprisingforthisprotocol,sincetheexecutiontimeisdominatedbyXMLprocessingandcom-munication.

Wealsoimplementedandverifiedanextensionoftheprotocoldescribedabove,wheretheserver,uponaccept-ingtherequestmessage,sendsbackaresponsemessagesignedwiththeprivatekeyassociatedwithitsX.509cer-tificate.Forthistwomessageprotocol,thesecuritygoals

12

areauthenticationoftherequestandtheresponse,aswellascorrelationbetweenthemessages.Correlationreliesonamechanismcalledsignatureconfirmation(describedinadraftrevisionofWS-Security),wheretheresponseechoesandsignsthepassword-basedsignaturevalueoftherequest.TheprotocolisnamedWSrequest-responseinthetables;ProVerifestablishesallourauthenticationandcorrelationgoals,buttakesalmost45minutesfortheanalysis.

Ourprotocolimplementationcanalsobeusedaspartofalargerwebapplication,whilestillbenefitingfromourresults.TheclientfunctionscanbeexportedasalibraryinvokedbyapplicationswritteninanylanguagerunningontheCLR,suchasC#orVisualBasic.Similarly,theserverfunctionscanbeembeddedinthesecuritystackofawebserverthatchecksallincomingmessagesforconformancetotheprotocolbeforehandingoverthemessagebodytoawebapplicationwritteninanylanguage.Inbothcases,assumingtheapplicationcodedoesnothaveaccesstosecretpasswordsorkeys,thesecurityresultstransparentlyapply.

6.Conclusions

Wedescribeanarchitectureandprogrammingmodelforsecurityprotocols.Forproductionuse,protocolcoderunsagainstconcretecryptographyandlow-levelnetwork-inglibraries.Forinitialdevelopment,thesamecoderunsagainstsymboliccryptographyandintra-processcommuni-cationlibraries.Forverification,muchofthecodetrans-latestoalow-levelpicalculusmodelforanalysisagainstaDolev-Yaoattacker.Theattackercanbeunderstoodandcustomizedinsource-leveltermsasanarbitraryprogramrunningagainstaninterfaceexportedbytheprotocolcode.Ourprototypeimplementationisthefirst,webelieve,toextractverifiablemodelsfromcodeimplementingstandardsecurityprotocols,andhenceabletointeroperatewithotherimplementations.Ourprototypehasmanylimitations;still,weconcludethatitsignificantlyreducesthegapbetweensymbolicmodelsofcryptographicprotocolsandtheirim-plementations.

LimitsofourmodelAsusual,formalsecurityguaranteesholdonlywithintheboundariesofthemodelbeingconsid-ered.Automatedmodelextraction,suchasours,enablestheformalverificationoflarge,detailedmodelscloselyrelatedtoimplementations.Inourexperience,suchmodelsaremorelikelytoencompasssecurityflawsthanthosefocusingonprotocolsinisolation.Independentlyofourwork,mod-ellingcanberefinedinvariousdirections.Certifiedcom-pilersandruntimeenvironmentscangivestrongguaranteesthatprogramexecutionscomplywiththeirformalseman-tics;inoursetting,theymayhelpbridgethegapbetweenthesemanticsofFandalow-levelmodelofitsnative-codeexecution,dealingforinstancewithmemorysafety.

Ourapproachalsocruciallyreliesonthesoundnessofsymboliccryptographywithregardstooneimplementa-tionofconcretecryptography,whichisfarfromobvi-ous.Pragmatically,ourmodellingofsymboliccryptog-raphyisflexibleenoughtoaccommodatemanyknownweaknessesofcryptographicalgorithms(introducingforin-stancesymboliccryptographicfunctions“fortheattackeronly”).Thereisalotofinterestingresearchonrecon-cilingsymboliccryptographywithmoreprecisecomputa-tionalmodels[3,6].Still,forthetimebeing,thesemodelsdonotsupportautomatedanalysesonthescaleneededforourprotocols.

RelatedworkTheideasofmodellingprotocolrolesasfunctionsandmodellinganactiveattackerasanarbitraryfunctionalcontextappearearlierinSumiiandPierce’sstud-iesofcryptographicprotocolswithinalambdacalculus[37,38].Unlikeourfunctionallanguage,whichhasstateandconcurrency,theircalculuscannotdirectlycapturelin-earityproperties(suchasreplaydetectionvianonces),asitsonlyimperativefeatureisnamegeneration.Severalsystems[35,31,27,36]operateinthereversedirection,andgen-eraterunnablecodefromabstractmodelsofcryptographicprotocolsinformalismssuchasstrandspaces,CAPSL,andthespicalculus.Thesesystemsneedtoaugmenttheunder-lyingformalismstoexpressimplementationdetailsthatareignoredinproofs,suchasmessagesizesanderrorhandlers.Goingfurtherinthedirectionofgrowingaformalismintoaprogramminglanguage,Guttman,Herzog,Ramsdell,andSniffen[24]proposeanewprogramminglanguageCPPLforwritingsecurityprotocols;CPPLcombinesfeaturesforcommunicationandcryptographywithatrustmanagementengineforlogically-definedauthorizationchecks.CPPLprogramscanbeverifiedusingstrandspacetechniques,al-thoughthereisnoautomaticsupportforthisatpresent.Alimitationofallofthesesystemsisthattheydonotimple-mentstandardmessageformatsandhencedonotinterop-eratewithotherimplementations.Intermsofengineeringeffort,itseemseasiertoachieveinteroperabilitybystartingfromanexistinggeneralpurposelanguagesuchasF#thanbydevelopinganewcompiler.

GiambiagiandDam[20]takeadifferentapproachtoshowingtheconformanceofimplementationtomodel.Theyneithertranslatemodeltocode,norcodetomodel.Instead,theyassumebothareprovidedbytheprogrammer,anddevelopatheorytoshowthattheinformationflowsal-lowedbytheimplementationofacryptographicprotocolarenoneotherthanthoseallowedbytheabstractmodeloftheprotocol.Theytreattheabstractprotocolasaspecifica-tionfortheimplementation,andimplicitlyassumecorrect-nessoftheabstractprotocol.

AskarovandSabelfeld[5]reportasubstantialdistributedimplementationwithintheJifsecurity-typedlanguageofa

13

cryptographicprotocolforonlinepokerwithoutatrustedthirdparty.Theirgoalistopreventsomeinsecureinforma-tionflowsbytyping.Theydonotderiveaformalmodeloftheprotocolfromtheircode.

Thereareonlyafewworksoncompilingimplemen-tationfilesforcryptographicprotocolstoformalmod-els.Bhargavan,Fournet,andGordon[8]translatethepol-icyfilesforwebservicestotheTulaFalemodellinglan-guage[10],forverificationbycompilationtoProVerif.Thistranslationcandetectprotocolerrorsinpolicysettings,butappliestoconfigurationfilesratherthanexecutablesourcecode.Othersymbolicmodelling[21,9,7,25,26]ofwebservicessecurityprotocolshasuncoveredarangeofpoten-tialattacks,buthasnoformalconnectiontosourcecode.Goubault-LarrecqandParrennes[22]arethefirsttoderiveaDolev-YaomodelfromimplementationcodewritteninC.TheirtoolCsurperformsaninterproceduralpoints-toanal-ysisonCcodetoyieldHornclausessuitableforinputtoaresolutionprover.TheydemonstrateCsuroncodeimple-mentingtheinitiatorroleoftheNeedham-Schroederpublic-keyprotocol.

Thereisalsorecentresearchonverifyingimplementa-tionsofcryptographicalgorithms,asopposedtoprotocols.Forinstance,Cryptol[19]isalanguage-basedapproachtoverifyingimplementationsofalgorithmssuchasAES.AcknowledgementsJamesMargetsonandDonSymehelpedusenormouslywithusingandadaptingtheF#com-piler.TonyHoareandDavidLangworthysuggestedim-provementstothepresentation.

References

[1]M.AbadiandC.Fournet.Mobilevalues,newnames,and

securecommunication.In28thACMSymposiumonPrin-ciplesofProgrammingLanguages(POPL’01),pages104–115,2001.

[2]M.AbadiandA.D.Gordon.Acalculusforcryptographic

protocols:Thespicalculus.InformationandComputation,148:1–70,1999.

[3]M.AbadiandP.Rogaway.Reconcilingtwoviewsofcryp-tography(thecomputationalsoundnessofformalencryp-tion).JournalofCryptology,15(2):103–127,2002.

[4]X.AllamigeonandB.Blanchet.Reconstructionofattacks

againstcryptographicprotocols.In18thIEEEComputerSe-curityFoundationsWorkshop(CSFW’05),pages140–154,2005.

[5]A.AskarovandA.Sabelfeld.Security-typedlanguagesfor

implementationofcryptographicprotocols:Acasestudy.In10thEuropeanSymposiumonResearchinComputerSecu-rity(ESORICS’05),volume3679ofLNCS,pages197–221.Springer,2005.

[6]M.Backes,B.Pfitzmann,andM.Waidner.Acomposable

cryptographiclibrarywithnestedoperations.InProceedings

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15][16]

[17][18][19][20]

[21]

[22]

[23][24]

ofthe10thACMConferenceonComputerandCommunica-tionsSecurity(CCS’03),pages220–230.ACMPress,2003.K.Bhargavan,R.Corin,C.Fournet,andA.D.Gordon.Se-curesessionsforwebservices.In2004ACMWorkshoponSecureWebServices(SWS),pages11–22,Oct.2004.

K.Bhargavan,C.Fournet,andA.D.Gordon.Verifyingpolicy-basedsecurityforwebservices.In11thACMConfer-enceonComputerandCommunicationsSecurity(CCS’04),pages268–277,Oct.2004.

K.Bhargavan,C.Fournet,andA.D.Gordon.Asemanticsforwebservicesauthentication.TheoreticalComput.Sci.,340(1):102–153,June2005.

K.Bhargavan,C.Fournet,A.D.Gordon,andR.Pucella.TulaFale:Asecuritytoolforwebservices.InInternationalSymposiumonFormalMethodsforComponentsandOb-jects(FMCO’03),volume3188ofLNCS,pages197–222.Springer,2004.

K.Bhargavan,C.Fournet,A.D.Gordon,andS.Tse.Ver-ifiedinteroperableimplementationsofsecurityprotocols.TechnicalReportMSR–TR–2006–46,MicrosoftResearch,2006.

B.Blanchet.AnefficientcryptographicprotocolverifierbasedonPrologrules.In14thIEEEComputerSecurityFoundationsWorkshop(CSFW’01),pages82–96,2001.B.Blanchet,M.Abadi,andC.Fournet.Automatedverifica-tionofselectedequivalencesforsecurityprotocols.In20thIEEESymposiumonLogicinComputerScience(LICS’05),pages331–340,2005.

B.BlanchetandA.Podelski.Verificationofcryptographicprotocols:Taggingenforcestermination.TheoreticalCom-puterScience,333(1-2):67–90,2005.

D.Box,F.Curbera,etal.WebServicesAddressing(WS-Addressing),Aug.2004.W3CMemberSubmission.

D.DolevandA.Yao.Onthesecurityofpublickeypro-tocols.IEEETransactionsonInformationTheory,IT–29(2):198–208,1983.

D.Eastlake,J.Reagle,etal.XMLEncryptionSyntaxandProcessing,2002.W3CRecommendation.

D.Eastlake,J.Reagle,D.Solo,etal.XML-SignatureSyntaxandProcessing,2002.W3CRecommendation.

GaloisConnections.CryptolReferenceManual,2005.

P.GiambiagiandM.Dam.Onthesecureimplementationofsecurityprotocols.ScienceofComputerProgramming,50:73–99,2004.

A.D.GordonandR.Pucella.Validatingawebservicesecu-rityabstractionbytyping.In2002ACMworkshoponXMLSecurity,pages18–29,2002.

J.Goubault-LarrecqandF.Parrennes.Cryptographicpro-tocolanalysisonrealCcode.In6thInternationalConfer-enceonVerification,ModelCheckingandAbstractInterpre-tation(VMCAI’05),volume3385ofLNCS,pages363–379.Springer,2005.

M.Gudginetal.SOAPVersion1.2,2003.W3CRecom-mendation.

J.D.Guttman,J.C.Herzog,J.D.Ramsdell,andB.T.Sniffen.Programmingcryptographicprotocols.InTrustedGlobalComputing(TGC’05),volume3705ofLNCS,pages116–145.Springer,2005.

[25]E.KleinerandA.W.Roscoe.Webservicessecurity:Apre-liminarystudyusingCasperandFDR.InAutomatedRea-soningforSecurityProtocolAnalysis(ARSPA04),2004.[26]E.KleinerandA.W.Roscoe.Ontherelationshipbetween

webservicessecurityandtraditionalprotocols.InMath-ematicalFoundationsofProgrammingSemantics(MFPSXXI),2005.

[27]S.Lukell,C.Veldman,andA.C.M.Hutchison.Au-tomatedattackanalysisandcodegenerationinamulti-dimensionalsecurityprotocolengineeringframework.InSouthernAfricanTelecommunicationNetworksandAppli-cationsConference(SATNAC),2003.[28]MicrosoftCorporation.WebServicesEnhancements

(WSE)2.0,2004.Athttp://msdn.microsoft.com/webservices/building/wse/default.aspx.[29]R.Milner.Functionsasprocesses.MathematicalStructures

inComputerScience,2(2):119–141,1992.

[30]R.Milner.CommunicatingandMobileSystems:theπ-Calculus.CUP,1999.

[31]F.MullerandJ.Millen.Cryptographicprotocolgenera-tionfromCAPSL.TechnicalReportSRI–CSL–01–07,SRI,2001.

[32]A.Nadalin,C.Kaler,P.Hallam-Baker,andR.Monzillo.

OASISWebServicesSecurity:SOAPMessageSecurity1.0(WS-Security2004),Mar.2004.OASISStandard200401.[33]R.NeedhamandM.Schroeder.Usingencryptionforau-thenticationinlargenetworksofcomputers.Commun.ACM,21(12):993–999,1978.

[34]D.OtwayandO.Rees.Efficientandtimelymutualauthen-tication.OperationSystemsReview,21(1):8–10,1987.

[35]A.Perrig,D.Song,andD.Phan.AGVI–automaticgenera-tion,verification,andimplementationofsecurityprotocols.In13thConferenceonComputerAidedVerification(CAV),LNCS,pages241–245.Springer,2001.

[36]D.Pozza,R.Sisto,andL.Durante.Spi2Java:automatic

cryptographicprotocolJavacodegenerationfromspicalcu-lus.In18thInternationalConferenceonAdvancedInforma-tionNetworkingandApplications(AINA2004),volume1,pages400–405,2004.

[37]E.SumiiandB.C.Pierce.Logicalrelationsforencryp-tion.In14thIEEEComputerSecurityFoundationsWork-shop(CSFW’01),pages256–269,2001.

[38]E.SumiiandB.C.Pierce.Abisimulationfordynamicseal-ing.In31stACMSymposiumonPrinciplesofProgrammingLanguages(POPL’04),pages161–172,2004.[39]D.Syme.F#,2005.Athttp://research.

microsoft.com/projects/ilx/fsharp.aspx.[40]T.WooandS.Lam.Asemanticmodelforauthentication

protocols.InIEEEComputerSocietySymposiumonRe-searchinSecurityandPrivacy,pages178–194,1993.

14