The following is an example of a memo (or email) that needs improvement.

After reading it, review the revision on the following page.

TO: Andrea Kanarek

This memo is in response to your recent inquiry about mail costs. Your message of April 30 said that you

wanted a brief explanation of what is being done in Mail Services to cut back on overall costs. I can tell

you that I have been doing many things to cut costs.

For one thing, I am trying very hard to locate duplicate names and addresses inadvertently included in

our mailing lists. This problem is particularly difficult when we merge multiple mailing lists. Another

thing I’m doing is related to envelope size. Departments that use envelopes larger that 6 ? by 11 ? are

costing us a lot of money, which they do not realize. Therefore, I am making a proposal to all

departments to limit envelope size.

Finally, I’m looking into the possibility of presorting some of our first- and third-class mail. Mailings that

are presorted are charged less.

Email message

Review the following email message. Re-word sentences or delete unnecessary words shile keeping the

original meaning.

Subject: Project Proposal

My dear Mr. Kanaga,

I was informed by telephone today by Susan Adobe, your coordinator, that you are interested in our

proposal. Needless to say I am very interested by this news. Unfortunately. I have a speaking

engagement over the next two days. I regret that I will not be able to speak with you directly. Would you

be so kind as to contact my colleague, John James, who will arrange a time for us to chat further about

these mat ters.

It will be most enjoyable to finally speak with you in person.

Best Regards,

Liz Jones

第二篇：Computer-assisted verification of a protocol for certified email

Computer-AssistedVeri?cationof

aProtocolforCerti?edEmail

Mart??nAbadi1andBrunoBlanchet2

1ComputerScienceDepartment,UniversityofCalifornia,SantaCruz

abadi@cs.ucsc.edu

2?D?epartementd’Informatique,EcoleNormaleSup?erieure,Paris

andMax-Planck-Institutf¨urInformatik,Saarbr¨ucken

Bruno.Blanchet@ens.fr

Abstract.Wepresenttheformalizationandveri?cationofarecentcryptographicprotocolforcerti?edemail.Relyingonatoolforauto-maticprotocolanalysis,weestablishthekeysecuritypropertiesoftheprotocol.Thiscasestudyexplorestheuseofgeneralcorrespondenceas-sertionsinautomaticproofs,andaimstodemonstratetheconsiderablepowerofthetoolanditsapplicabilitytonon-trivial,interestingproto-cols.

1Introduction

Agreatdealofe?orthasbeeninvestedinthedevelopmentoftechniquesforspecifyingandverifyingsecurityprotocolsinrecentyears.Thise?ortisjusti?ed,inparticular,bytheseriousnessofsecurity?awsandtherelativesimplicityofsecurityprotocols.Ithasproducedanumberofinterestingmethodsande?ectivetools.Theserangefrommathematicalframeworksformanualproofstofullyautomaticmodel-checkers.Theformerarefundamentallyconstrainedbytheunreliabilityandtime-scarcityofhumanprovers.Thelattertendtobelimitedtobasicpropertiesofsmallsystems,suchasthesecrecyofsessionkeysin?nite-statesimpli?cationsofprotocols;theymaybeviewedasusefulbutultimatelylimitedautomatictesters.Thedevelopmentofautomaticorsemi-automatictoolsthatovercometheselimitationsisanimportantproblemandthesubjectofactiveresearch.

Inpreviouswork,wehavedevelopedaprotocolchecker[1,6,7]thatcanestablishsecrecyandauthenticitypropertiesofprotocolsrepresenteddirectlyasprogramsinaminimalprogrammingnotation(anextensionofthepicalculus).Theprotocolsneednotbe?nite-state;thetoolcandealwithanunboundednumberofprotocolsessions,evenexecutedinparallel.Nevertheless,theproofsarefullyautomaticandoftenfast.

Thispaperreportsonafairlyambitiousapplicationofthistoolintheveri?-cationofarecentlypublishedprotocolforcerti?edemail[2].Theprotocolallowsasendertosendanemailmessagetoareceiver,insuchawaythatthereceivergetsthemessageifandonlyifthesenderobtainsanunforgeablereceiptforthe

message.Theprotocolisnon-trivial,partlybecauseofanumberofreal-worldconstraints.Theveri?cationyieldsassuranceaboutthesoundnessofthepro-tocol.Italsosuggestsapromisingmethodforreasoningaboutother,relatedprotocols.

Thiscasestudyaimstodemonstratetheconsiderablepowerofthetoolanditsapplicabilitytointerestingprotocols.Ithasalsoservedinguidingcertainimprovementstothetool.Speci?cally,formalizingthemainpropertiesoftheprotocolhasleadustoageneralizationofthetooltohandlealargeclassofcorrespondenceassertions[17].Thebulkoftheproofsremainsfullyautomatic;forthecodepresentedinthispaper,theautomaticproofstakeonly80msonanIntelXeon1.7GHzprocessor.Easymanualargumentsshowthatthecorre-spondenceassertionscapturetheexpectedsecurityguaranteesfortheprotocol.Becausetheprotocolisexpresseddirectlyinaprogrammingnotation,withoutlimitationto?nite-stateinstances,theneedforadditionalargumentstojustifytheprotocolrepresentationis,ifnoteliminated,drasticallyreduced.

OutlineWereviewthedescriptionofthecerti?edemailprotocolinSection2.Wealsoreviewourveri?cationtechnique,inSection3,andshowhowtoextenditsoastohandlethecorrespondenceassertionsonwhichwerelyhere.Weexplainourformalspeci?cationoftheprotocolinSection4,thenproveitssecuritypropertiesinSection5.WeconcludeinSection6,mentioningourworkontheanalysisofmoreelaboratevariantsoftheprotocol.

RelatedworkItisfairlycommontoreasoninformallyaboutsecurityprotocols,withvariousdegreesofthoroughnessandrigor.Forinstance,KrawczykgavesomeinformalargumentsaboutthepropertiesoftheSkemeprotocol(avariantofthecoreofIPsec)whenheintroducedSkeme[10].Similarly,thepresentationoftheprotocolthatwetreatinthispaperincludedinformalproofsketchesforsomeofitscentralproperties[2].Generally,suchproofsareinformative,butfarfromcompleteandfullyreliable.

Ithasbeenwidelyarguedthatformalproofsareparticularlyimportantforsecurityprotocols,becauseoftheseriousnessofsecurity?aws.Nevertheless,formalproofsforsubstantial,practicalprotocolsremainrelativelyrare.Nextwementionwhatseemtobethemostrelevantresultsinthisarea.

ThetheoremproverIsabellehasbeenusedforverifying(fragmentsof)severalsigni?cantprotocolswithaninductivemethod,inparticularKerberos[4,5],TLS(adescendantofSSL3.0)[14],andthee-commerceprotocolSET[3].Followingthesamegeneralapproach,G.BellaandC.Longoarecurrentlyworkingontheveri?cationthecerti?edemailprotocolthatwetreatinthispaper.Itwillbeinterestingtocomparede?nitionsandproofs.

MeadowshasusedtheNRLprotocolveri?erforreasoningabouttheInter-netKeyExchangeprotocol,acomponentofproposalsforIPsecurity[12].Thereasoning,althoughenlighteninginsomerespects,wasnotafullveri?cation.The?nite-statemodelcheckerMurphihasservedfortheveri?cationofSSL3.0[13]andofcontract-signingprotocols[16].Somewhatsimilarly,Mochahasbeenusedfortheveri?cationofcontract-signingprotocolswithinagame

model[11].(Contract-signingprotocolshavesomehigh-levelsimilaritiestopro-tocolsforcerti?edemail.)Largelybecauseoftoolcharacteristics,theproofsinMurphiandMocharequirenon-trivialencodingsandsimpli?cationsoftheprotocolsunderconsideration,andoftheirproperties.

Schneiderhasstudiedanon-repudiationprotocolinaCSP-basedmodel,withmanualproofs[15].Thatprotocol,whichisduetoZhouandGollmann,hascommonalitieswithprotocolsforcerti?edemail.

GordonandJe?reyhavebeendevelopingattractivetype-basedtechniquesforprovingcorrespondenceassertionsofprotocols[8,9].Todate,theyhavehadtosupportonlylimitedformsofcorrespondenceassertions,andtheyhaveincludedalimitedrepertoireofcryptographicprimitives.Intheserespects,theirsystemisinsu?cientfortheprotocolthatwetreatinthispaper,andweakerthanthetoolthatweuse.Ontheotherhand,thoselimitationsareprobablynotintrinsic.2TheProtocol

Thissectionrecallsthedescriptionoftheprotocolforcerti?edemail.Thissec-tionisself-contained,butwereferthereadertotheoriginaldescription[2]foradditionaldetailsandcontext.

Protocolsforcerti?edemailaimtoallowasender,S,tosendanemailmessagetoareceiver,R,sothatRgetsthemessageifandonlyifSgetsacorrespondingreturnreceipt.Someprotocolsadditionallyaimtoensurethecon?dentialityofthemessage.

Thisprotocol,likeseveralothers,reliesonanon-linetrustedthirdparty,TTP.Forsimplicity,thechannelsbetweenTTPandtheotherpartiesareassumedtoguaranteereliablemessagedelivery.Furthermore,thechannelbetweenRandTTPshouldprovidesecrecyandauthenticationofTTPtoR.(ThesepropertiesareneededwhenRgivesapasswordorsomeothersecrettoTTPinordertoproveitsidentity.)InpracticesuchachannelmightbeanSSLconnectionor,moregenerally,achannelprotectedwithsymmetrickeysestablishedviaasuitableprotocol.

TheprotocolsupportsseveraloptionsforauthenticatingR.Foreachemail,Spicksoneoftheoptions;thechoiceisdenotedbyauthoption.Wehavedonetheproofsforalloptions.Forthesakeofbrevity,however,weonlyshowourresultsforthemodecalledBothAuth,inwhichbothTTPandSauthenticateR.–TTPauthenticatesRusingasharedsecretRPwd—apasswordthatidenti?esRtoTTP.

–SauthenticatesRusingaquery/responsemechanism.RisgivenaqueryqbythereceiversoftwareandristheresponsethatSexpectsRtogive.

Theprotocolreliesonanumberofcryptographicprimitives.Thecorrespond-ingnotationisasfollows.E(k,m)isanencryptionofmusingkeykundersomesymmetricencryptionalgorithm.H(m)isthehashofminsomecollision-resistanthashingscheme.A(k,m)isanencryptionofmusingkeykundersomepublic-keyencryptionalgorithm.S(k,m)isasignatureofmusingkeykunderapublic-key

em=E(k,m)

hS=H(cleartext|q|r|em)

S2TTP=A(TTPEncKey,S|authoption|“givektoRforhS”)'$

TTP

4.S(TTPSigKey,“Ihavereleased??thekeyforS2TTP??...”)??3.“trykforhS”

??'$???

S???????2.S2TTP|“ownerofRPwdwantskeyforhS”1.TTP|em|authoption|cleartext|q|S2TTP

Fig.1.ProtocolsketchR&%&%signaturealgorithm.Finallym1|···|mndenotestheunambiguousconcatena-tionofthemis.

TTPhasapublickeyTTPEncKeythatScanuseforencryptingmessagesforTTP,andacorrespondingsecretkeyTTPDecKey.TTPalsohasasecretkeyTTPSigKeythatitcanuseforsigningmessagesandapublickeyTTPVerKeythatScanuseforverifyingthesesignatures.

Inthe?rststepoftheprotocol,Sencryptsitsmessageunderafreshlygen-eratedsymmetrickey,encryptsthiskeyunderTTPEncKey,andmailsthisandtheencryptedmessagetoR.ThenRforwardstheencryptedkeytoTTP.AfterauthenticatingRappropriately,TTPreleasesthekeytoR(soRcandecryptandreadthemessage)andsendsareceipttoS.Inmoredetail,theexchangeofmessagesgoesasfollows.(Figure1,adaptedfrom[2],showssomeofthisdetail.)Step1:WhenSwishestosendamessagemtoR:

1.1.Sgeneratesakeyk.Salsopicksauthoption(BothAuthinthispaper).Sknows

orgeneratesaqueryqtowhichRshouldrespondr.

1.2.Sencryptsmwithk,lettingem=E(k,m).

1.3.SthencomputeshS=H(cleartext|q|r|em).Thishashwillbothidentify

themessagetoTTPandserveforauthenticatingR.Thepartcleartextissimplyaheader.

1.4.ScomputesS2TTP=A(TTPEncKey,S|authoption|“givektoRforhS”).

1.5.SsendsMessage1:

Message1,StoR:TTP|em|authoption|cleartext|q|S2TTP

Step2:WhenRreceivesamessageoftheform:TTP|em?|authoption?|cleartext?|q?|S2TTP?:

2.1.Rreadscleartext?,decideswhetheritwantstoreadthemessagewiththe

assistanceofTTP,andcheckstheauthenticationoption(tobeBothAuth,inthispaper).IfRdecidestoproceed,itconstructsaresponser?toqueryq?,andrecallsitspasswordRPwdforTTP.

2.2.RcomputeshR=H(cleartext?|q?|r?|em?).

2.3.RsendsMessage2:

Message2,RtoTTP:S2TTP?|“ownerofRPwdwantskeyforhR”

ThismessageandthenextonearetransmittedonthesecurechannelthatlinksRandTTP.

Steps3and4:WhenTTPreceivesofamessageoftheformS2TTP??|“ownerofRPwd?wantskeyforh?R”:

3.1.TTPtriestodecryptS2TTP??usingTTPDecKey.Thecleartextshouldbeof

theformS|authoption??|“givek?toR?forh?S”.??3.2.TTPchecksthatRPwdisthepasswordforR?andthath?SequalshR.IfTTP’scheckssucceed,itproceedswithMessages3and4.

3.3.TTPsendsMessage3:

Message3,TTPtoR:“tryk?forh?R”

UponreceiptofsuchamessageRusesk?todecryptem?,obtainingm.

4.1.TTPsendsMessage4:

Message4,TTPtoS:S(TTPSigKey,“IhavereleasedthekeyforS2TTP??toR?”)

4.2.WhenSreceivesMessage4,itchecksthisreceipt.Lateron,ifSeverwants

toprovethatRhasreceivedmtoajudge,Scanprovidethismessage,em,k,cleartext,q,andr,andthejudgeshouldcheckthatthesevaluesandTTP’spublickeymatch.

3TheVeri?cationTool

Inthissectionwereviewtheveri?cationtoolthatweemployforouranalysis(see[1,6,7]forfurtherinformation).Wealsoexplainhowweextendthistool.

Thetoolrequiresexpressingprotocolsinaformallanguage,whichwedescribebelow.Thesemanticsofthislanguageisthepointofreferenceforourproofs.Thetoolissound,withrespecttothissemantics.(Soproofswiththetoolcanguaranteetheabsenceofattackscapturedinthissemantics,butnotnecessarilyofotherattacks.)Ontheotherhand,thetoolisnotcomplete;however,itissuccessfulinsubstantialproofs,aswedemonstrate.

3.1TheInputLanguage

Theveri?ertakesasinputthedescriptionofaprotocolinalittleprogramminglanguage,anextensionofthepicalculus.ThiscalculusrepresentsmessagesbytermsM,N,...,andprogramsbyprocessesP,Q,....Identi?ersarepartitionedintonames,variables,constructors,anddestructors.Weoftenusea,b,andcfornames,xforavariable,fforaconstructor,andgforadestructor.

Constructorsarefunctionsthatserveforbuildingterms.Thus,thetermsarevariables,names,andconstructorapplicationsoftheformf(M1,...,Mn).Aconstructorfofaritynisintroducedwiththedeclarationfunf/n.Ontheotherhand,destructorsdonotappearinterms,butonlymanipulatetermsinprocesses.Theyarepartialfunctionsontermsthatprocessescanapply.Theprocessletx=g(M1,...,Mn)inPelseQtriestoevaluateg(M1,...,Mn);ifthissucceeds,thenxisboundtotheresultandPisrun,elseQisrun.Moreprecisely,adestructorgofaritynisdescribedwithasetofreductionrulesoftheformg(M1,...,Mn)→MwhereM1,...,Mn,Maretermswithoutfreenames.Thesereductionrulesarespeci?edinareducdeclaration.Weextend

??,...,Mn)→M?ifandonlyifthereexistsasubstitutiontheserulesbyg(M1σandareductionruleg(M1,...,Mn)→Minthedeclarationofgsuchthat

Mi?=σMiforalli∈{1,...,n},andM?=σM.Pairingandencryptionaretypicalconstructors;projectionsanddecryptionaretypicaldestructors.Moregenerally,wecanrepresentdatastructuresandcryptographicoperationsusingconstructorsanddestructors,ascanbeseenbelowinourcodingoftheprotocolforcerti?edemail.

Theprocesscalculusincludesauxiliaryeventsthatareusefulinspecifyingsecurityproperties.Theprocessbegin(M).Pexecutestheeventbegin(M),thenP.Theprocessend(M).Pexecutestheeventend(M),thenP.Weprovesecuritypropertiesoftheform“ifacertainendeventhasbeenexecuted,thencertainbegineventshavebeenexecuted”.

Mostotherconstructsofthelanguagecomefromthepicalculus.Theinputprocessin(M,x);PinputsamessageonchannelM,thenrunsPwiththevari-ablexboundtotheinputmessage.Theoutputprocessout(M,N);PoutputsthemessageNonthechannelM,thenrunsP.Thenilprocess0doesnothing.TheprocessP|QistheparallelcompositionofPandQ.Thereplication!Prep-resentsanunboundednumberofcopiesofPinparallel.Therestrictionnewa;Pcreatesanewnamea,thenexecutesP.Theletde?nitionletx=MinPrunsPwithxboundtoM,andifM=NthenPelseQrunsPwhenMequalsN,otherwiseitrunsQ.Asusual,wemayomitanelseclausewhenitconsistsof0.Thenameaisboundintheprocessnewa;P.ThevariablexisboundinPintheprocessesin(M,x);P,letx=g(M1,...,Mn)inPelseQ,andletx=MinP.Wewritefn(P)andfv(P)forthesetsofnamesandvariablesfreeinP,respectively.Aprocessisclosedifithasnofreevariables;itmayhavefreenames.Processesthatrepresentcompleteprotocolsarealwaysclosed.

Theformalsemanticsofthislanguagecanbede?nedbyareductionrelationoncon?gurations,asexplainedintheappendix.(Thissemantics,aswellasthe

proofmethod,haveevolvedinminorwayssincepreviouspublications[7].)Areductiontraceisa?nitesequenceofreductionsteps.

Wegenerallyassumethatprocessesexecuteinthepresenceofanadversary,whichisitselfaprocessinthesamecalculus.Theadversaryneednotbepro-grammedexplicitly;weusuallyestablishresultswithrespecttoalladversaries.Weneedonlyconstraintheinitialknowledgeoftheadversary,whichwerep-resentwithasetofnamesInit,andrestricttheadversarynottouseauxiliaryevents:

De?nition1.LetInitbea?nitesetofnames.TheclosedprocessQisanInit-adversaryifandonlyiffn(Q)?InitandQdoesnotcontainbeginorendevents.

3.2TheInternalRepresentationandtheProofEngine

Givenaprotocolexpressedasaprocessintheinputlanguage,theveri?er?rsttranslatesit,automatically,intoasetofHornclauses(logicprogrammingrules).Intherules,messagesarerepresentedbypatterns,whichareexpressionssimilartotermsexceptthatnamesaarereplacedwithfunctionsa[...].Afreenameaisreplacedwiththefunctionwithoutparametera[](orsimplya),whileaboundnameisreplacedwithafunctionofinputsabovetherestrictionthatcreatesthename.Therulesarewrittenintermsoffourkindsoffacts:–

–

–

–attacker(p)meansthattheadversarymayhavethemessagep;mess(p,p?)meansthatthemessagep?maybesentonchannelp;begin(p)meansthattheeventbegin(p)mayhavebeenexecuted;end(p)meansthattheeventend(p)mayhavebeenexecuted.

Theveri?erusesaresolution-basedsolvingalgorithminordertodeterminepropertiesoftheprotocol.Speci?cally,itimplementsafunctionsolveP,Init(F)thattakesasparameterstheprotocolP,theinitialknowledgeoftheadversaryInit,andafactF,andreturnsasetofHornclauses.Thisfunction?rsttrans-latestheprotocolintoasetofHornclausesC,thensaturatesthissetusingaresolution-basedalgorithm[7,Sections4.2and4.3].Finally,thisfunctiondeter-mineswhatisderivable.Moreprecisely,letF?beaninstanceofF.LetCbbeanysetofclosedfactsbegin(p).WecanshowthatthefactF?isderivablefromC∪CbifandonlyifthereexistaclauseF1∧...∧Fn→F0insolveP,Init(F)andasubstitutionσsuchthatF?=σF0andσF1,...,σFnarederivablefromC∪Cb.Inparticular,whensolveP,Init(F)=?,noinstanceofFisderivable.OthervaluesofsolveP,Init(F)giveinformationonwhichinstancesofFarederivable,andunderwhichconditions.Inparticular,thebeginfactsinthehypothesesoftheclausesinsolveP,Init(F)indicatewhichbeginfactsmustbeinCbinordertoproveF?,thatis,whichbegineventsmustbeexecuted.

3.3Secrecy

Intheinputlanguage,wede?nesecrecyintermsofthecommunicationsofaprocessthatexecutesinparallelwithanarbitraryattacker.Thistreatmentof

secrecyisafairlydirectadaptationofourearlierone[1],withageneralizationfromfreenamestoterms.

De?nition2(Secrecy).LetPbeaclosedprocessandMatermsuchthatfn(M)?fn(P).TheprocessPpreservesthesecrecyofallinstancesofMfromInitifandonlyifforanyInit-adversaryQ,anyc∈fn(Q),andanysubstitu-tionσ,noreductiontraceofP|Qexecutesout(c,σM).

Thefollowingresultprovidesamethodforprovingsecrecyproperties:

Theorem1(Secrecy).LetPbeaclosedprocess.LetMbeatermsuchthatfn(M)?fn(P).Letpbethepatternobtainedbyreplacingnamesawithpatternsa[]inthetermM.AssumethatsolveP,Init(attacker(p))=?.ThenPpreservesthesecrecyofallinstancesofMfromInit.

Basically,thisresultsaysthatifthefactattacker(p)isnotderivablethentheadversarycannotobtainthetermMthatcorrespondstop.

3.4CorrespondenceAssertions

Asshownin[7],theveri?ercanserveforestablishingcorrespondenceasser-tions[17]oftherestrictedform“ifend(M)hasbeenexecuted,thenbegin(M)musthavebeenexecuted”.Here,weextendthistechniquesoastoprovespeci?-cationsofthemoregeneralform“ifend(N)hasbeenexecuted,thenbegin(M1),...,begin(Mn)musthavebeenexecuted”.Deemphasizingtechnicaldi?erenceswithWoo’sandLam’sde?nitions,werefertothesespeci?cationsascorrespon-denceassertions.Below,weusecorrespondenceassertionsforestablishingthatRgetsS’smessageifandonlyifSgetsacorrespondingreceipt.

Wede?nethemeaningofthesespeci?cationsasfollows:

De?nition3(Correspondence).LetPbeaclosedprocessandN,M1,...,Mlbetermssuchthatfn(N)∪fn(M1)∪...∪fn(Ml)?fn(P).TheprocessPsat-is?esthecorrespondenceassertionend(N)?begin(M1),...,begin(Ml)withrespecttoInit-adversariesifandonlyif,foranyInit-adversaryQ,foranyσde?nedonthevariablesofN,ifend(σN)isexecutedinsomereductiontraceofP|Q,thenwecanextendσsothatfork∈{1,...,l},begin(σMk)isexecutedinthistraceaswell.

AnalogouslytoTheorem1,thenexttheoremprovidesamethodforprovingthesecorrespondenceassertionswithourveri?er.

Theorem2(Correspondence).LetPbeaclosedprocessandN,M1,...,Mlbetermssuchthatfn(N)∪fn(M1)∪...∪fn(Ml)?fn(P).Letp,p1,...,plbethepatternsobtainedbyreplacingnamesawithpatternsa[]inthetermsN,M1,...,Ml,respectively.Assumethat,forallrulesRinsolveP,Init(end(p)),thereexistσ?andHsuchthatR=H∧begin(σ?p1)∧...∧begin(σ?pl)→end(σ?p).ThenPsatis?esthecorrespondenceassertionend(N)?begin(M1),...,begin(Ml)withrespecttoInit-adversaries.

Intuitively,theconditiononRmeansthat,forthefactend(σ?p)tobederivable,begin(σ?p1),...,begin(σ?pl)mustbederivable.Theconclusionofthetheoremisthecorrespondingstatementonevents:ifend(σN)hasbeenexecuted,thenbegin(σM1),...,begin(σMl)musthavebeenexecutedaswell.

4FormalizingtheProtocol

Inordertoanalyzetheprotocolforcerti?edemail,weprogramitintheveri?er’sinputlanguage,followingtheinformalspeci?cationratherclosely.Inthecodebelow,commentssuchas“Step1.1”refertocorrespondingstepsoftheinformalspeci?cation.

Thecoderepresentsthesituationinwhichallprincipalsproceedhonestly.InSection5,whenweconsidersituationsinwhichSorRareadversarialandmaythereforenotexecutethiscode,wesimplifythespeci?cationaccordingly.Inaddition,inordertospecifyandprovesecurityproperties,weaddevents(attheprogrampointsmarkedEventS,EventR,andEventTTP).

(*Public-keycryptography*)

funpk/1.funA/2.

reducdecA(y,A(pk(y),x))=x.

(*Signatures*)

funS/2.funSpk/1.

reduccheckS(Spk(y),S(y,x))=x.

reducgetS(S(y,x))=x.

(*Shared-keycryptography*)

funE/2.

reducdecE(y,E(y,x))=x.

(*Hashfunction*)

funH/1.

(*Constantstoidentifymessages*)

funGive/0.funWants/0.funTry/0.funReleased/0.

(*Constantauthenticationmodes.WeconsideronlyBothAuthhere*)funBothAuth/0.

(*FunctionfromR’spasswordtoR’sname*)

funPasswdTable/1.

(*Itisassumedthatanattackercannotrelateqandr=Reply(h,q)exceptforthehostshitcreatesitself*)

privatefunReply/2.

reducReplyOwnHost(x,q)=Reply(PasswdTable(x),q).

(*Buildamessage*)

privatefunMessage/2.

(*Secrecyassumptions*)

notTTPDecKey.notTTPSigKey.

(*Freenames(publicandprivateconstants)*)freec,cleartext,Sname,TTPname.

privatefreeTTPDecKey,TTPSigKey,RPwd.

letprocessS=

(*Theattackerchoosespossiblerecipientsofthemessage*)in(c,recipient);

(*Buildthemessagetosend*)

newmsgid;letm=Message(recipient,msgid)in(*Step1*)

newk;newq;letr=Reply(recipient,q)inletem=E(k,m)in

leths=H((cleartext,q,r,em))in

(*Step(*Step(*Step(*Step

letS2TTP=A(TTPEncKey,(Sname,BothAuth,(Give,k,recipient,hs)))in(*EventS[tobeaddedlater]*)

out(recipient,(TTPname,em,BothAuth,cleartext,q,S2TTP)));(*Step(*Step4.2*)!

in(Sname,inmess4);

let(=Released,=S2TTP,=recipient)=checkS(TTPVerKey,inmess4)in

(*Sknowsthattherecipienthasreadthemessage*)0

elseout(Sname,inmess4).

letprocessR=(*Step2*)

in(Rname,(=TTPname,em2,=BothAuth,cleartext2,q2,S2TTP2));letr2=Reply(Rname,q2)in(*Step2.1*)lethr=H((cleartext2,q2,r2,em2))in(*Step2.2*)(*EstablishthesecurechannelR-TTP*)newsecchannel;

out(ChannelToTTP,Rname);out(ChannelToTTP,secchannel);

letoutchannel=(TTPname,secchannel)inletinchannel=(Rname,secchannel)in(*EventR[tobeaddedlater]*)

out(outchannel,(S2TTP2,(Wants,RPwd,hr)));(*Step2.3*)(*Step3.3*)!

in(inchannel,(=Try,k3,=hr));letm3=decE(k3,em2)in

1.11.21.31.4

*)*)*)*)

1.5*)

(*Rhasobtainedthemessagem3=m*)

end(Rreceived(m3)).

letprocessTTP=

(*EstablishthesecurechannelR-TTP*)

in(ChannelToTTP,receivername);

in(ChannelToTTP,secchannel);

letinchannel=(TTPname,secchannel)in

letoutchannel=(receivername,secchannel)in

(*Step3*)

in(inchannel,(S2TTP3,(=Wants,RPwd3,hr3)));

let(Sname3,authoption3,(=Give,k3,R3,=hr3))=

decA(TTPDecKey,S2TTP3)in

ifR3=PasswdTable(RPwd3)then

ifR3=receivernamethen

(*EventTTP[tobeaddedlater]*)

out(outchannel,(Try,k3,hr3));

(*Step4.1*)

out(Sname3,S(TTPSigKey,(Released,S2TTP3,R3))).

process

letTTPEncKey=pk(TTPDecKey)inout(c,TTPEncKey);

letTTPVerKey=Spk(TTPSigKey)inout(c,TTPVerKey);

letRname=PasswdTable(RPwd)inout(c,Rname);

newChannelToTTP;

((!processS)|(!processR)|(!processTTP)

|(!in(c,m);out(ChannelToTTP,m)))

Thiscode?rstdeclarescryptographicprimitives.Forinstance,theconstruc-torAisthepublic-keyencryptionfunction,whichtakestwoparameters,apublickeyandacleartext,andreturnsaciphertext.Theconstructorpkcomputesapublickeyfromasecretkey.ThedestructordecAisthecorrespondingdecryp-tionfunction.FromaciphertextA(pk(y),x)andthecorrespondingsecretkeyy,itreturnsthecleartextx.HencewegivetheruledecA(y,A(pk(y),x))=x.Weassumeperfectcryptography,sothecleartextcanbeobtainedfromthecipher-textonlywhenonehasthedecryptionkey.Wede?nesignatures,shared-keyencryption,andahashfunctionanalogously.NotethattheconstructorSpkthatbuildsapublickeyforsignaturesfromasecretkeyisdi?erentfromtheconstruc-torpkthatbuildsapublickeyforencryptions.ThedestructorcheckSchecksthesignature,whilegetSreturnsthecleartextmessagewithoutcheckingthesignature.(Inparticular,theadversarymayusegetSinordertoobtainmessagecontentsfromsignedmessages.)Concatenationisrepresentedbytuples,whicharepre-declaredbydefault.Wealsodeclareanumberofconstantsthatappearinmessages.(*Step3.1*)(*Step3.2*)(*Step3.3*)

TheconstructorPasswdTablecomputesthenameofareceiverfromitspass-word.Thisconstructorrepresentsthepasswordtable(hostname,hostpassword).Sinceallhostnamesarepublicbutsomepasswordsaresecret,theadversarymustnotbeabletocomputetheappropriatepasswordfromahostname,sowede?neafunctionthatmapspasswordstohostnamesbutnottheconverse:hostname=PasswdTable(hostpassword).Oneadvantageofthisencodingisthatwecancompactlymodelsystemswithanunboundednumberofhosts.Thechallenge-responseauthenticationofRbySgoesasfollows.Screatesanarbitraryqueryq,andthereplyrtothisqueryiscomputedbytheconstructorReply,sor=Reply(h,q)wherehistherecipienthostname.BothSandRcanusetheconstructorReply.However,thisconstructorisdeclaredprivate,thatis,theadversarycannotapplyit.(Otherwise,itcouldimpersonateR.)Theadversarymustbeabletocomputerepliesforhoststhatitcreates,thatis,whenithasthepasswordofthehost.Therefore,wede?neapublicdestructorReplyOwnHostthatcomputesareplyfromthequeryandthepasswordofthehost.

TheconstructorMessagebuildsthemessagesthatSsendstoR.Weassumethatthesemessagesareinitiallysecret,sowemaketheconstructorprivate.WealsoassumethatSsendsdi?erentmessagestodi?erentrecipients,soletamessagebeafunctionoftherecipientandofamessageidenti?er.

Secrecyassumptionscorrespondtoanoptimizationofourveri?er.Thedecla-rationnotMindicatestotheveri?erthatMissecret.Theveri?ercanthenusethisinformationinordertospeedupthesolvingprocess.Attheendofsolving,theveri?erchecksthatthesecrecyassumptionisactuallytrue,sothatawrongsecrecyassumptionleadstoanerrormessagebutnottoanincorrectresult.Thedeclarationfreedeclarespublicfreenames.cisapublicchannel,cleartextistheheaderofthemessagessentbyS,andSnameandTTPnamearethenamesofSandTTP,respectively.R’snameisRname=PasswdTable(RPwd)soitnotafreename.(Itisdeclaredattheendoftheprotocol.)Thedecla-rationprivatefreedeclaresprivatefreenames(notknownbytheadversary);TTPDecKeyandTTPSigKeyareTTP’ssecretkeys,andRPwdisR’spassword.TheprocessesprocessS,processR,andprocessTTPrepresentS,R,andTTP,respectively.Theseprocessesarecomposedinthelastpartoftheprotocolspec-i?cation.ThispartcomputesTTP’spublicencryptionkeyfromitssecretkeybytheconstructorpk:TTPEncKey=pk(TTPDecKey).ThepublickeyTTPEncKeyisoutputonthepublicchannelcsothattheadversarycanhaveTTPEncKey.Weproceedsimilarlyforthekeypair(TTPSigKey,TTPVerKey).Atlast,wecomputeR’snamefromitspassword:Rname=PasswdTable(RPwd).Thisnameispublic,sowesenditonchannelc,sothattheadversarycanhaveit.Inthefollowing,weuseRnameasanabbreviationforthetermPasswdTable(RPwd).TheroleofChannelToTTPandofthelastelementoftheparallelcompositionisexplainedbelowinthedescriptionofprocessR.

TheprocessprocessS?rstreceivesthenameofthehosttowhichSisgoingtosenditsmessage,onthepublicchannelc.Thus,theadversarycanchoosethathost.ThisconservativeassumptionimpliesthatScansenditsmessagetoanyhost.ThenSbuildsthemessage:itcreatesanewmessageidmsgid,

andbuildsthemessagembycallingtheconstructorMessage.Thenitexecutesthestepsoftheprotocoldescription.Forinstance,instep1.1,itcreatesanewkeykbynewk,anewqueryqbynewq,andcomputesthecorrespondingreplyr.Instep1.4,thesentence“givektorecipientforhs”isrepresentedbyatuplecontainingtheconstantGiveandtheparametersk,recipient,andhs.Othersentencesarerepresentedanalogously.Notethat,atstep1.5,wesendthemessagetotherecipientonchannelrecipient.Inourcodingoftheprotocol,thechannelalwaysindicatesthedestinationofthemessage.Thisindicationmakesiteasiertode?nethemeaningof“amessagereachesitsdestination”,butitisonlyanindication:whenthechannelispublic,theadversarymaystillobtainthemessageorsenditsownmessagesonthechannel.Inthedestructorapplicationofstep4.2,weuseapattern-matchingconstruct:

let(=Released,=S2TTP,=recipient)=...in...

Apattern(p1,...,pn)matchesatupleofarityn,whenp1,...,pnmatchthecom-ponentsofthetuple.Apatternxmatchesanyterm,andbindsxtothisterm.Apattern=MmatchesonlythetermM.Sothedestructorapplicationofstep4.2succeedsifandonlyifinmess4=S(TTPSigKey,(Released,S2TTP,recipient)).Thesamepattern-matchingconstructisusedformessageinput.Whenthecheckofinmess4fails,theincomingmessageinmess4isreturnedonthechannelSname(bytheelseclauseofthedestructorapplication),sothatanothersessionofScangetit.Weassumethattheexecutionisfair,sothatallsessionsofSgetachancetohavethereceiptinmess4.Moreover,becauseofthereplicationatthebeginningofstep4.2,SstillwaitsforareceiptfromTTPevenafterreceivingawrongreceipt.Inanactualimplementation,Swouldstoreasetofthemessagesithassentrecentlyandforwhichithasnotyetobtainedareceipt.Whenobtain-ingareceipt,itwouldlookforthecorrespondingmessageinthisset.OurcodingrepresentsthislookupbyreturningthereceiptonSnameuntilitisconsumedbytherightsessionofS.

TheprocessprocessR?rstexecutessteps2.1and2.2,thenitestablishesasecureconnectionwithTTP.Theinformalspeci?cationdoesnotspelloutthedetailsrelatedtothisconnection,soweneedtopickthem.Severalreasonablechoicesareavailable;weexploreonehereandmentionothersinSection6.InordertoestablishtheconnectionwithTTP,RemploysanasymmetricchannelChannelToTTP(createdattheendoftheprotocoldescription)onwhichany-bodycanwritebutonlyTTPcanread.ForstartingaconnectionwithTTP,onesendsitsownnamereceivername(hereRname)andanewnamesecchannelonChannelToTTP.FurtherexchangesbetweenRandTTParethendoneonchan-nels(TTPname,secchannel)fromRtoTTPand(receivername,secchannel)fromTTPtoR.Weusepairsforchannelssoastomentionexplicitlythedestinationhostinthechannelname.OnemightseesomesimilaritywithTCPconnections,inwhichpacketscontaindestinationaddresses.Sincethenamesecchannelcre-atedbyRissecret,onlyRandTTPwillbeabletosendorreceivemessageson(TTPname,secchannel)and(receivername,secchannel),sothechannelR-TTPisindeedsecure.ThischannelprovidesauthenticationofTTP,sinceonlyTTP

canreadonChannelToTTP.AnyhostcansendmessagesonChannelToTTP,andthusstartaconnectionwithTTP.SotheauthenticationofRisnotprovidedbythechannelbutbythepasswordcheckthatTTPperforms(instep3.2).Rwritesonthatchannel,TTPreadsonit.Inordertoallowtheadversarytowriteonthatchannel,weusearelayprocess(!in(c,m);out(ChannelToTTP,m))(lastlineoftheprotocoldescription)thatgetsamessageoncandresendsitonChannelToTTP.Thus,bysendingamessageonc,theadversarycansenditonChannelToTTP.AfterestablishingtheconnectionwithTTP,Rcontinuestheexecutionofsteps2.3and3.3.Intheend,RemitstheeventRreceived(m3),tonotethatRhascorrectlyreceivedthemessagem3.Below,thiseventisusefulinthesecurityproofs.

TheprocessprocessTTP?rstestablishesasecurechannelwithamessagerecipient,asexplainedabove.Thenitexecutesstep3.Notethat,betweensteps

3.2and3.3,itchecksthatitsinterlocutorintheconnection,receivername,actu-allycorrespondstotheexpectedreceiverofthemessage,R3.Thischeckensuresthatthemessageonoutchannelgoestotheexpectedreceiverofthemessage.Finally,TTPsendsthekeyk3tothereceiverofthemessage(step3.3)andthereceipttothesender(step4.1).

5Results

Inthissectionwepresenttheproofsofthemainsecuritypropertiesoftheprotocol.Weheavilyrelyontheveri?erfortheseproofs.

5.1Secrecy

LetP0betheprocessthatrepresentstheprotocol.Theveri?ercanproveau-tomaticallythatthisprocesspreservesthesecrecyofthemessagemsentbyStoR.

Proposition1.LetInit={Sname,TTPname,c,cleartext}.TheprocessP0pre-servesthesecrecyofallinstancesofMessage(Rname,i)fromInit.

Automaticproof:Wegivetheappropriatequeryattacker(Message(Rname,i)).ThetoolcomputessolveP0,Init(attacker(Message(Rname,i)))=?.Hence,byTheorem1,theprocessP0preservesthesecrecyofMessage(Rname,i)fromInit.

?

5.2Receipt

Themaincorrectnesspropertyoftheprotocolisthefollowing:RreceivesthemessagemifandonlyifSgetsaproofthatRhasreceivedthemessage.Thisproofshouldbesuchthat,ifSgoestoajudgewithit,thejudgecande?nitelysaythatRhasreceivedthemessage.

ThispropertyholdsonlywhenthedeliveryofmessagesisguaranteedonthechannelsfromTTPtoR,fromTTPtoS,andfromStothejudge,hencethefollowingde?nition.

De?nition4.Wesaythatamessagemsentonchannelcreachesitsdestina-tionifandonlyifitiseventuallyreceivedbyaninputonchannelcintheinitialprocessP0oraprocessderivedfromP0.Iftheadversaryreceivesthemessage,itreemitsthemessageonchannelc.

Furthermore,weusethefollowingfairnesshypotheses:

–Ifin?nitelyoftenareductionstepcanbeexecuted,thenitwilleventuallybeexecuted.

–Ifamessagemissentonchannelc,andsomeinputsonchannelcreemitit,thatis,theyexecutein(c,m)...out(c,m),andsomedonotreemitmonc,thenmwilleventuallybereceivedbyaninputthatdoesnotreemitit.Althoughthisde?nitionandthesehypothesesarestatedsomewhatinformally,theycanbemadepreciseintermsofthesemanticsofthelanguage.Severalvariantsarepossible.

Thefactthatmessagesreachtheirdestinationandthefairnesshypothesescannotbetakenintoaccountbyourveri?er,soitcannotprovetherequiredpropertiesinafullyautomaticway.Still,theveri?ercanproveacorrespondenceassertionthatconstitutesthemostimportantpartoftheproof.Indeed,wehavetoshowpropertiesoftheform:ifsomeevente1hasbeenexecuted,thensomeevente2hasorwillbeexecuted.Theveri?ershowsautomaticallythecorrespondenceassertion:ife1hasbeenexecutedthensomeeventse?2havebeen

?executedbeforee1.Weshowmanuallythatiftheeventse2havebeenexecuted,

thene2willbeexecutedaftere?2.Thusthecorrespondenceassertioncapturesthedesiredsecurityproperty.Themanualproofjustconsistsinfollowingtheexecutionstepsoftheprocessaftere?2.Itismuchsimplerthanthe?rstpart,whichshouldgobackwardthroughallpossibleexecutionhistoriesleadingtoe1.Fortunately,the?rstpartisfullyautomatic.

Weusethefollowingprocesstorepresentthejudgetowhichtheinformalspeci?cationoftheprotocolalludes:

funReceived/0.freeJudgename.

letprocessJudge=

(*SmustsendTTP’scerti?cateplusotherinformation*)

in(Judgename,(certif,Sname5,k5,cleartext5,q5,r5,em5));

let(=Released,S2TTP5,Rname5)=checkS(TTPVerKey,certif)in

letm5=decE(k5,em5)in

leths5=H((cleartext5,q5,r5,em5))in

ifS2TTP5=

A(TTPEncKey,(Sname5,BothAuth,(Give,k5,Rname5,hs5)))then

(*ThejudgesaysthatRname5hasreceivedm5*)

end(JudgeSays(Received,Rname5,m5)).

Thejudgereceivesacerti?catefromS,triestocheckit,andifitsucceeds,saysthatthereceiverhasreceivedthemessage.ThisprocessisexecutedinparallelwithprocessR,processTTP,andprocessS.AttheendofprocessS,insteadofexecuting0,thesenderSsendstothejudge:

out(Judgename,(inmess4,Sname,k,cleartext,q,r,em))

Theresulttoprovedecomposesintotwopropositions,Propositions2and3.Proposition2.AssumethatthemessagesfromTTPsentonSname3andfromSsentonJudgenamereachtheirdestinations.IfRhasreceivedm,thenthejudgesaysthatRhasreceivedm.

Inthisproof,Risincludedintheadversary:RtriestogetamessagewithoutShavingthecorrespondingreceipt.SoweneednotconstrainRtofollowtheprotocol.TheprocessforRbecomes:

out(c,ChannelToTTP);out(c,RPwd)|in(c,m);end(Rreceived(m))

ThisprocessrevealsalltheinformationthatRhas.Whentheadversaryobtainssomemessagem,itcansenditonc,thusexecutetheeventend(Rreceived(m)).SinceRisincludedintheadversary,theadversarycancomputetheconstructorReply,soitsdeclarationbecomes:funReply/2.WritingP0fortheresultingpro-cessthatrepresentsthewholesystem,thepropositionbecomes,moreformally:Proposition2’.AssumethatthemessagesfromTTPsentonSname3andfromSsentonJudgenamereachtheirdestinations.LetInit={Sname,TTPname,Judgename,c,cleartext}.ForanyInit-adversaryQ,iftheeventend(Rreceived(Message(Mx,Mi)))isexecutedinareductiontraceofP0|QforsometermsMxandMi,thenend(JudgeSays(Received,Mx,Message(Mx,Mi)))isexecutedinallcontinuationsofthistrace.

AtpointEventTTP,weintroducetheeventbegin(TTPsend(Sname3,S(TTPSigKey,(Released,S2TTP3,R3)))),tonotethatTTPsendsthereceiptS(TTPSigKey,(Released,S2TTP3,R3))toS.AtpointEventS,weintroducetheeventbegin(S(Sname,k,cleartext,q,r,m)),tonotethatShasallpa-rametersneededtoobtaintheanswerfromthejudge(exceptTTP’sreceipt).Automaticpartoftheproof:Weinvokeourtoolwiththequeryend(Rreceived(Message(x,i))),todetermineunderwhichconditionsaninstanceofthecorrespondingeventmaybeexecuted.ThetoolthencomputesthesetofclausessolveP0,Init(end(Rreceived(Message(x,i))))andreturnsaruleoftheform:

begin(TTP(Sname,S(TTPSigKey,(Released,A(TTPEncKey,(Sname,BothAuth,(Give,pk,px,H((cleartext,pq,pr,E(pk,Message(px,pi))))))),px))))∧begin(Shas(Sname,pk,cleartext,pq,pr,Message(px,pi)))∧

H→end(Rreceived(Message(px,pi)))

forsomepatternspx,pk,pq,pr,pi,andsomehypothesisH.

So,byTheorem2,ifend(Rreceived(Message(Mx,Mi)))isexecutedinatraceofP0|Q,thentheevents

begin(TTPsend(Sname,certi?cate))

begin(Shas(Sname,Mk,cleartext,Mq,Mr,Message(Mx,Mi)))

areexecutedinthistraceforsometermsMk,Mq,andMr,withcerti?cate=S(TTPSigKey,(Released,A(TTPEncKey,(Sname,BothAuth,(Give,Mk,Mx,H((cleartext,Mq,Mr,E(Mk,Message(Mx,Mi))))))),Mx)).

Manualpartoftheproof:SinceTTPexecutesbegin(TTP(Sname,certi?cate))asprovedabove,itisthengoingtoexecuteout(Sname,certi?cate).Sincethismessagereachesitsdestination,itwillthenbereceivedbyaninputonSnamefromP0,thatis,bythelastinputofprocessS.Moreover,theses-sionthathasexecutedbegin(Shas(Sname,Mk,cleartext,Mq,Mr,Message(Mx,Mi)))doesnotreemitthismessage,sobythefairnesshypothesis,thismessagewillbereceivedbyasessionofSthatdoesnotreemitit.Suchasessionsuccess-fullychecksthecerti?cateandsendsittothejudgeonthechannelJudgename.Sincethismessagereachesitsdestination,itwillbereceivedbytheinputonJudgenameinprocessJudge.Thenthejudgealsocheckssuccessfullythecerti?-cate(thecheckalwayssucceedswhenS’schecksucceeds),sothejudgeexecutesend(JudgeSays(Received,Mx,Message(Mx,Mi))).?Theveri?erprovestherequiredcorrespondenceassertioninafullyautomaticway.Itisthenonlyafewlinesofprooftoobtainthedesiredsecurityproperty.Moreover,weneednotevenknowinadvancetheexactcorrespondenceassertiontoconsider:theveri?ertellsuswhichcorrespondenceassertionholdsforthegivenendevent.

TurningtotheguaranteesforR,weestablish:

Proposition3.AssumethatthemessagefromTTPsentonoutchannelreachesitsdestination.IfthejudgesaysthatRhasreceivedm,thenRhasreceivedm.Inthisproof,Sisincludedintheadversary:SmaytrytofoolthejudgeintosayingthatRhasreceivedamessageitdoesnothave.Therefore,weneednotbespeci?conhowSbehaves,sotheprocessforSissimply0.TheadversarycancomputetheconstructorReply,soitsdeclarationbecomes:funReply/2.WritingP0fortheresultingprocessthatrepresentsthewholesystem,thepropositionbecomes,moreformally:

Proposition3’.AssumethatthemessagefromTTPsentonoutchannelreachesitsdestination.LetInit={Sname,TTPname,Judgename,c,cleartext}.ForanyInit-adversaryQ,ifend(JudgeSays(Received,Rname,Mm))isexe-cutedinareductiontraceofP0|QforsometermMm,thentheeventend(Rreceived(Mm))isexecutedinallcontinuationsofthistrace.

AtpointEventR,weintroducetheeventbegin(Rhas(secchannel,em2,hr)),tonotethatRhasreceivedtheencryptedmessage.AtpointEventTTP,weintroducetheeventbegin(TTP(outchannel,(Try,k3,hr3)))tonotethatTTPsendsthekeyk3toR.

Automaticpart:Wegiveourveri?erthequeryend(JudgeSays(Received,Rname,m)).Theresultreturnedbytheveri?ershows,usingTheorem2,that,iftheeventend(JudgeSays(Received,Rname,Mm))isexecutedinareductiontraceofP0|QforsometermMm,thentheeventsbegin(Rhas(Msecchannel,E(Mk,

Mm),Mhr))andbegin(TTPsend((Rname,Msecchannel),(Try,Mk,Mhr)))areexecutedinthistraceforsometermsMk,Msecchannel,andMhr.

Manualpart:TTPisgoingtosendtheMessage3indicatedbytheeventbegin(TTPsend(...))toR.Sincethismessagereachesitsdestination,itwillbereceivedbythesessionofRthatexecutestheeventbegin(Rhas(...))mentionedabove(sincethevalueofthechannel(Rname,Msecchannel)mustmatch).Thissessionthenexecutesend(Rreceived(Mm)).?6Conclusion

Thispaperreportsontheformalspeci?cationofanon-trivial,practicalprotocolforcerti?edemail,andontheveri?cationofitsmainsecurityproperties.Mostoftheveri?cationworkisdonewithanautomaticprotocolveri?er,whichweadaptedforthepresentpurposes.Theuseofthistoolsigni?cantlyreducestheproofburden.Italsoreducestheriskofhumanerrorinproofs.Althoughthetoolitselfhasnotbeenveri?ed,webelievethatitsuseisquiteadvantageous.Wehavealsospeci?edandveri?edmoreelaboratevariantsoftheprotocol,throughsimilarmethods.(Weomitdetailsforlackofspace.)Inparticular,wehavetreatedallfourauthenticationmodes.WehavealsotreatedthreewaysofestablishingthesecurechannelbetweenRandTTP:theoneexplainedhere,onebasedonasmallpublic-keyprotocol,andonebasedonasimpli?edversionoftheSSHprotocolwithaDi?e-Hellmankeyagreement(challenginginitsownright).Forthesethreeversions,theautomaticpartsoftheproofstake2min30sonanIntelXeon1.7Ghz.Themanualpartsareassimpleastheonesshownabove.Writingthespeci?cationswasmoredelicateandinterestingthanconstructingthecorrespondingproofs.

Acknowledgments

Mart??nAbadi’sresearchwaspartlysupportedbyfacultyresearchfundsgrantedbytheUniversityofCalifornia,SantaCruz,andbytheNationalScienceFoun-dationunderGrantsCCR-0204162andCCR-0208800.

References

1.M.AbadiandB.Blanchet.Analyzingsecurityprotocolswithsecrecytypesandlogicprograms.In29thAnnualACMSIGPLAN-SIGACTSymposiumonPrin-ciplesofProgrammingLanguages(POPL’02),pages33–44,Portland,OR,Jan.2002.ACMPress.

2.M.Abadi,N.Glew,B.Horne,andB.Pinkas.Certi?edemailwithalighton-linetrustedthirdparty:Designandimplementation.In11thInternationalWorldWideWebConference(WWW’02),Honolulu,Hawaii,USA,May2002.ACMPress.

3.G.Bella,F.Massacci,andL.C.Paulson.Theveri?cationofanindustrialpaymentprotocol:TheSETpurchasephase.InV.Atluri,editor,9thACMConferenceonComputerandCommunicationsSecurity(CCS’02),pages12–20,Washington,DC,Nov.2002.ACMPress.

4.G.BellaandL.C.Paulson.UsingIsabelletoprovepropertiesoftheKerberosauthenticationsystem.InDIMACSWorkshoponDesignandFormalVeri?cationofSecurityProtocols,Piscataway,NJ,Sept.1997.

5.G.BellaandL.C.Paulson.KerberosversionIV:inductiveanalysisofthesecrecygoals.InJ.-J.Quisquateretal.,editors,ComputerSecurity-ESORICS98,vol-ume1485ofLectureNotesinComputerScience,pages361–375,Louvain-la-Neuve,Belgium,Sept.1998.SpringerVerlag.

6.B.Blanchet.Ane?cientcryptographicprotocolveri?erbasedonPrologrules.In14thIEEEComputerSecurityFoundationsWorkshop(CSFW-14),pages82–96,CapeBreton,NovaScotia,Canada,June2001.IEEEComputerSociety.

7.B.Blanchet.Fromsecrecytoauthenticityinsecurityprotocols.InM.HermenegildoandG.Puebla,editors,9thInternationalStaticAnalysisSympo-sium(SAS’02),volume2477ofLectureNotesinComputerScience,pages342–359,Madrid,Spain,Sept.2002.SpringerVerlag.

8.A.GordonandA.Je?rey.Authenticitybytypingforsecurityprotocols.In14thIEEEComputerSecurityFoundationsWorkshop(CSFW-14),pages145–159,CapeBreton,NovaScotia,Canada,June2001.IEEEComputerSociety.

9.A.GordonandA.Je?rey.Typesande?ectsforasymmetriccryptographicproto-cols.In15thIEEEComputerSecurityFoundationsWorkshop(CSFW-15),pages77–91,CapeBreton,NovaScotia,Canada,June2002.IEEEComputerSociety.

10.H.Krawczyk.SKEME:Aversatilesecurekeyexchangemechanismforinternet.In

ProceedingsoftheInternetSocietySymposiumonNetworkandDistributedSystemsSecurity(NDSS’96),SanDiego,CA,Feb.1996.Availableathttp://bilbo.isu.edu/sndss/sndss96.html.

11.S.KremerandJ.-F.Raskin.Gameanalysisofabuse-freecontractsigning.In

15thIEEEComputerSecurityFoundationsWorkshop(CSFW-15),pages206–222,CapeBreton,NovaScotia,Canada,June2002.IEEEComputerSociety.

12.C.Meadows.AnalysisoftheInternetKeyExchangeprotocolusingtheNRL

protocolanalyzer.InIEEESymposiumonSecurityandPrivacy,pages216–231,Oakland,CA,May1999.IEEEComputerSociety.

13.J.C.Mitchell,V.Shmatikov,andU.Stern.Finite-stateanalysisofSSL3.0.In

7thUSENIXSecuritySymposium,pages201–216,SanAntonio,TX,Jan.1998.

14.L.C.Paulson.InductiveanalysisoftheInternetprotocolTLS.ACMTransactions

onInformationandSystemSecurity,2(3):332–351,Aug.1999.

15.S.Schneider.Formalanalysisofanon-repudiationprotocol.In11thIEEECom-

puterSecurityFoundationsWorkshop(CSFW-11),pages54–65,Rockport,Mas-sachusetts,June1998.IEEEComputerSociety.

16.V.ShmatikovandJ.C.Mitchell.Finite-stateanalysisoftwocontractsigning

protocols.TheoreticalComputerScience,283(2):419–450,June2002.

17.T.Y.C.WooandS.S.Lam.Asemanticmodelforauthenticationprotocols.

In1993IEEESymposiumonResearchonSecurityandPrivacy,pages178–194,Oakland,CA,1993.IEEEComputerSociety.

Appendix:Semantics

Asemanticcon?gurationisapairE,PwheretheenvironmentEisa?nitesetofnamesandPisa?nitemultisetofclosedprocesses.TheenvironmentEmustcontainatleastallfreenamesofprocessesinP.Thecon?guration{a1,...,an},{P1,...,Pn}correspondstotheprocessnewa1;...newan;(P1|

...|Pn).Thesemanticsofthecalculusisde?nedbyareductionrelation→onsemanticcon?gurationsasfollows:

E,P

E,P

E,P

E,P∪{0}→E,P(RedNil)∪{!P}→E,P∪{P,!P}(RedRepl)∪{P|Q}→E,P∪{P,Q}(RedPar)∪{newa;P}→E∪{a?},P∪{P{a?/a}}(RedRes)

wherea?∈/E.

E,P∪{out(N,M).Q,in(N,x).P}→E,P∪{Q,P{M/x}}(RedI/O)E,P∪{letx=g(M1,...,Mn)inPelseQ}→E,P∪{P{M?/x}}

ifg(M1,...,Mn)→M?(RedDestr1)E,P∪{letx=g(M1,...,Mn)inPelseQ}→E,P∪{Q}(RedDestr2)

ifthereexistsnoM?suchthatg(M1,...,Mn)→M?

E,P∪{letx=MinP}→E,P∪{P{M/x}}(RedLet)E,P∪{ifM=MthenPelseQ}→E,P∪{P}(RedCond1)E,P∪{ifM=NthenPelseQ}→E,P∪{Q}(RedCond2)

ifM=N

E,P∪{begin(M).P}→E,P∪{P}(RedBegin)E,P∪{end(M).P}→E,P∪{P}(RedEnd)AreductiontraceTofaclosedprocessPisa?nitesequenceofreductionsfn(P),{P}→...→E?,P?.

Theoutputout(M,N)isexecutedinatraceTifandonlyifthistracecontainsareductionE,P∪{out(N,M).Q,in(N,x).P}→E,P∪{Q,P{M/x}}forsomeE,P,x,P,Q.

Theeventbegin(M)isexecutedinatraceTifandonlyifthistracecontainsareductionE,P∪{begin(M).P}→E,P∪{P}forsomeE,P,P.

Theeventend(M)isexecutedinatraceTifandonlyifthistracecontainsareductionE,P∪{end(M).P}→E,P∪{P}forsomeE,P,P.