Table Of Content

(cid:3)y Interpreting Strands in Linear Logic I. Cervesato N. Durgin M. Kanovich, A. Scedrov ITT Industries Stanford University Universityof Pennsylvania [email protected] [email protected] fmaxkanov,[email protected] Abstract One recent setting for stating the basic assumptions of the Dolev-Yao model is given by strand spaces [13, 14, 39]. The adoption of the Dolev-Yao model, an abstraction of se- Roughly, a strand is a linearly ordered sequence of events curity protocols that supports symbolic reasoning, is respon- that represents the actions of a protocol participant. A sible for many successes in protocol analysis. In particular, strand space is a collection of strands, equipped with a it has enabled using logic e(cid:11)ectively to reason about pro- graphstructuregeneratedbycausalinteractionamongpar- tocols. One recent framework for expressing the basic as- ticipants. This is closely related to Lamport’s notion of sumptions oftheDolev-Yao modelisgivenbystrand spaces, causalityindistributedsystems[21], andaclearinstanceof certain directed graphs whose structure re(cid:13)ects causal inter- Mazurkiewicz’s de(cid:12)nition of trace within concurrency the- actions among protocol participants. We represent strand ory [31]. Prior to a run of the protocol, each principal constructions asrelativelysimpleformulasin(cid:12)rst-order lin- chooses certain data to be used in the protocol, such as ear logic, a re(cid:12)nement of traditional logic known for an in- keysor nonces. trinsic and natural accounting of process states, events, and In contrast, a formal de(cid:12)nition of the Dolev-Yao model resources. The proposed encoding is shown to be sound and intermsofmultisetrewritingwithexistentialquanti(cid:12)cation, complete. Interestingly, this encoding di(cid:11)ers from the mul- MSR[6,7,12],allowsnewvaluessuchaskeysandnoncesto tiset rewriting de(cid:12)nition of the Dolev-Yao model, which is be chosen at any time during the protocol run, as the need also based onlinearlogic. Thisraises thepossibilitythat the for new choices arises. In this formalism, a way of choos- multiset rewriting framework may di(cid:11)er from strand spaces ing new values is provided by the proof rules of existential in some subtle way, although the two settings are known to quanti(cid:12)cation. The MSR formalism has been incorporated agree on the basic secrecy property. into a high-level speci(cid:12)cation language for authentication protocols, CAPSL[10]. 1 Introduction In [7], we established a substantial equivalence of the MSR and strand space formalisms. We introduced a suit- In recent years, a variety of methods have been developed able abstraction of strand con(cid:12)gurations that corresponds for analyzing andreasoning about protocols based oncryp- to MSR states, and showed that related pairs of states and tographic primitives. Although there are many di(cid:11)erences con(cid:12)gurations are equi-reachable. This is relevant for se- amongtheseproposals, mostcurrentformalapproachesuse curity analysis because several basic properties of security the so-called \Dolev-Yao" model of adversary capabilities, protocols(e.g.secrecy)canbephrasedasreachabilityprob- whichappearstobedrawnfrompositions takenin[34]and lems. However, itis notclear thatall relevantproperties of from a simpli(cid:12)ed model presented in [11]. In this idealized security protocols can be phrased in terms of reachability. setting, a protocol adversary is allowed to nondeterministi- Thus a more re(cid:12)ned analysis of the MSR and strand space callychooseamongpossibleactions. Messagesarecomposed formalismsmightrevealthedi(cid:11)erencesbetweenthetwofor- of indivisible abstract values,notsequencesof bits, anden- malismsinregardtosomesubtlepropertiesofprotocols. In cryptionismodeledinanidealizedway. Theadversarymay this paper, which may be seen as a companion to [7], we only sendmessages comprised of datait \knows" as there- providesome preliminarysteps inthis direction. sult of overhearing pasttransmissions. TheMSRandstrandspaceformalismsareanalyzedhere The Dolev-Yao abstraction makes symbolic reasoning in the formal setting of linear logic [16], a re(cid:12)nement of aboutcrypto-protocols aviableapproach. Thisobservation modallogicwithanintrinsicandnaturalaccountingofpro- hasmaterializedinanumberofsuccessfulanalysesthatuse cess states and events. The choice of linear logic is natu- model checking [29, 33, 38] and on several proposals based ral because of the very close connection between multiset onlogic,thequintessentialtoolofsymbolicreasoning[4,35]. rewriting and simple fragments of linear logic, which has been studied extensively [3, 30, 15, 19, 5]. We extend this (cid:3) Partially supported by DoD MURI \Semantic Consistency in standard correspondence to include (cid:12)rst-order parameters Information Exchange" as ONR Grant N00014-97-1-0505, by NSF GrantsCCR-9509931,CCR-9629754andCCR-9800785,andbyNRL andexistentially quanti(cid:12)edvariables. undercontractN0014-96-D2024 tovariousauthors. On the other hand, we also formally represent strand y Wewould liketothankJohnMitchell,PatrickLincoln,Cather- constructionsasrelativelysimpleformulasin(cid:12)rst-orderlin- ineMeadowsandSylvanPinskyforthefruitfuldiscussionsthatcon- ear logic. This encoding is also shown to be sound and tributedtothiswork. complete. As in our previous work on multiset rewriting 1 Report Documentation Page Form Approved OMB No. 0704-0188 Public reporting burden for the collection of information is estimated to average 1 hour per response, including the time for reviewing instructions, searching existing data sources, gathering and maintaining the data needed, and completing and reviewing the collection of information. Send comments regarding this burden estimate or any other aspect of this collection of information, including suggestions for reducing this burden, to Washington Headquarters Services, Directorate for Information Operations and Reports, 1215 Jefferson Davis Highway, Suite 1204, Arlington VA 22202-4302. Respondents should be aware that notwithstanding any other provision of law, no person shall be subject to a penalty for failing to comply with a collection of information if it does not display a currently valid OMB control number. 1. REPORT DATE 3. DATES COVERED 2000 2. REPORT TYPE 00-00-2000 to 00-00-2000 4. TITLE AND SUBTITLE 5a. CONTRACT NUMBER Interpreting Strands in Linear Logic 5b. GRANT NUMBER 5c. PROGRAM ELEMENT NUMBER 6. AUTHOR(S) 5d. PROJECT NUMBER 5e. TASK NUMBER 5f. WORK UNIT NUMBER 7. PERFORMING ORGANIZATION NAME(S) AND ADDRESS(ES) 8. PERFORMING ORGANIZATION ITT Industries,4 West Red Oak Lane,White Plains,NY,10604 REPORT NUMBER 9. SPONSORING/MONITORING AGENCY NAME(S) AND ADDRESS(ES) 10. SPONSOR/MONITOR’S ACRONYM(S) 11. SPONSOR/MONITOR’S REPORT NUMBER(S) 12. DISTRIBUTION/AVAILABILITY STATEMENT Approved for public release; distribution unlimited 13. SUPPLEMENTARY NOTES The original document contains color images. 14. ABSTRACT 15. SUBJECT TERMS 16. SECURITY CLASSIFICATION OF: 17. LIMITATION OF 18. NUMBER 19a. NAME OF ABSTRACT OF PAGES RESPONSIBLE PERSON a. REPORT b. ABSTRACT c. THIS PAGE 12 unclassified unclassified unclassified Standard Form 298 (Rev. 8-98) Prescribed by ANSI Std Z39-18 speci(cid:12)cations of securityprotocols [6,7, 12],theproofrules (=) [ (cid:0)!) is acyclic [7]. In terms of protocols, the (cid:12)rst ofexistentialquanti(cid:12)cationprovidedawayofchoosingnew threeconstraintsimplythatamessageissenttoatmostone values, such as nonces or keys. However, the linear logic recipient at a time, no message is received from more than interpretation introduced here maintains the strand space one sender, and every received message has been sent, re- intuition that nonces are chosen before the protocol is run. spectively. Dangling positive nodes correspond to messages Letusnotethatthisencodingdi(cid:11)ersfromthestandardlin- in transit. Therefore, a bundlerepresents a snapshot of the ear logic representation of multiset rewriting. This raises execution of a protocol. the possibility that the multiset rewriting framework may di(cid:11)er fromstrand spaces in somesubtle way. Linear logic has found applications in numerous areas (cid:26)(~x;~n): ~nfresh, (cid:25)(~x) > of Computer Science, and it has concrete prospects of in- (cid:13)uencing the (cid:12)eld of security protocol analysis in a sim- ww ilar way. As a speci(cid:12)cation language, linear logic has (cid:6)m1(cid:127)(~x;~n) been used to provide elegant and e(cid:11)ective representations w of many systems that share characteristics with crypto- w protocols[8,9,17,18]. Thenaturalembeddingofconcurrent (cid:6)m2(cid:127)(~x;~n) systems in linear logic [15, 20], in particular in its graph- .. . based presentations [16], is also likely to be relevant, given the interpretation of security protocols as concurrent sys- (cid:6)mj(cid:26)j(cid:0)1(~x;~n) tems [1, 40]. Work on meta-reasoning in linear logic [32] w promises to address protocol correctness [4, 35] e(cid:11)ectively (cid:6)mj(cid:26)w(cid:127)j(~x;~n) and e(cid:14)ciently. Finally, some of the theoretical results lin- earlogic hasbroughtabout(e.g.complexityissues[23])are w w expectedtoyieldabetterunderstandingofthemostfunda- (cid:127)? mentalaspects of security protocols [12]. This paper is organized as follows: Section 2 recalls the notionofstrandandreachabilitybetweenstrandcon(cid:12)gura- Figure 1: AParametric Strand tions; Section 3 provides some background on linear logic; Section 4 describes the translation of strand constructions Wenowbuildontheseacceptedde(cid:12)nitionsandpresenta into linear logic, while inSection 5we provesoundnessand strand-basedlanguageforthespeci(cid:12)cationof protocols and completeness theorems that relate strand reachability and oftheirexecution. Theinterestedreadermayconsult[7]for linear logic derivability for their translation. In Section 6, further details. wecomparetheseresultswiththetranslationofthemultiset Data such as the identity of principals and their long- rewritingspeci(cid:12)cationsofasecurityprotocolinlinearlogic. termkeysoftenconstitutethestageonwhichtheexecution of a protocol takes place, and does not change as it un- folds. We represent and access this persistent information 2 Parametric Strands through a (cid:12)xed multiset (cid:5) of ground atomic formulas with distinguishedpersistentpredicates (e.g.PubK andPrvK)[7]. In this section, we recall (cid:12)rst the notions of strand spaces Arole ismodeledasaparametric strand: astrandwhere and bundles [13, 39], and then recent extensions aimed at the messages may contain variables. An actual strand is capturing protocol execution atthe level of strands [7]. obtained by instantiating all the variables in a parametric An event is a pair consisting of a message m and an strand (or an initial segment of one) with persistent infor- indication of whether it has been sent (+m) or received mation and actual message pieces. Aparametric strand for ((cid:0)m)[13]. Astrand isa(cid:12)nitesequenceof events. Weindi- the role (cid:26) may look as in Figure 1. The freshness of ~n, cate strands with the letter s, the length of a strand as jsj, i.e.thefactthatthevariables~nshouldbeinstantiatedwith anditsi-theventassi(fori=1:::jsj). Astrandsisthere- \new"constantsthathavenotbeenusedbefore,isexpressed fore a chain graph (S;=)), where S = fsi : i = 1:::jsjg, as a side condition. Using the terminology in [13, 39], the moreoversi =)sj i(cid:11)j =i+1,and(cid:12)nallythenodessi are values ~n are uniquely originated. The relationship between labeled with events. variables are expressed in [39] using intuitive notation, e.g. (cid:0)1 A strand space is a set of strands with an additional k for the inverse key of k, or kA for the public key of A. relation ((cid:0)!) on the nodes, such that if (cid:23)1 (cid:0)! (cid:23)2, then Weformalizetheserelationsbyequipping(cid:26)withconstraints (cid:23)1 = +m and (cid:23)2 = (cid:0)m; (cid:0)! represents the transmission (cid:25)(~x),that,withoutlossofgenerality,willbeasetofpersis- of the message m from the sender (cid:23)1 to the receiver (cid:23)2. A tentatomicformulasparameterizedover~x. Inthispaper,it strand space is therefore a graph with two types of arrows, isconvenienttoequipeachparametricstrandwithaninitial a bi-graph using the terminology in [7], (cid:27) = (S;=);(cid:0)!) node labeled with > and an ending node labeled ?. This with the above restriction on (cid:0)!. Given such (cid:27), we will addition is discussed at length in[7]. sometimes write S(cid:27), =)(cid:27), and (cid:0)!(cid:27) for S, =), and (cid:0)! A protocol is given as a set of roles. The model of the respectively. intruder in the style of Dolev and Yao [11, 34] is also spec- + (cid:0) Let S and S indicate the set of positively- and i(cid:12)ed as a set of parametric strands P(P0) called penetrator negatively-labeled nodes in S respectively. A bundle [13, 7] strands, where P0 is theintruder’s initial knowledge [7, 39]. (seealso [21])isastrandspace(cid:27)=(S;=);(cid:0)!)suchthat Asanexample,Figure2showshowtheNeedham-Schroeder + (cid:0) the bipartite graph (S ;S ;(cid:0)!) is functional (a positive public key protocol is modeled using parametric strands, nodehasatmostoneoutgoing(cid:0)!-edge),injective(anega- where we have used incoming and outgoing arrows instead tivenodehasatmostoneincoming(cid:0)!-edge),andsurjective of the tags + and (cid:0) for readability. We ask the reader to (a negative node has at least one incoming (cid:0)!-edge), and 2 (cid:0)1 (cid:0)1 Initiator(KA;KA ;KB;NA;NB) Responder(KB;KB ;KA;NB;NA) (cid:0)1 (cid:0)1 NA fresh,(cid:25)A(KA;KA ;KB) NB fresh,(cid:25)B(KB;KB ;KA) > > wQ(q0) wQ(q00) w w w w fNA;K(cid:127)AgKB (cid:0)! (cid:0)! fNA;K(cid:127)AgKB wQ(q1) wQ(q10) w w w w (cid:0)! fNA;N(cid:127)BgKA fNA;N(cid:127)BgKA (cid:0)! wQ(q2) wQ(q20) w w w w fNB(cid:127)gKB (cid:0)! (cid:0)! fNB(cid:127)gKB wstop wstop w w w w (cid:127)? (cid:127)? where (cid:25)A(KA;KA(cid:0)1;KB) = PubK(KA); PrvK(KA;KA(cid:0)1); PubK(KB) (cid:25)B(KB;KB(cid:0)1;KA) = PubK(KB); PrvK(KB;KB(cid:0)1); PubK(KA) Figure 2: ExtendedStrandSpeci(cid:12)cation of Needham-Schroeder ignoretheshadedannotationsonthe=)-edgesforthemo- We de(cid:12)ne the notion of one-step transition between ] ] ment. two con(cid:12)gurations ((cid:27)1;(cid:27)1)(cid:6)1 and ((cid:27)2;(cid:27)2)(cid:6)2, written Thesede(cid:12)nitionsallowustospecializethebundlesweare ] o ] lookingat: givenasetofparametricstrandsS,everystrand ((cid:27)1;(cid:27)1)(cid:6)17(cid:0)!S((cid:27)2;(cid:27)2)(cid:6)2, by means of four rules that we call Cf, Ci, S and R. For the sake of conciseness, we limit in a bundle (cid:27) should be an initial pre(cid:12)x of an instantiated ourselvestoanintuitivepresentationbasedonthefollowing protocol (orpenetrator)strand. Weareinterestedininitial sketches. A formal de(cid:12)nitioncan befound in [7]. pre(cid:12)xes since a bundle is a snapshot of the execution of a protocol, and a particular role instance may be halfway S(cid:22) S(cid:22)]nS(cid:22) S(cid:22) > S(cid:22)]nS(cid:22) through its execution. We then say that (cid:27) is a bundle over Cf((cid:26);(cid:24)) S. (cid:0)!S w w Wewillnowgiveafewde(cid:12)nitionsneededtoemulatethe (cid:127)..(cid:26)[(cid:24)] execution of a protocol with parametric strands. First, ob- . serve that the network tra(cid:14)c in a bundle is expressed in terms of events and of the (cid:0)! relation. The edges of (cid:0)! S(cid:22) > S(cid:22)]nS(cid:22) S(cid:22) > S(cid:22)]nS(cid:22) representpasttra(cid:14)c: messagesthathavebeensentandsuc- Ci((cid:26)[(cid:24)];(cid:18)) cessfully received. The dangling positive nodes correspond w (cid:0)!S w w w to current tra(cid:14)c: messages in transit that have been sent, (cid:127)..(cid:26)[(cid:24)] (cid:127)..(cid:26)[(cid:24);(cid:18)] but not yet received. We will call these nodes the fringe of . . thebundle(orstrandspace). Moreformally,givenastrand space (cid:27)=(S;=);(cid:0)!), its fringe is theset S (cid:23)0 S]nS S (cid:23)0 S]nS 0 0 S((cid:23);(cid:23)0;(cid:23)00) Fr((cid:27))=f(cid:23) :(cid:23) 2S; (cid:23) =+m; and69(cid:23) :(cid:23) (cid:0)!(cid:23) g: (cid:0)!S w 00 w 00 Another component of the execution state of a protocol (cid:23)w (cid:23) (cid:23)w (cid:23) isadescriptionoftheactionsthatcanlegallytakeplacesin (+(cid:127)m) ((cid:0)m) (+(cid:127)m)(cid:0)(cid:0)(cid:0)(cid:0)!((cid:0)m) order to continue the execution. First, some technicalities. Let (cid:27) be a bundle over a set of parametric strands S, a S (cid:23)0 S]nS S (cid:23)0 S]nS completion of (cid:27) is any strand space (cid:27)~ that embeds (cid:27) as a R((cid:23);(cid:23)0;(cid:23)00) subgraph,andthatextendseachincompletestrandinitwith (cid:0)!S theomittednodesandtherelative=)-edges. Ifsisastrand (cid:23)00 ww(cid:23) (cid:23)00 ww(cid:23) in (cid:27) and s~ is its extension in (cid:27)~, the sequence obtained by (+m(cid:0))(cid:0)(cid:0)(cid:0)!((cid:0)(cid:127)m) (+m(cid:0))(cid:0)(cid:0)(cid:0)!((cid:0)(cid:127)m) removingeveryeventinsfroms~isitselfa(possiblyempty) strand. We call it a residual strand and indicate it as s~ns. Themoveothatlabelsthetransitionarrow7(cid:0)!S recordsthe We then write (cid:27)~n(cid:27) for the set of all residual strands of (cid:27)~ necessaryinformationtoreconstructthetransitionuniquely. with respect to (cid:27). Rule Cf describes the instantiation of a parametric Giventhesepreliminaryde(cid:12)nitions,acon(cid:12)guration over strand(cid:26)(~x;~n)withasubstitution(cid:24) forallitsvariablesthat ] ] Sisastructure((cid:27);(cid:27) )(cid:6) where(cid:27)isabundleoverS,and(cid:27) is are marked\fresh" (~n). Thesubstitutedconstants mustbe anextensionof(cid:27) whoseonlyadditional(cid:0)!-edgesoriginate distinct from each other and from any other value appear- ] ] in Fr((cid:27)), cover all of Fr((cid:27)), and point to (cid:27) n(cid:27), and (cid:12)nally ingin(cid:27)1. RuleCi realizesthesecondstageofinstantiation: ] thesignature (cid:6)listsall thesymbolsthatappear in (cid:27) (and it applies a substitution (cid:18) to the remaining variables ~x of (cid:27)). a partially instantiated strand (cid:26)[(cid:24)], checks that the atomic 3 formulasresultingfrominstantiatingtheconstraints(cid:25)(~x)of while A1(cid:0)(cid:14)A2 realizes resource A2 subject to the avail- ] (cid:26) with (cid:18) satisfy (cid:5), and install its initial node > in (cid:27)1 to ability of A1 while consuming A1 itself (this implements ] therefore the notion of transition). When instantiating produce (cid:27)2. We must perform instantiation in two stages quanti(cid:12)ers, we write [t=x]A for the capture-free substitu- to handle protocols where two parties exchange newly pro- tion of term t for variable x in formula A. We abbreviate ducednoncesasintheNeedham-Schroederprotocol inFig- [t1=x1]([t2=x2](:::[tn=xn]A))as [t1=x1;:::;tn=xn]A. ure 2. Contexts are(cid:12)nitemultisetsofcomma-separatedformu- Theremainingrulesdealwithmessagetransmissionand las. The empty context is denoted \(cid:1)". We will use the reception once a strand has beeninstalled in thecon(cid:12)gura- 0 00 letter (cid:0) and (cid:1), possibly subscripted, to indicate contexts. tion. Inparticular,(cid:23), (cid:23) and(cid:23) arenodesonfullyinstanti- atedstrands. RuleSmodelstheactionofsendingamessage: A signature (cid:6) is a list of constants. Thederivabilityjudgmentswewillrelyuponaresequents ifthecon(cid:12)gurationathandembedsastrandthatisnotfully of theform[17]: contained in the bundle part (cid:27)1 and the (cid:12)rst missing node (cid:0); (cid:1) ‘(cid:6) A (cid:23) is positive, we add an (cid:0)!-arrow to a matching negative 00 node (cid:23) and include (cid:23) in (cid:27)2. Receiving a message is mod- where the formulas in (cid:0) and (cid:1) are the resources available ] eled by rule R: if ((cid:27)1;(cid:27)1)(cid:6)1 mentions a strand that is not to produce the formula A. While the elements in (cid:1) shall fully contained in its bundle part and its (cid:12)rst missing node be used exactly once, the resources in (cid:0) can be exploited (cid:23) has an incoming (cid:0)!-edge,we add it tothe bundle. arbitrarily manytimes, possibly zero. This convenienttwo- Amultistep transition amountstochainingzeroormore context formulation [17] is rewritten as a more common one-steptransitions. Thisrelationisobtainedbytakingthe single-context sequent by augmenting (cid:1) with the result of ~o (cid:3) o re(cid:13)exiveandtransitiveclosure7(cid:0)!S of7(cid:0)!S,where~oisthe pre(cid:12)xing every formula in (cid:0) with the exponential modality sequenceofthecomponentmoves(\(cid:1)"ifempty). ~oisatrace \!" [16]. The signature (cid:6) lists all the constants mentioned of the computation. in the sequent. Although usually omitted in presentations Ourde(cid:12)nitionoftransitionpreservescon(cid:12)gurations, i.e. of (linear) logic, it simpli(cid:12)es ourtreatmentof nonces. ] ] o ] if((cid:27)1;(cid:27)1)(cid:6)1 isacon(cid:12)gurationand((cid:27)1;(cid:27)1)(cid:6)17(cid:0)!S((cid:27)2;(cid:27)2)(cid:6)2, The relevant inference rules for this language are dis- ] playedinFigure3. Therulesontheleft-handsidearecalled then ((cid:27)2;(cid:27)2)(cid:6)2 is also a con(cid:12)guration. Moreover, (cid:6)1 (cid:18)(cid:6)2. multiplicative. Ruleidwillbeusedattheleavesofaderiva- These properties extendtomultistep transitions. tion: itspeci(cid:12)es thatan object Acanbetrivially produced from A itself (the formulas in (cid:0) are ignored). Notice that 3 Elements of Linear Logic no excess resources are admitted. Rule (cid:0)(cid:14)l speci(cid:12)es how to use a resource A1(cid:0)(cid:14)A2 to build an object C: if A1 can Thetargetofourinterpretationofstrandconstructionswill be produced using part of the context ((cid:1)1), then A2 and beasublanguageoflinearlogic[16]. Wechoosethisformal- what remains of the context ((cid:1)2) are available to produce ismovermoretraditionallogicsbecauseofitsinterpretation C. Rule (cid:10)l states that a composite resource can be bro- of formulas as consumable resources. This provides, for ex- kentomakeitscomponentsindividuallyavailable,while(cid:10)r ample, a simple way of modeling the fact that receiving a speci(cid:12)es thatA1 (cid:10) A2 isproducedbybuildingitspartsin- messagemakesitunavailabletootherrecipients(unlessfur- dependently. Theconstant1isthenon-resource: itdoesnot ther actions are taken). contribute toa goal (rule 1l)anddoes requireanyresource Thislanguage,afragmentof(cid:12)rst-ordermultiplicativeex- to be established (rule 1r). Rule cut permits constructing ponentiallinearlogictobeprecise,isgivenbythefollowing anobjectinstages: inordertoobtainC,onecan(cid:12)rstbuild grammar: A with some of the available resources, and then use A to achieveC. SinceCcanalwaysbeproduceddirectlyfromthe A ::=P Atomic formulas original resources, this rule is e(cid:11)ectively redundant, which j1 Multiplicative unit we emphasize bydisplaying it in a shadedfont. jA1 (cid:10) A2 Multiplicative conjunction The right-hand side of Figure 3 shows rule dl (derelic- jA1(cid:0)(cid:14)A2 Linear implication tion), which makes a copy of a formula A in (cid:0) available in j8x:A Universal quanti(cid:12)cation (cid:1), and the rules concerning the quanti(cid:12)ers. Observe that j9x:A Existential quanti(cid:12)cation the existential quanti(cid:12)ers in the context(cid:1) are instantiated with new constants (rule 9l), which we record in the sig- P ::=N(m) Message in transit nature (cid:6). In the right-hand side of the turnstile (rule 9r), jPubK(k)j ::: Persistent information thesequanti(cid:12)ershaveinsteadthefunctionofhidingtheuse jQ(q) Intermediate step of these newly introduced constants. Notice that they are jstop Role completion instantiated with constants from (cid:6) rather than with arbi- We use messages and their constituents as the basis of the trary terms: this is su(cid:14)cient for our purposes. Instead, we term language of our formulas, as described in [7]. We rely allowuniversallyquanti(cid:12)edvariablestobeinstantiatedwith on the unary predicate symbol N to hold messages being arbitrary terms(rule 8l). exchanged, and we maintain the syntax we glimpsed at in theprevioussectionforpersistentinformation. Atomsofthe 4 Strands in Linear Logic formQ(q)identifyuniquelytheintermediate=)-edgesina con(cid:12)guration (see Section 4). Finally, the atomic constant We will now describe the translation of parametric strands stop will indicate the completionof a strand. and con(cid:12)gurations into the fragment of linear logic we just The connectives we will need are (cid:10), known as multi- discussed. We shall emphasize that this encoding does not plicative conjunction, the constant 1 (multiplicative unit), treat penetrator strands di(cid:11)erently from regular protocol (cid:0)(cid:14) or linear implication, and the usual quanti(cid:12)ers. A re- strands in any way. This adheres to the strand philosophy, source A1 (cid:10) A2 consists of the sum of parts A1 and A2, 4 Multiplicatives Exponentialsandquanti(cid:12)ers (cid:0);(cid:1)1 ‘(cid:6) A (cid:0);(cid:1)2;A ‘(cid:6) C (cid:0);A;(cid:1);A ‘(cid:6) C id cut dl (cid:0);A ‘(cid:6) A (cid:0);(cid:1)1;(cid:1)2 ‘(cid:6) C (cid:0);A;(cid:1) ‘(cid:6) C (cid:0);(cid:1)1 ‘(cid:6) A1 (cid:0);(cid:1)2;A2 ‘(cid:6) C (cid:0);(cid:1);[t=x]A ‘(cid:6) C (cid:0)(cid:14)l 8l (cid:0);(cid:1)1;(cid:1)2;A1(cid:0)(cid:14)A2 ‘(cid:6) C (cid:0);(cid:1);8x:A ‘(cid:6) C (cid:0);(cid:1);A1;A2 ‘(cid:6) C (cid:0);(cid:1)1 ‘(cid:6) A1 (cid:0);(cid:1)2 ‘(cid:6) A2 (cid:0);(cid:1);[c=x]A ‘(cid:6);c C (cid:0);(cid:1) ‘(cid:6);c [c=x]A (cid:10)l (cid:10)r 9l ((cid:3)) 9r (cid:0);(cid:1);A1 (cid:10) A2 ‘(cid:6) C (cid:0);(cid:1)1;(cid:1)2 ‘(cid:6) A1 (cid:10) A2 (cid:0);(cid:1);9x:A ‘(cid:6) C (cid:0);(cid:1) ‘(cid:6);c 9x:A (cid:0);(cid:1) ‘(cid:6) C 1l 1r (cid:0);(cid:1);1 ‘(cid:6) C (cid:0);(cid:1) ‘(cid:6) 1 ((cid:3)) cnotin(cid:6) Figure 3: RelevantRulesof Linear Logic andcontrastswithotherapproacheswhichsyntacticallydif- any other value in use. Applying this encoding to the ferentiate theintrudermodel(e.g. [6]). Needham-Schroederprotocolspeci(cid:12)edinFigure2yieldsthe Let(cid:26)(~n;~x;~y)beaparametricstrandwithconstraints\~n linear logic formulas inFigure 4. fresh, (cid:25)(~x)". Lets0;s1;:::;sn;sn+1 bethenodesof (cid:26),with In order to de(cid:12)ne the encoding of a con(cid:12)guration, we s0 =>, sn+1 =?, and for i=0::n, si =)si+1. We de(cid:12)ne need to extend this notation to partially and fully instanti- p q the encoding of node si (for i = 0::n+1), written si , as atedstrands. Let(cid:24)beasubstitutionforthe\fresh"variables follows: ~n of (cid:26). Then p q sn+1 =stop p q p q p q p q (cid:26)[(cid:24)] =[(cid:24);u0=q0;:::;un(cid:0)1=qn(cid:0)1]8~x;~y: s0 ; si =Q(qi(cid:0)1) (cid:10) (Q(qi(cid:0)1) (cid:10) N(m)(cid:0)(cid:14) si+1 ) if si=(cid:0)m p q p q where u0;:::;un(cid:0)1 are distinct constants. If furthermore (cid:18) si =Q(qi(cid:0)1) (cid:10) (Q(qi(cid:0)1)(cid:0)(cid:14)N(m) (cid:10) si+1 ) is a substitution for the remaining variables ~x;~y of (cid:26), we if si=+m p q p q de(cid:12)ne s0 =(cid:10)(cid:25)(~x)(cid:0)(cid:14)(cid:10)(cid:25)(~x) (cid:10) s1 p q p q (cid:26)[(cid:24);(cid:18)] =[(cid:18)]([(cid:24);u0=q0;:::;un(cid:0)1=qn(cid:0)1] s0 ): where, given a multiset of formulas (cid:1), (cid:10)(cid:1) is the formula obtained by taking the multiplicative conjunction of very p q Observe that (cid:18) can mention some of the constants newly element of (cid:1). For i = 1::n, si expresses the action in si p q introducedby(cid:24). Weextendthenotation si ,fori=0::n+ byplacing thesent(received)message min theconsequent 1,tothecasewheresiisanodeinafullyinstantiatedstrand (resp.antecedent)oftheimplication. Rule(cid:0)(cid:14)lwillhavethe (clearly, the qi’s will havebeenreplaced with ui’s). e(cid:11)ect of inserting (resp. removing) N(m) into (resp. from) We shall now encode con(cid:12)gurations. A con(cid:12)guration the context (cid:1). Notice that its application will also insert ] p q ((cid:27);(cid:27) )(cid:6) comprisesthreetypesofinformation: 1)anaccount si into (cid:1), enabling in this way the next action. This ofhowthissituationhasbeenreached(as(cid:27)andthestrands techniqueisknownascontinuation-passing style inthepro- ] in (cid:27) that have been instantiated, but not yet used); 2) a gramminglanguage community. descriptionofthecurrentsituation(inFr((cid:27)));and3)asum- The arguments of the conjuncts Q(q0);:::;Q(qn(cid:0)1) are ] distinctvariables. Itisconvenienttointerpretthemaslabels maryofthefutureactionsthatcanbeperformed(in(cid:27) n(cid:27)). for the =)-edges of (cid:26), as shown in Figure 2. The last ar- Wewill ignore the(cid:12)rstaspect sinceitwill bepartially cap- row,leadingtosn+1 =?,isinsteadlabeledwiththepropo- tured through the notion of derivation. The representation sitional letter stop. These atoms serve multiple purposes: ofFr((cid:27))willsimplybetheconjunctionofthemessagesinit (cid:12)rsttheyprovideawaytopreservetheorderofconsecutive (or 1 if none is present): message transmissions or receptions, which may prove im- p q Fr((cid:27)) =NHN(m):m2Fr((cid:27))I: portantfor someapplications; secondtheirpresencegreatly simpli(cid:12)esourproofsastheyimplementthe\locksandkeys" wherewewriteH:::Iforthemultisetequivalentoftheusual technique[23], whichhas yieldedfaithful representations of ] setnotationf:::g. Asfor(cid:27) n(cid:27),wetaketheconjunctionof variouscomputationalparadigmsinlinearlogic[22,23,24]; therepresentation of eachfully instantiated residual strand third, they are a crucial device for bridging the gap with in it, plus the representation of the strands that are only the multiset rewriting speci(cid:12)cation of a protocol [7]. Were partially instantiated: these reasons, in particular the (cid:12)rst one, to fall, a simpler encoding can be achieved by replacing the Q(qi)’s and stop p ] q p q ] (cid:27) n(cid:27) =NH si+1 :s=(cid:26)[(cid:24);(cid:18)] in (cid:27) ; with the linear logic constant 1. ] ingTthheeferneceovdainrigabolfes(cid:26)iinsapcsh0iqe:vedbyappropriatelyquantify- (cid:10)NHp(cid:26)[(cid:24)]q :(cid:26)s[i(cid:24)]2in(cid:27)S(cid:27);]Ia:ndsi+1 2(cid:27)Sn(cid:27)SI p q p q (cid:26) =9qo;:::;qn(cid:0)1:9~n:8~x;~y: s0 Forthesakeof conciseness, wede(cid:12)netherepresentation ] of a con(cid:12)guration ((cid:27);(cid:27) )(cid:6) as Existentially quantifying the qi’s, as well as ~n, guarantees p ] q p ] q p ]q that they will be instantiated with constants distinct from ((cid:27);(cid:27) )(cid:6) = Fr((cid:27);(cid:27) ) (cid:10) (cid:27)n(cid:27) : 5 (cid:0)1 (cid:0)1 (cid:0)1 9q0;q1;q2:9nA:8kA;kA ;kB;nB: (cid:10)(cid:25)A(kA;kA ;kB) (cid:0)(cid:14) (cid:10)(cid:25)A(kA;kA ;kB) (cid:10) Q(q0) (cid:10)( Q(q0) (cid:0)(cid:14) N(fkA;nAgkB) (cid:10) Q(q1) (cid:10)( Q(q1) (cid:10) N(fnA;nBgkA) (cid:0)(cid:14) Q(q2) (cid:10)( Q(q2) (cid:0)(cid:14) N(fnBgkB) (cid:10)stop))) 0 0 0 (cid:0)1 (cid:0)1 (cid:0)1 0 9q0;q1;q2:9nB:8kB;kB ;kA;nA: (cid:10)(cid:25)B(kB;kB ;kA) (cid:0)(cid:14) (cid:10)(cid:25)B(kB;kB ;kA) (cid:10) Q(q0) (cid:10)( 0 0 Q(q0) (cid:10) N(fkA;nAgkB) (cid:0)(cid:14) Q(q1) (cid:10)( 0 0 Q(q1) (cid:0)(cid:14) Q(q2) (cid:10) N(fnA;nBgkA) (cid:10)( 0 Q(q2) (cid:10) N(fnBgkB) (cid:0)(cid:14) stop))) Figure 4: Linear Logic Translation of the Needham-SchroederProtocol Wewill maketheencodingwe havejust presentedmore Proof: By induction on the structure of ~o. If the move se- concrete by means of an example. The upper part of Fig- quenceisprocessedright-to-left,weobtainacut-freederiva- ] ure 5 shows a con(cid:12)guration ((cid:27);(cid:27) ) representing an initial tion. Operating forward (left-to-right) requires the use of stage of Lowe’s attack [26] on the Needham-Schroederpro- the cut rule (whichcan subsequentiallybe eliminated). 2 tocol in Figure 2. It contains six strands: an initiator, a responder, and one instance of each of the four penetrator strands M0 (access to the intruder’s initial knowledge), D Intheaboveproof, eachmoveissimulatedbytheappli- (decryption), M (access to public information) and E (en- cationofanumberoflinearlogic rules. This(cid:12)nergranular- cryption). A detailed discussion of penetrator strands can ityisahindrancewhenconsideringaderivationthatrelates be found in [7]. Constants are indicated using a di(cid:11)erent the encoding of two con(cid:12)gurations, and trying to read o(cid:11) font than variables (e.g. nA as opposed to nA). In this con- the move sequences that have actually been applied: these (cid:12)guration,theinitiatorhasexecutedits(cid:12)rstaction,strands micro-steps can be intermingled in arbitrary ways. This M0 andD havebeencompleted,strandsM andE arefully forces us to break our completeness proof into a numberof instantiatedbutstillhavetoexecutetheir(cid:12)rstaction,while stages aimed at disentangling the given linear logic deriva- the responder strand has been only partially instantiated. tion. First we reduce ourselves to a purely multiplicative The only message in transit (thefringe) is (nA;kA). settingbypushingdlandthequanti(cid:12)errulesatthebottom ] of thegivenderivation. Thesecondboxin(cid:12)gure5showstheencodingof((cid:27);(cid:27) ) in linear logic. Observe that, whenever the border between ] Lemma 5.2 Let S be a set of parametric strands and (cid:27)Q(aun(cid:26)id)c(cid:27)orrnes(cid:27)pocnrodsisnegstaonthaectiinvteersstercatnedd,=t)he-eadtgoemaicppfoeramrsualas ((cid:27)1;(cid:27)1])(cid:6), ((cid:27)2;(cid:27)2])(cid:6);~n two con(cid:12)gurations over S. If there p ] q is a cut-free derivation D of the sequent a conjunct in (cid:27) n(cid:27) . Similarly, each terminated strand contributes an occurrence of stop. The residual of every p q p ] q p ] q active strand yields a formula with implications. Finally, S ; (cid:5); ((cid:27)1;(cid:27)1)(cid:6) ‘(cid:6) 9~n: ((cid:27)2;(cid:27)2)(cid:6);~n (cid:10) (cid:5) notice that the representation of the partially instantiated then there exists an instantiation of variables ~n with fresh responderstrandaccountsfortheonlyquanti(cid:12)ersappearing 0 ] in p((cid:27);(cid:27)])q. distinctconstants(cid:6),acon(cid:12)guration((cid:27)0;(cid:27)0)(cid:6);(cid:6)0,andacut- (cid:3) free derivation D of the sequent 5 Soundness and Completeness p q p 0 ] q S ;(cid:1)‘(cid:6);(cid:6)0 [(cid:6)=~n]((cid:27)2;(cid:27)2)(cid:6);(cid:6)0 (cid:10) (cid:5) We will now show that, given the above encoding, reach- p ] q p ] q ability among con(cid:12)gurations is mapped to the derivability where (cid:1)=(cid:5); ((cid:27)1;(cid:27)1)(cid:6) ; ((cid:27)0;(cid:27)0)(cid:6);(cid:6)0 , that does use nei- of their representation in linear logic, and vice versa. Con- ther dl nor any of the quanti(cid:12)er rules 8l, 9l, 9r. structing a derivation that mimics a sequence of moves in the strand world, formally stated in the following theorem, Proof: Weexploittherelativepermutabilityoftheseinfer- is fairly simple. encerules,asdescribedin[25]. Moreprecisely,weapplythe following four steps: Theorem 5.1 (Soundness) ] 1. We permute rule dl below every other rule. The re- Let S be a set of parametric strands and ((cid:27)1;(cid:27)1)(cid:6), ] sulting derivation consists then of a sequence of appli- ((cid:27)2;(cid:27)2)(cid:6);n~ two con(cid:12)gurations over S. If there is a move cations of dl followed bya subderivation D0 that does sequence ~o such that notuse thisrule. Theapplications of dl correspondto ] ~o (cid:3) 0 ] committingtotheparametricstrandsthatwillbeused ((cid:27)1;(cid:27)1)(cid:6)7(cid:0)!S;(cid:5)[(cid:6)=~n]((cid:27)2;(cid:27)2)(cid:6);(cid:6)0 toproduce((cid:27)2;(cid:27)2])(cid:6);~n (onceinstantiated,theywillcor- ] forsomeinstantiation ofvariables~nwithfreshdistinct con- respond to ((cid:27)0;(cid:27)0)(cid:6);(cid:6)0). 0 stants (cid:6),thenthere exists alinearlogicderivation D ofthe 0 2. Wepermuterule9ltothebottomofD,whichenables sequent 00 ustoconsiderasubderivationD thatdoesnotcontain p q p ] q p ] q theserules. Theseuses of9l correspondtopickingthe S ; (cid:5); ((cid:27)1;(cid:27)1)(cid:6) ‘(cid:6) 9~n: ((cid:27)2;(cid:27)2)(cid:6);~n (cid:10) (cid:5): 0 new constants thatappear in (cid:6) beforehand. 6 0 Initiator M D M E Responder (cid:0)1 (cid:0)1 (cid:0)1 (cid:0)1 (kA;kA ;kI;nA;nB) (kI ) ((nA;kA);kI;kI ) (kB) ((nA;kA);kB) (kB;kB ;kA;nB;nA) > > > > > > _ Q(qA0) Q(qM00) _ Q(qD0) fnA;kAgkI >fnA;kAgkI Q(qD1) Q(qE0) _ _ k(cid:0)I 1 >k(cid:0)I 1 Q(qM0) Q(qD2) Q(qB0) _ _ (nA;kA) >(nA;kA) Q(qA1) Q(qE1) _ _ kB kB Q(qE2) _ _ stop fnA;kAgkB fkA;nAgkB stop Q(qB1) _ _ fnA;nBgkA stop fnA;nBgkA Q(qA2) stop Q(qB2) _ _ fnBgkI fnBgkB stop stop _ _ _ _ _ _ ? ? ? ? ? ? p q N((nA;kA)) Fr((cid:27)) = A Q(u1) (cid:10) ( p(cid:27)]n(cid:27)q=8>>>>>>>>>>>>>>>>>>>>>>< (cid:10)(cid:10)(cid:10)(cid:10) ssQQttoo((uuppM0E0QQ))(((cid:10)uu(cid:10)A1E0QQ())(Q(((cid:10)(cid:10)uu(A2E1qNN))M0(cid:0)(((cid:10))(f(cid:14)n(cid:0)nNAN(cid:14)A;((;NkfknA(nBBkB))gB)g(cid:0)k)(cid:0)Ak(cid:14)I(cid:14))(cid:10))Q(cid:0)Q(cid:10)((cid:14)s(utuQE2osE1tp)()ou)(cid:10)pA2(cid:10))))(((cid:10) ( 9=;9>=IEMMDn(i((0(t((kninakBAAt(cid:0)I);o;1krk)A(Ak))A;;k;kBkI;(cid:0)A)k1(cid:0)I;1k)I;nA;nB) E >>>>>>>>>>>>>>>>>>>>>>: (cid:10) (8kB(cid:10);k(cid:25)B(cid:0)B1Q(;k(kBuAB0;QQ;k)nB(((cid:0)(cid:10)Auu12B1:;QN))k(cid:0)((cid:0)(Auf(cid:14)(cid:14))B2kNQ(cid:0))A((cid:14)(;(cid:10)funn(cid:10)B2AAN);(cid:25)g((cid:10)kkBfABn(gNBk)kgB(B(cid:0)fk)(cid:14);nBkQ(cid:10)A)B(cid:0)(;(cid:0)1usn(cid:14);tB1Boks)gpAtok)(cid:10))Ap)))(cid:10))())(cid:10))Q((uB0) (cid:10) ( >;9>>>=>>>;Responder(kB;kB(cid:0)1;kA;nB;nA) where pM0q= 9q0:8x: P0(x)(cid:0)(cid:14)P0(x) (cid:10) Q(q0) (cid:10) ( Q(q0)(cid:0)(cid:14)N(x) (cid:10) stop) pDq= 9q0;q1;q2:8m;k;k0: PrivK(k;k0)(cid:0)(cid:14)PrivK(k;k0) (cid:10) Q(q0) (cid:10) ( Q(q0) (cid:10) N(fmgk)(cid:0)(cid:14)Q(q1) (cid:10) ( Q(q1) (cid:10) N(k0)(cid:0)(cid:14)Q(q2) (cid:10) ( Q(q2)(cid:0)(cid:14)N(m) (cid:10) stop))) p q M = 9q0:8k: PubK(k)(cid:0)(cid:14)PubK(k) (cid:10) Q(q0) (cid:10) ( Q(q0)(cid:0)(cid:14)N(k) (cid:10) stop) p q E = 9q0;q1;q2:8m;k: PubK(k)(cid:0)(cid:14)PubK(k) (cid:10) Q(q0) (cid:10) ( Q(q0) (cid:10) N(m)(cid:0)(cid:14)Q(q1) (cid:10) ( Q(q1) (cid:10) N(k)(cid:0)(cid:14)Q(q2) (cid:10) ( Q(q2)(cid:0)(cid:14)N(fmgk) (cid:10) stop))) Figure 5: A Translation: Lowe’s attack on the Needham-SchroederProtocol 7 00 3. We permute rules 9r to the end of D , obtaining a id 000 subderivation D that does not mention these rules. 0 The applications of 9r correspond to hiding (cid:6) in the (cid:10)r overall derivation. (cid:10)l 4. Finally, we permute every use of 8r down past every (cid:3) (cid:10)l;:::;(cid:10)l;(cid:0)(cid:14)l otherrule,makingexplicitasubderivationD withthe 9 preleqtueirtehdecinhsatraancttieartisiotincso.f (T(cid:27)h0e;(cid:27)a0]p)(cid:6)p;l(cid:6)ic0a.tions of 8l com2- (cid:10)l;::::;:(cid:10):l;(cid:0)(cid:14)l >>= ; S=R 8l >>; ; Ci o When interpreted at the strand level, Lemma 5.2 speci(cid:12)es that amovesequencecanberearranged sothatparametric 9r strands are chosen and instantiated before any message is exchanged. More speci(cid:12)cally, all uses of Cf happen (cid:12)rst, 9l ; Cf o followed by all applications of Ci. Only then, can S- and dl R-movestakeplace. The next stepconsists ingrouping together the rule ap- plicationsthatcorrespondtoeachmoveinthemultiplicative Figure 6: Completeness Argument part of the given derivation. This provides a simple way of identifying movesS andR. Lemma 5.3 Let S be a set of parametric strands and A (cid:12)ne analysis of this proof reveals that linear logic ] ] derivationsenableaformofabstractionthatmovesequences ((cid:27)1;(cid:27)1)(cid:6), ((cid:27)2;(cid:27)2)(cid:6) two con(cid:12)gurations over S. If there is (cid:3) do not achieve. Indeed, the tree structure of a derivation a cut-free derivation D of the sequent doesnotalwaysimposeatotalorderonindependenttransi- p q p ] q p ] q tions. Thisisaverymildformofnon-determinismcompared S ; (cid:5); ((cid:27)1;(cid:27)1)(cid:6) ‘(cid:6) ((cid:27)2;(cid:27)2)(cid:6) (cid:10) (cid:5) withtheexplicitconcurrencypresentinbundles[7]. Weex- pecttoget amodel closer tobundlesbyconsidering graph- that uses only rules fromthe lefthalfofFigure 3,then there (cid:3)(cid:3) based formulations of linear logic such as proof nets [16]. exists a cut-free derivation D of this sequent such that Furthermore,game-theoreticinvestigationsoflinearlogic[2] (cid:15) Every use of (cid:10)r appear just below id, 1r or (cid:10)r; have produced methods for obtaining very strong forms of completeness which couldbe relevantin this setting. (cid:15) Rules 1l and (cid:10)l are applied eagerly. 6 Interpreting Multiset Rewriting in Linear Logic Proof: Again, we take advantage of the permutability re- sults in [25]. Rule (cid:10)r can be pushed up past any other In this section, we brie(cid:13)y describe how multiset rewriting rule (exceptid and 1r). Onthe other hand, (cid:10)l and 1l can techniquescanbeconvenientlyusedtoexpresssecuritypro- always be permuted down, as long as the nesting of sub- tocols (Section6.1). Wethenshow howtheresulting speci- formulas is respected (clearly if the left-hand side contains (cid:12)cationistranslatedintolinearlogicandstatetheexpected a formula (A (cid:10) B)(cid:0)(cid:14)C, a proof fragment that dismantles this formula mustapply (cid:10)l above (cid:0)(cid:14)l). 2 correctness results (Section 6.2). Finally, we compare the linear logic expressions we derive from the strand and mul- tiset rewriting speci(cid:12)cations of a protocol (Section6.3). Atthispoint,wehavethemeanstoextractasequenceof movesfromalinearlogicderivationthatrelatestheencoding 6.1 Multiset Rewriting for Cryptoprotocols of two con(cid:12)gurations. A multiset M is an unordered collection of objects or ele- ments, possibly with repetitions. The empty multiset does Theorem 5.4 (Completeness) ] not contain any object and will be written \(cid:1)". We accu- Let S be a set of parametric strands and ((cid:27)1;(cid:27)1)(cid:6), ] mulate the elements of two multisets M and N by taking ((cid:27)2;(cid:27)2)(cid:6);n~ two con(cid:12)gurations over S. If there is a linear theirmultisetunion,denoted\M;N". Theelementswewill logic derivation D of the sequent consider here will be (cid:12)rst-order atomic formulas A(~t) over p q p ] q p ] q some signature. S ; (cid:5); ((cid:27)1;(cid:27)1)(cid:6) ‘(cid:6) 9~n: ((cid:27)2;(cid:27)2)(cid:6);~n (cid:10) (cid:5) In its simplest form, a multiset rewrite rule r is a pair of multisetsF andG, respectivelycalledits antecedent and then there exists an instantiation of variables ~n with fresh 0 consequent. We will consider a slightly more elaborate no- distinct constants (cid:6) and a move sequence ~o such that tion in which F and G are multisets of (cid:12)rst-order atomic ] ~o (cid:3) 0 ] formulaswithvariablesamong~x. Weemphasizethisaspect ((cid:27)1;(cid:27)1)(cid:6)7(cid:0)!S;(cid:5)[(cid:6)=~n]((cid:27)2;(cid:27)2)(cid:6);(cid:6)0: by writing them as F(~x) and G(~x). Furthermore, we shall beabletomarkvariablesintheconsequentsothattheyare Proof: The use of Lemma 5.2 followed by Lemma 5.3 to instantiated to \fresh" constants, that have not previously D yields a derivation structured as in Figure 6, from which beenencountered,eveniftheruleisusedrepeatedly. Arule moves over con(cid:12)guration can easily be read o(cid:11) (shown on assumes thenthe form the rightof theschematic derivation). 2 r: F(~x)(cid:0)!9~n:G(~x;~n) 8 Initiator (cid:0)1 (cid:0)1 (cid:0)1 rA0: (cid:25)A0(KA;KA ) (cid:0)! A0(KA;KA );(cid:25)A0(KA;KA ) (cid:0)1 (cid:0)1 rA1: A0(KA;KA );(cid:25)A1(KB) (cid:0)! 9NA:A1(KA;KA ;KB;NA);N(fNA;KAgKB);(cid:25)A1(KB) (cid:0)1 (cid:0)1 rA2: A1(KA;KA ;KB;NA);N(fNA;NBgKA) (cid:0)! A2(KA;KA ;KB;NA;NB) (cid:0)1 (cid:0)1 rA3: A2(KA;KA ;KB;NA;NB) (cid:0)! A3(KA;KA ;KB;NA;NB);N(fNBgKB) Responder (cid:0)1 (cid:0)1 (cid:0)1 rB0: (cid:25)B0(KB;KB ) (cid:0)! B0(KB;KB );(cid:25)B0(KB;KB ) (cid:0)1 (cid:0)1 rB1: B0(KB;KB );N(fNA;KAgKB);(cid:25)B1(KA) (cid:0)! B1(KA;KB;KB ;NA);(cid:25)B1(A) (cid:0)1 (cid:0)1 rB2: B1(KA;KB;KB ;NA) (cid:0)! 9NB:B2(KA;KB;KB ;NA;NB);N(fNA;NBgKA) (cid:0)1 (cid:0)1 rB3: B2(KA;KB;KB ;NA;NB);N(fNBgKB) (cid:0)! B3(KA;KB;KB ;NA;NB) where (cid:25)A0(KA;KA(cid:0)1) = PubK(KA);PrvK(KA;KA(cid:0)1) (cid:25)B0(KB;KB(cid:0)1) = PubK(KB);PrvK(KB;KB(cid:0)1) (cid:25)A1(KB) = PubK(KB) (cid:25)B1(KA) = PubK(KA) Figure 7: Multiset Rewriting Speci(cid:12)cation of the Needham-SchroederProtocol where r is a label and 9~n indicates that the constants that Persistent information: We express persistent informa- instantiate~noughttobefresh. Amultiset rewriting system tionexactlyaswedidinthecaseofstrandsinSection2, R is a set of rewrite rules. i.e.bymeansof a multiset(cid:5) of ground facts. Rewriterulesallowtransformingamultisetintoanother We represent each role (cid:26) in a protocol by meansof a single multiset by making localized changes to the elements that role generation rule and a (cid:12)nite number of protocol execu- appear in it. Given a multiset of ground facts M over a tion rules. The purpose of the former is to prepare for the signature (cid:6), a rule r: F(~x)(cid:0)!9~n:G(~x;~n) is applicable if M = F(~t);M0, for terms ~t. Then, applying r to M yields execution of an instance of role (cid:26). Ithas theform themultisetN =G(~t;~c);M0 wheretheconstants~carefresh r(cid:26)0: (cid:25)(~x)(cid:0)!A(cid:26)0(~x);(cid:25)(~x): (inparticular,theydonotappearinM),~xand~nhavebeen where, as in previous sections, (cid:25)(~x) denotes a multiset instantiated with~tand~crespectively, andthefacts F(~t)in of persistent atomic formulas that may mention variables M havebeen replaced with G(~t;~c) to produce N. The new among ~x. Notice how persistent information is preserved. signature is (cid:6);~c. Wedenote theapplication of a single rule Theexecutionrulesdescribethemessagessentandexpected and of zero or more rewrite rules by means of the one-step by the principal acting in this role. For i =0:::l(cid:26)(cid:0)1, we and multistep transition judgments: havea rule r(cid:26)i+1 of either of thefollowing two forms: r ~r (cid:3) send: A(cid:26)i(~x);(cid:25)(~x;~z) M(cid:6)(cid:0)!RN(cid:6)0 M(cid:6)(cid:0)!RN(cid:6)0 (cid:0)! 9~n:A(cid:26)i+1(~x;~z;~n);N(m(~x;~z;~n));(cid:25)(~x;~z) 0 respectively, where (cid:6) and (cid:6) are the signatures over which receive: A(cid:26)i(~x);N(m(~x;~y));(cid:25)(~x;~y;~z) M andN arerespectivelyde(cid:12)ned. Thelabels r and~r iden- (cid:0)! A(cid:26)i+1(~x;~y;~z);(cid:25)(~x;~y;~z) tify which rule(s) have been applied and the terms ~t used to instantiate ~x. Thus, ~r acts as a complete trace of the where m(~v) stands for a message pattern with variables execution. among ~v. In the (cid:12)rst type of rules, we rely on the exis- tential operator 9~n to model the ability of a principal to Wemodelprotocolsbymeansofspeci(cid:12)callytailoredmul- create nonces when sending a message. This principal can tiset rewriting systems. Wecall this approachMSR. With- alsoincludesomepersistentdata~z (e.g.thenameandpub- out loss of generality, we consider here a slightly simpli(cid:12)ed lic key of an interlocutor), possibly related to information versionofthemodelintroducedin[6,12]. Werelyuponthe it already possesses (~x). In the second rule template, the following atomicformulas: principal should be able to access persistent information ~z related to data in the received message ~y (e.g. the sender’s Network messages: Network messages are modeled by public key) or previously known information ~x. Situations thepredicateN(m),wheremisamessagebeingtrans- whereaprincipalbothsendsandreceiveamessage,orsends mitted. multiplemessages, can easily be expressedbythese rules. Aprotocolisspeci(cid:12)edasasetRofsuchroles. Asanex- Role states: We (cid:12)rst choose a set of role identi(cid:12)ers ample,Figure7showstheencodingofourrunningexample (cid:26)1;:::;(cid:26)n for the di(cid:11)erent roles constituting the pro- in the MLR notation. tocol. Then, for each role (cid:26), we havea (cid:12)nite family of The behavior of the intruder according to the Dolev- role state predicates fA(cid:26)i(m~) j i = 0:::l(cid:26)g. They are Yao model [11, 34] is similarly speci(cid:12)ed as a set of rewrite intendedtoholdtheinternalstateofaprincipalinrole rules[6]. Wewill referto themas I. Astate is thena mul- (cid:26) duringthesuccessive steps of theprotocol. tisetofgroundfactsS =(cid:5);A;N;I,whereAisamultisetof Intruder knowledge: The adversary’s knowledge is held rolestates A(cid:26)i(~t),N ismultisetofmessages N(m)currently inadistributedwayinfactsoftheformI(m),wherem intransit, andI summarizestheintruder’sknowledgeI(m). is some piece of information captured or fabricated by Inparticulartheinitialstateisjust(cid:5);I0,whereI0 contains the intruder. theinformation (e.g. keys)initially knownto theintruder. 9

ebook img

DTIC ADA465155: Interpreting Strands in Linear Logic PDF

13 Pages·0.4 MB·English
by  Defense Technical Information Center
#additional_collections #dticarchive
Save to my drive
Quick download
Download
Upgrade Premium
Most books are stored in the elastic cloud where traffic is expensive. For this reason, we have a limit on daily download.

Preview DTIC ADA465155: Interpreting Strands in Linear Logic

(cid:3)y Interpreting Strands in Linear Logic I. Cervesato N. Durgin M. Kanovich, A. Scedrov ITT Industries Stanford University Universityof Pennsylvania [email protected] [email protected] fmaxkanov,[email protected] Abstract One recent setting for stating the basic assumptions of the Dolev-Yao model is given by strand spaces [13, 14, 39]. The adoption of the Dolev-Yao model, an abstraction of se- Roughly, a strand is a linearly ordered sequence of events curity protocols that supports symbolic reasoning, is respon- that represents the actions of a protocol participant. A sible for many successes in protocol analysis. In particular, strand space is a collection of strands, equipped with a it has enabled using logic e(cid:11)ectively to reason about pro- graphstructuregeneratedbycausalinteractionamongpar- tocols. One recent framework for expressing the basic as- ticipants. This is closely related to Lamport’s notion of sumptions oftheDolev-Yao modelisgivenbystrand spaces, causalityindistributedsystems[21], andaclearinstanceof certain directed graphs whose structure re(cid:13)ects causal inter- Mazurkiewicz’s de(cid:12)nition of trace within concurrency the- actions among protocol participants. We represent strand ory [31]. Prior to a run of the protocol, each principal constructions asrelativelysimpleformulasin(cid:12)rst-order lin- chooses certain data to be used in the protocol, such as ear logic, a re(cid:12)nement of traditional logic known for an in- keysor nonces. trinsic and natural accounting of process states, events, and In contrast, a formal de(cid:12)nition of the Dolev-Yao model resources. The proposed encoding is shown to be sound and intermsofmultisetrewritingwithexistentialquanti(cid:12)cation, complete. Interestingly, this encoding di(cid:11)ers from the mul- MSR[6,7,12],allowsnewvaluessuchaskeysandnoncesto tiset rewriting de(cid:12)nition of the Dolev-Yao model, which is be chosen at any time during the protocol run, as the need also based onlinearlogic. Thisraises thepossibilitythat the for new choices arises. In this formalism, a way of choos- multiset rewriting framework may di(cid:11)er from strand spaces ing new values is provided by the proof rules of existential in some subtle way, although the two settings are known to quanti(cid:12)cation. The MSR formalism has been incorporated agree on the basic secrecy property. into a high-level speci(cid:12)cation language for authentication protocols, CAPSL[10]. 1 Introduction In [7], we established a substantial equivalence of the MSR and strand space formalisms. We introduced a suit- In recent years, a variety of methods have been developed able abstraction of strand con(cid:12)gurations that corresponds for analyzing andreasoning about protocols based oncryp- to MSR states, and showed that related pairs of states and tographic primitives. Although there are many di(cid:11)erences con(cid:12)gurations are equi-reachable. This is relevant for se- amongtheseproposals, mostcurrentformalapproachesuse curity analysis because several basic properties of security the so-called \Dolev-Yao" model of adversary capabilities, protocols(e.g.secrecy)canbephrasedasreachabilityprob- whichappearstobedrawnfrompositions takenin[34]and lems. However, itis notclear thatall relevantproperties of from a simpli(cid:12)ed model presented in [11]. In this idealized security protocols can be phrased in terms of reachability. setting, a protocol adversary is allowed to nondeterministi- Thus a more re(cid:12)ned analysis of the MSR and strand space callychooseamongpossibleactions. Messagesarecomposed formalismsmightrevealthedi(cid:11)erencesbetweenthetwofor- of indivisible abstract values,notsequencesof bits, anden- malismsinregardtosomesubtlepropertiesofprotocols. In cryptionismodeledinanidealizedway. Theadversarymay this paper, which may be seen as a companion to [7], we only sendmessages comprised of datait \knows" as there- providesome preliminarysteps inthis direction. sult of overhearing pasttransmissions. TheMSRandstrandspaceformalismsareanalyzedhere The Dolev-Yao abstraction makes symbolic reasoning in the formal setting of linear logic [16], a re(cid:12)nement of aboutcrypto-protocols aviableapproach. Thisobservation modallogicwithanintrinsicandnaturalaccountingofpro- hasmaterializedinanumberofsuccessfulanalysesthatuse cess states and events. The choice of linear logic is natu- model checking [29, 33, 38] and on several proposals based ral because of the very close connection between multiset onlogic,thequintessentialtoolofsymbolicreasoning[4,35]. rewriting and simple fragments of linear logic, which has been studied extensively [3, 30, 15, 19, 5]. We extend this (cid:3) Partially supported by DoD MURI \Semantic Consistency in standard correspondence to include (cid:12)rst-order parameters Information Exchange" as ONR Grant N00014-97-1-0505, by NSF GrantsCCR-9509931,CCR-9629754andCCR-9800785,andbyNRL andexistentially quanti(cid:12)edvariables. undercontractN0014-96-D2024 tovariousauthors. On the other hand, we also formally represent strand y Wewould liketothankJohnMitchell,PatrickLincoln,Cather- constructionsasrelativelysimpleformulasin(cid:12)rst-orderlin- ineMeadowsandSylvanPinskyforthefruitfuldiscussionsthatcon- ear logic. This encoding is also shown to be sound and tributedtothiswork. complete. As in our previous work on multiset rewriting 1 Report Documentation Page Form Approved OMB No. 0704-0188 Public reporting burden for the collection of information is estimated to average 1 hour per response, including the time for reviewing instructions, searching existing data sources, gathering and maintaining the data needed, and completing and reviewing the collection of information. Send comments regarding this burden estimate or any other aspect of this collection of information, including suggestions for reducing this burden, to Washington Headquarters Services, Directorate for Information Operations and Reports, 1215 Jefferson Davis Highway, Suite 1204, Arlington VA 22202-4302. Respondents should be aware that notwithstanding any other provision of law, no person shall be subject to a penalty for failing to comply with a collection of information if it does not display a currently valid OMB control number. 1. REPORT DATE 3. DATES COVERED 2000 2. REPORT TYPE 00-00-2000 to 00-00-2000 4. TITLE AND SUBTITLE 5a. CONTRACT NUMBER Interpreting Strands in Linear Logic 5b. GRANT NUMBER 5c. PROGRAM ELEMENT NUMBER 6. AUTHOR(S) 5d. PROJECT NUMBER 5e. TASK NUMBER 5f. WORK UNIT NUMBER 7. PERFORMING ORGANIZATION NAME(S) AND ADDRESS(ES) 8. PERFORMING ORGANIZATION ITT Industries,4 West Red Oak Lane,White Plains,NY,10604 REPORT NUMBER 9. SPONSORING/MONITORING AGENCY NAME(S) AND ADDRESS(ES) 10. SPONSOR/MONITOR’S ACRONYM(S) 11. SPONSOR/MONITOR’S REPORT NUMBER(S) 12. DISTRIBUTION/AVAILABILITY STATEMENT Approved for public release; distribution unlimited 13. SUPPLEMENTARY NOTES The original document contains color images. 14. ABSTRACT 15. SUBJECT TERMS 16. SECURITY CLASSIFICATION OF: 17. LIMITATION OF 18. NUMBER 19a. NAME OF ABSTRACT OF PAGES RESPONSIBLE PERSON a. REPORT b. ABSTRACT c. THIS PAGE 12 unclassified unclassified unclassified Standard Form 298 (Rev. 8-98) Prescribed by ANSI Std Z39-18 speci(cid:12)cations of securityprotocols [6,7, 12],theproofrules (=) [ (cid:0)!) is acyclic [7]. In terms of protocols, the (cid:12)rst ofexistentialquanti(cid:12)cationprovidedawayofchoosingnew threeconstraintsimplythatamessageissenttoatmostone values, such as nonces or keys. However, the linear logic recipient at a time, no message is received from more than interpretation introduced here maintains the strand space one sender, and every received message has been sent, re- intuition that nonces are chosen before the protocol is run. spectively. Dangling positive nodes correspond to messages Letusnotethatthisencodingdi(cid:11)ersfromthestandardlin- in transit. Therefore, a bundlerepresents a snapshot of the ear logic representation of multiset rewriting. This raises execution of a protocol. the possibility that the multiset rewriting framework may di(cid:11)er fromstrand spaces in somesubtle way. Linear logic has found applications in numerous areas (cid:26)(~x;~n): ~nfresh, (cid:25)(~x) > of Computer Science, and it has concrete prospects of in- (cid:13)uencing the (cid:12)eld of security protocol analysis in a sim- ww ilar way. As a speci(cid:12)cation language, linear logic has (cid:6)m1(cid:127)(~x;~n) been used to provide elegant and e(cid:11)ective representations w of many systems that share characteristics with crypto- w protocols[8,9,17,18]. Thenaturalembeddingofconcurrent (cid:6)m2(cid:127)(~x;~n) systems in linear logic [15, 20], in particular in its graph- .. . based presentations [16], is also likely to be relevant, given the interpretation of security protocols as concurrent sys- (cid:6)mj(cid:26)j(cid:0)1(~x;~n) tems [1, 40]. Work on meta-reasoning in linear logic [32] w promises to address protocol correctness [4, 35] e(cid:11)ectively (cid:6)mj(cid:26)w(cid:127)j(~x;~n) and e(cid:14)ciently. Finally, some of the theoretical results lin- earlogic hasbroughtabout(e.g.complexityissues[23])are w w expectedtoyieldabetterunderstandingofthemostfunda- (cid:127)? mentalaspects of security protocols [12]. This paper is organized as follows: Section 2 recalls the notionofstrandandreachabilitybetweenstrandcon(cid:12)gura- Figure 1: AParametric Strand tions; Section 3 provides some background on linear logic; Section 4 describes the translation of strand constructions Wenowbuildontheseacceptedde(cid:12)nitionsandpresenta into linear logic, while inSection 5we provesoundnessand strand-basedlanguageforthespeci(cid:12)cationof protocols and completeness theorems that relate strand reachability and oftheirexecution. Theinterestedreadermayconsult[7]for linear logic derivability for their translation. In Section 6, further details. wecomparetheseresultswiththetranslationofthemultiset Data such as the identity of principals and their long- rewritingspeci(cid:12)cationsofasecurityprotocolinlinearlogic. termkeysoftenconstitutethestageonwhichtheexecution of a protocol takes place, and does not change as it un- folds. We represent and access this persistent information 2 Parametric Strands through a (cid:12)xed multiset (cid:5) of ground atomic formulas with distinguishedpersistentpredicates (e.g.PubK andPrvK)[7]. In this section, we recall (cid:12)rst the notions of strand spaces Arole ismodeledasaparametric strand: astrandwhere and bundles [13, 39], and then recent extensions aimed at the messages may contain variables. An actual strand is capturing protocol execution atthe level of strands [7]. obtained by instantiating all the variables in a parametric An event is a pair consisting of a message m and an strand (or an initial segment of one) with persistent infor- indication of whether it has been sent (+m) or received mation and actual message pieces. Aparametric strand for ((cid:0)m)[13]. Astrand isa(cid:12)nitesequenceof events. Weindi- the role (cid:26) may look as in Figure 1. The freshness of ~n, cate strands with the letter s, the length of a strand as jsj, i.e.thefactthatthevariables~nshouldbeinstantiatedwith anditsi-theventassi(fori=1:::jsj). Astrandsisthere- \new"constantsthathavenotbeenusedbefore,isexpressed fore a chain graph (S;=)), where S = fsi : i = 1:::jsjg, as a side condition. Using the terminology in [13, 39], the moreoversi =)sj i(cid:11)j =i+1,and(cid:12)nallythenodessi are values ~n are uniquely originated. The relationship between labeled with events. variables are expressed in [39] using intuitive notation, e.g. (cid:0)1 A strand space is a set of strands with an additional k for the inverse key of k, or kA for the public key of A. relation ((cid:0)!) on the nodes, such that if (cid:23)1 (cid:0)! (cid:23)2, then Weformalizetheserelationsbyequipping(cid:26)withconstraints (cid:23)1 = +m and (cid:23)2 = (cid:0)m; (cid:0)! represents the transmission (cid:25)(~x),that,withoutlossofgenerality,willbeasetofpersis- of the message m from the sender (cid:23)1 to the receiver (cid:23)2. A tentatomicformulasparameterizedover~x. Inthispaper,it strand space is therefore a graph with two types of arrows, isconvenienttoequipeachparametricstrandwithaninitial a bi-graph using the terminology in [7], (cid:27) = (S;=);(cid:0)!) node labeled with > and an ending node labeled ?. This with the above restriction on (cid:0)!. Given such (cid:27), we will addition is discussed at length in[7]. sometimes write S(cid:27), =)(cid:27), and (cid:0)!(cid:27) for S, =), and (cid:0)! A protocol is given as a set of roles. The model of the respectively. intruder in the style of Dolev and Yao [11, 34] is also spec- + (cid:0) Let S and S indicate the set of positively- and i(cid:12)ed as a set of parametric strands P(P0) called penetrator negatively-labeled nodes in S respectively. A bundle [13, 7] strands, where P0 is theintruder’s initial knowledge [7, 39]. (seealso [21])isastrandspace(cid:27)=(S;=);(cid:0)!)suchthat Asanexample,Figure2showshowtheNeedham-Schroeder + (cid:0) the bipartite graph (S ;S ;(cid:0)!) is functional (a positive public key protocol is modeled using parametric strands, nodehasatmostoneoutgoing(cid:0)!-edge),injective(anega- where we have used incoming and outgoing arrows instead tivenodehasatmostoneincoming(cid:0)!-edge),andsurjective of the tags + and (cid:0) for readability. We ask the reader to (a negative node has at least one incoming (cid:0)!-edge), and 2 (cid:0)1 (cid:0)1 Initiator(KA;KA ;KB;NA;NB) Responder(KB;KB ;KA;NB;NA) (cid:0)1 (cid:0)1 NA fresh,(cid:25)A(KA;KA ;KB) NB fresh,(cid:25)B(KB;KB ;KA) > > wQ(q0) wQ(q00) w w w w fNA;K(cid:127)AgKB (cid:0)! (cid:0)! fNA;K(cid:127)AgKB wQ(q1) wQ(q10) w w w w (cid:0)! fNA;N(cid:127)BgKA fNA;N(cid:127)BgKA (cid:0)! wQ(q2) wQ(q20) w w w w fNB(cid:127)gKB (cid:0)! (cid:0)! fNB(cid:127)gKB wstop wstop w w w w (cid:127)? (cid:127)? where (cid:25)A(KA;KA(cid:0)1;KB) = PubK(KA); PrvK(KA;KA(cid:0)1); PubK(KB) (cid:25)B(KB;KB(cid:0)1;KA) = PubK(KB); PrvK(KB;KB(cid:0)1); PubK(KA) Figure 2: ExtendedStrandSpeci(cid:12)cation of Needham-Schroeder ignoretheshadedannotationsonthe=)-edgesforthemo- We de(cid:12)ne the notion of one-step transition between ] ] ment. two con(cid:12)gurations ((cid:27)1;(cid:27)1)(cid:6)1 and ((cid:27)2;(cid:27)2)(cid:6)2, written Thesede(cid:12)nitionsallowustospecializethebundlesweare ] o ] lookingat: givenasetofparametricstrandsS,everystrand ((cid:27)1;(cid:27)1)(cid:6)17(cid:0)!S((cid:27)2;(cid:27)2)(cid:6)2, by means of four rules that we call Cf, Ci, S and R. For the sake of conciseness, we limit in a bundle (cid:27) should be an initial pre(cid:12)x of an instantiated ourselvestoanintuitivepresentationbasedonthefollowing protocol (orpenetrator)strand. Weareinterestedininitial sketches. A formal de(cid:12)nitioncan befound in [7]. pre(cid:12)xes since a bundle is a snapshot of the execution of a protocol, and a particular role instance may be halfway S(cid:22) S(cid:22)]nS(cid:22) S(cid:22) > S(cid:22)]nS(cid:22) through its execution. We then say that (cid:27) is a bundle over Cf((cid:26);(cid:24)) S. (cid:0)!S w w Wewillnowgiveafewde(cid:12)nitionsneededtoemulatethe (cid:127)..(cid:26)[(cid:24)] execution of a protocol with parametric strands. First, ob- . serve that the network tra(cid:14)c in a bundle is expressed in terms of events and of the (cid:0)! relation. The edges of (cid:0)! S(cid:22) > S(cid:22)]nS(cid:22) S(cid:22) > S(cid:22)]nS(cid:22) representpasttra(cid:14)c: messagesthathavebeensentandsuc- Ci((cid:26)[(cid:24)];(cid:18)) cessfully received. The dangling positive nodes correspond w (cid:0)!S w w w to current tra(cid:14)c: messages in transit that have been sent, (cid:127)..(cid:26)[(cid:24)] (cid:127)..(cid:26)[(cid:24);(cid:18)] but not yet received. We will call these nodes the fringe of . . thebundle(orstrandspace). Moreformally,givenastrand space (cid:27)=(S;=);(cid:0)!), its fringe is theset S (cid:23)0 S]nS S (cid:23)0 S]nS 0 0 S((cid:23);(cid:23)0;(cid:23)00) Fr((cid:27))=f(cid:23) :(cid:23) 2S; (cid:23) =+m; and69(cid:23) :(cid:23) (cid:0)!(cid:23) g: (cid:0)!S w 00 w 00 Another component of the execution state of a protocol (cid:23)w (cid:23) (cid:23)w (cid:23) isadescriptionoftheactionsthatcanlegallytakeplacesin (+(cid:127)m) ((cid:0)m) (+(cid:127)m)(cid:0)(cid:0)(cid:0)(cid:0)!((cid:0)m) order to continue the execution. First, some technicalities. Let (cid:27) be a bundle over a set of parametric strands S, a S (cid:23)0 S]nS S (cid:23)0 S]nS completion of (cid:27) is any strand space (cid:27)~ that embeds (cid:27) as a R((cid:23);(cid:23)0;(cid:23)00) subgraph,andthatextendseachincompletestrandinitwith (cid:0)!S theomittednodesandtherelative=)-edges. Ifsisastrand (cid:23)00 ww(cid:23) (cid:23)00 ww(cid:23) in (cid:27) and s~ is its extension in (cid:27)~, the sequence obtained by (+m(cid:0))(cid:0)(cid:0)(cid:0)!((cid:0)(cid:127)m) (+m(cid:0))(cid:0)(cid:0)(cid:0)!((cid:0)(cid:127)m) removingeveryeventinsfroms~isitselfa(possiblyempty) strand. We call it a residual strand and indicate it as s~ns. Themoveothatlabelsthetransitionarrow7(cid:0)!S recordsthe We then write (cid:27)~n(cid:27) for the set of all residual strands of (cid:27)~ necessaryinformationtoreconstructthetransitionuniquely. with respect to (cid:27). Rule Cf describes the instantiation of a parametric Giventhesepreliminaryde(cid:12)nitions,acon(cid:12)guration over strand(cid:26)(~x;~n)withasubstitution(cid:24) forallitsvariablesthat ] ] Sisastructure((cid:27);(cid:27) )(cid:6) where(cid:27)isabundleoverS,and(cid:27) is are marked\fresh" (~n). Thesubstitutedconstants mustbe anextensionof(cid:27) whoseonlyadditional(cid:0)!-edgesoriginate distinct from each other and from any other value appear- ] ] in Fr((cid:27)), cover all of Fr((cid:27)), and point to (cid:27) n(cid:27), and (cid:12)nally ingin(cid:27)1. RuleCi realizesthesecondstageofinstantiation: ] thesignature (cid:6)listsall thesymbolsthatappear in (cid:27) (and it applies a substitution (cid:18) to the remaining variables ~x of (cid:27)). a partially instantiated strand (cid:26)[(cid:24)], checks that the atomic 3 formulasresultingfrominstantiatingtheconstraints(cid:25)(~x)of while A1(cid:0)(cid:14)A2 realizes resource A2 subject to the avail- ] (cid:26) with (cid:18) satisfy (cid:5), and install its initial node > in (cid:27)1 to ability of A1 while consuming A1 itself (this implements ] therefore the notion of transition). When instantiating produce (cid:27)2. We must perform instantiation in two stages quanti(cid:12)ers, we write [t=x]A for the capture-free substitu- to handle protocols where two parties exchange newly pro- tion of term t for variable x in formula A. We abbreviate ducednoncesasintheNeedham-Schroederprotocol inFig- [t1=x1]([t2=x2](:::[tn=xn]A))as [t1=x1;:::;tn=xn]A. ure 2. Contexts are(cid:12)nitemultisetsofcomma-separatedformu- Theremainingrulesdealwithmessagetransmissionand las. The empty context is denoted \(cid:1)". We will use the reception once a strand has beeninstalled in thecon(cid:12)gura- 0 00 letter (cid:0) and (cid:1), possibly subscripted, to indicate contexts. tion. Inparticular,(cid:23), (cid:23) and(cid:23) arenodesonfullyinstanti- atedstrands. RuleSmodelstheactionofsendingamessage: A signature (cid:6) is a list of constants. Thederivabilityjudgmentswewillrelyuponaresequents ifthecon(cid:12)gurationathandembedsastrandthatisnotfully of theform[17]: contained in the bundle part (cid:27)1 and the (cid:12)rst missing node (cid:0); (cid:1) ‘(cid:6) A (cid:23) is positive, we add an (cid:0)!-arrow to a matching negative 00 node (cid:23) and include (cid:23) in (cid:27)2. Receiving a message is mod- where the formulas in (cid:0) and (cid:1) are the resources available ] eled by rule R: if ((cid:27)1;(cid:27)1)(cid:6)1 mentions a strand that is not to produce the formula A. While the elements in (cid:1) shall fully contained in its bundle part and its (cid:12)rst missing node be used exactly once, the resources in (cid:0) can be exploited (cid:23) has an incoming (cid:0)!-edge,we add it tothe bundle. arbitrarily manytimes, possibly zero. This convenienttwo- Amultistep transition amountstochainingzeroormore context formulation [17] is rewritten as a more common one-steptransitions. Thisrelationisobtainedbytakingthe single-context sequent by augmenting (cid:1) with the result of ~o (cid:3) o re(cid:13)exiveandtransitiveclosure7(cid:0)!S of7(cid:0)!S,where~oisthe pre(cid:12)xing every formula in (cid:0) with the exponential modality sequenceofthecomponentmoves(\(cid:1)"ifempty). ~oisatrace \!" [16]. The signature (cid:6) lists all the constants mentioned of the computation. in the sequent. Although usually omitted in presentations Ourde(cid:12)nitionoftransitionpreservescon(cid:12)gurations, i.e. of (linear) logic, it simpli(cid:12)es ourtreatmentof nonces. ] ] o ] if((cid:27)1;(cid:27)1)(cid:6)1 isacon(cid:12)gurationand((cid:27)1;(cid:27)1)(cid:6)17(cid:0)!S((cid:27)2;(cid:27)2)(cid:6)2, The relevant inference rules for this language are dis- ] playedinFigure3. Therulesontheleft-handsidearecalled then ((cid:27)2;(cid:27)2)(cid:6)2 is also a con(cid:12)guration. Moreover, (cid:6)1 (cid:18)(cid:6)2. multiplicative. Ruleidwillbeusedattheleavesofaderiva- These properties extendtomultistep transitions. tion: itspeci(cid:12)es thatan object Acanbetrivially produced from A itself (the formulas in (cid:0) are ignored). Notice that 3 Elements of Linear Logic no excess resources are admitted. Rule (cid:0)(cid:14)l speci(cid:12)es how to use a resource A1(cid:0)(cid:14)A2 to build an object C: if A1 can Thetargetofourinterpretationofstrandconstructionswill be produced using part of the context ((cid:1)1), then A2 and beasublanguageoflinearlogic[16]. Wechoosethisformal- what remains of the context ((cid:1)2) are available to produce ismovermoretraditionallogicsbecauseofitsinterpretation C. Rule (cid:10)l states that a composite resource can be bro- of formulas as consumable resources. This provides, for ex- kentomakeitscomponentsindividuallyavailable,while(cid:10)r ample, a simple way of modeling the fact that receiving a speci(cid:12)es thatA1 (cid:10) A2 isproducedbybuildingitspartsin- messagemakesitunavailabletootherrecipients(unlessfur- dependently. Theconstant1isthenon-resource: itdoesnot ther actions are taken). contribute toa goal (rule 1l)anddoes requireanyresource Thislanguage,afragmentof(cid:12)rst-ordermultiplicativeex- to be established (rule 1r). Rule cut permits constructing ponentiallinearlogictobeprecise,isgivenbythefollowing anobjectinstages: inordertoobtainC,onecan(cid:12)rstbuild grammar: A with some of the available resources, and then use A to achieveC. SinceCcanalwaysbeproduceddirectlyfromthe A ::=P Atomic formulas original resources, this rule is e(cid:11)ectively redundant, which j1 Multiplicative unit we emphasize bydisplaying it in a shadedfont. jA1 (cid:10) A2 Multiplicative conjunction The right-hand side of Figure 3 shows rule dl (derelic- jA1(cid:0)(cid:14)A2 Linear implication tion), which makes a copy of a formula A in (cid:0) available in j8x:A Universal quanti(cid:12)cation (cid:1), and the rules concerning the quanti(cid:12)ers. Observe that j9x:A Existential quanti(cid:12)cation the existential quanti(cid:12)ers in the context(cid:1) are instantiated with new constants (rule 9l), which we record in the sig- P ::=N(m) Message in transit nature (cid:6). In the right-hand side of the turnstile (rule 9r), jPubK(k)j ::: Persistent information thesequanti(cid:12)ershaveinsteadthefunctionofhidingtheuse jQ(q) Intermediate step of these newly introduced constants. Notice that they are jstop Role completion instantiated with constants from (cid:6) rather than with arbi- We use messages and their constituents as the basis of the trary terms: this is su(cid:14)cient for our purposes. Instead, we term language of our formulas, as described in [7]. We rely allowuniversallyquanti(cid:12)edvariablestobeinstantiatedwith on the unary predicate symbol N to hold messages being arbitrary terms(rule 8l). exchanged, and we maintain the syntax we glimpsed at in theprevioussectionforpersistentinformation. Atomsofthe 4 Strands in Linear Logic formQ(q)identifyuniquelytheintermediate=)-edgesina con(cid:12)guration (see Section 4). Finally, the atomic constant We will now describe the translation of parametric strands stop will indicate the completionof a strand. and con(cid:12)gurations into the fragment of linear logic we just The connectives we will need are (cid:10), known as multi- discussed. We shall emphasize that this encoding does not plicative conjunction, the constant 1 (multiplicative unit), treat penetrator strands di(cid:11)erently from regular protocol (cid:0)(cid:14) or linear implication, and the usual quanti(cid:12)ers. A re- strands in any way. This adheres to the strand philosophy, source A1 (cid:10) A2 consists of the sum of parts A1 and A2, 4 Multiplicatives Exponentialsandquanti(cid:12)ers (cid:0);(cid:1)1 ‘(cid:6) A (cid:0);(cid:1)2;A ‘(cid:6) C (cid:0);A;(cid:1);A ‘(cid:6) C id cut dl (cid:0);A ‘(cid:6) A (cid:0);(cid:1)1;(cid:1)2 ‘(cid:6) C (cid:0);A;(cid:1) ‘(cid:6) C (cid:0);(cid:1)1 ‘(cid:6) A1 (cid:0);(cid:1)2;A2 ‘(cid:6) C (cid:0);(cid:1);[t=x]A ‘(cid:6) C (cid:0)(cid:14)l 8l (cid:0);(cid:1)1;(cid:1)2;A1(cid:0)(cid:14)A2 ‘(cid:6) C (cid:0);(cid:1);8x:A ‘(cid:6) C (cid:0);(cid:1);A1;A2 ‘(cid:6) C (cid:0);(cid:1)1 ‘(cid:6) A1 (cid:0);(cid:1)2 ‘(cid:6) A2 (cid:0);(cid:1);[c=x]A ‘(cid:6);c C (cid:0);(cid:1) ‘(cid:6);c [c=x]A (cid:10)l (cid:10)r 9l ((cid:3)) 9r (cid:0);(cid:1);A1 (cid:10) A2 ‘(cid:6) C (cid:0);(cid:1)1;(cid:1)2 ‘(cid:6) A1 (cid:10) A2 (cid:0);(cid:1);9x:A ‘(cid:6) C (cid:0);(cid:1) ‘(cid:6);c 9x:A (cid:0);(cid:1) ‘(cid:6) C 1l 1r (cid:0);(cid:1);1 ‘(cid:6) C (cid:0);(cid:1) ‘(cid:6) 1 ((cid:3)) cnotin(cid:6) Figure 3: RelevantRulesof Linear Logic andcontrastswithotherapproacheswhichsyntacticallydif- any other value in use. Applying this encoding to the ferentiate theintrudermodel(e.g. [6]). Needham-Schroederprotocolspeci(cid:12)edinFigure2yieldsthe Let(cid:26)(~n;~x;~y)beaparametricstrandwithconstraints\~n linear logic formulas inFigure 4. fresh, (cid:25)(~x)". Lets0;s1;:::;sn;sn+1 bethenodesof (cid:26),with In order to de(cid:12)ne the encoding of a con(cid:12)guration, we s0 =>, sn+1 =?, and for i=0::n, si =)si+1. We de(cid:12)ne need to extend this notation to partially and fully instanti- p q the encoding of node si (for i = 0::n+1), written si , as atedstrands. Let(cid:24)beasubstitutionforthe\fresh"variables follows: ~n of (cid:26). Then p q sn+1 =stop p q p q p q p q (cid:26)[(cid:24)] =[(cid:24);u0=q0;:::;un(cid:0)1=qn(cid:0)1]8~x;~y: s0 ; si =Q(qi(cid:0)1) (cid:10) (Q(qi(cid:0)1) (cid:10) N(m)(cid:0)(cid:14) si+1 ) if si=(cid:0)m p q p q where u0;:::;un(cid:0)1 are distinct constants. If furthermore (cid:18) si =Q(qi(cid:0)1) (cid:10) (Q(qi(cid:0)1)(cid:0)(cid:14)N(m) (cid:10) si+1 ) is a substitution for the remaining variables ~x;~y of (cid:26), we if si=+m p q p q de(cid:12)ne s0 =(cid:10)(cid:25)(~x)(cid:0)(cid:14)(cid:10)(cid:25)(~x) (cid:10) s1 p q p q (cid:26)[(cid:24);(cid:18)] =[(cid:18)]([(cid:24);u0=q0;:::;un(cid:0)1=qn(cid:0)1] s0 ): where, given a multiset of formulas (cid:1), (cid:10)(cid:1) is the formula obtained by taking the multiplicative conjunction of very p q Observe that (cid:18) can mention some of the constants newly element of (cid:1). For i = 1::n, si expresses the action in si p q introducedby(cid:24). Weextendthenotation si ,fori=0::n+ byplacing thesent(received)message min theconsequent 1,tothecasewheresiisanodeinafullyinstantiatedstrand (resp.antecedent)oftheimplication. Rule(cid:0)(cid:14)lwillhavethe (clearly, the qi’s will havebeenreplaced with ui’s). e(cid:11)ect of inserting (resp. removing) N(m) into (resp. from) We shall now encode con(cid:12)gurations. A con(cid:12)guration the context (cid:1). Notice that its application will also insert ] p q ((cid:27);(cid:27) )(cid:6) comprisesthreetypesofinformation: 1)anaccount si into (cid:1), enabling in this way the next action. This ofhowthissituationhasbeenreached(as(cid:27)andthestrands techniqueisknownascontinuation-passing style inthepro- ] in (cid:27) that have been instantiated, but not yet used); 2) a gramminglanguage community. descriptionofthecurrentsituation(inFr((cid:27)));and3)asum- The arguments of the conjuncts Q(q0);:::;Q(qn(cid:0)1) are ] distinctvariables. Itisconvenienttointerpretthemaslabels maryofthefutureactionsthatcanbeperformed(in(cid:27) n(cid:27)). for the =)-edges of (cid:26), as shown in Figure 2. The last ar- Wewill ignore the(cid:12)rstaspect sinceitwill bepartially cap- row,leadingtosn+1 =?,isinsteadlabeledwiththepropo- tured through the notion of derivation. The representation sitional letter stop. These atoms serve multiple purposes: ofFr((cid:27))willsimplybetheconjunctionofthemessagesinit (cid:12)rsttheyprovideawaytopreservetheorderofconsecutive (or 1 if none is present): message transmissions or receptions, which may prove im- p q Fr((cid:27)) =NHN(m):m2Fr((cid:27))I: portantfor someapplications; secondtheirpresencegreatly simpli(cid:12)esourproofsastheyimplementthe\locksandkeys" wherewewriteH:::Iforthemultisetequivalentoftheusual technique[23], whichhas yieldedfaithful representations of ] setnotationf:::g. Asfor(cid:27) n(cid:27),wetaketheconjunctionof variouscomputationalparadigmsinlinearlogic[22,23,24]; therepresentation of eachfully instantiated residual strand third, they are a crucial device for bridging the gap with in it, plus the representation of the strands that are only the multiset rewriting speci(cid:12)cation of a protocol [7]. Were partially instantiated: these reasons, in particular the (cid:12)rst one, to fall, a simpler encoding can be achieved by replacing the Q(qi)’s and stop p ] q p q ] (cid:27) n(cid:27) =NH si+1 :s=(cid:26)[(cid:24);(cid:18)] in (cid:27) ; with the linear logic constant 1. ] ingTthheeferneceovdainrigabolfes(cid:26)iinsapcsh0iqe:vedbyappropriatelyquantify- (cid:10)NHp(cid:26)[(cid:24)]q :(cid:26)s[i(cid:24)]2in(cid:27)S(cid:27);]Ia:ndsi+1 2(cid:27)Sn(cid:27)SI p q p q (cid:26) =9qo;:::;qn(cid:0)1:9~n:8~x;~y: s0 Forthesakeof conciseness, wede(cid:12)netherepresentation ] of a con(cid:12)guration ((cid:27);(cid:27) )(cid:6) as Existentially quantifying the qi’s, as well as ~n, guarantees p ] q p ] q p ]q that they will be instantiated with constants distinct from ((cid:27);(cid:27) )(cid:6) = Fr((cid:27);(cid:27) ) (cid:10) (cid:27)n(cid:27) : 5 (cid:0)1 (cid:0)1 (cid:0)1 9q0;q1;q2:9nA:8kA;kA ;kB;nB: (cid:10)(cid:25)A(kA;kA ;kB) (cid:0)(cid:14) (cid:10)(cid:25)A(kA;kA ;kB) (cid:10) Q(q0) (cid:10)( Q(q0) (cid:0)(cid:14) N(fkA;nAgkB) (cid:10) Q(q1) (cid:10)( Q(q1) (cid:10) N(fnA;nBgkA) (cid:0)(cid:14) Q(q2) (cid:10)( Q(q2) (cid:0)(cid:14) N(fnBgkB) (cid:10)stop))) 0 0 0 (cid:0)1 (cid:0)1 (cid:0)1 0 9q0;q1;q2:9nB:8kB;kB ;kA;nA: (cid:10)(cid:25)B(kB;kB ;kA) (cid:0)(cid:14) (cid:10)(cid:25)B(kB;kB ;kA) (cid:10) Q(q0) (cid:10)( 0 0 Q(q0) (cid:10) N(fkA;nAgkB) (cid:0)(cid:14) Q(q1) (cid:10)( 0 0 Q(q1) (cid:0)(cid:14) Q(q2) (cid:10) N(fnA;nBgkA) (cid:10)( 0 Q(q2) (cid:10) N(fnBgkB) (cid:0)(cid:14) stop))) Figure 4: Linear Logic Translation of the Needham-SchroederProtocol Wewill maketheencodingwe havejust presentedmore Proof: By induction on the structure of ~o. If the move se- concrete by means of an example. The upper part of Fig- quenceisprocessedright-to-left,weobtainacut-freederiva- ] ure 5 shows a con(cid:12)guration ((cid:27);(cid:27) ) representing an initial tion. Operating forward (left-to-right) requires the use of stage of Lowe’s attack [26] on the Needham-Schroederpro- the cut rule (whichcan subsequentiallybe eliminated). 2 tocol in Figure 2. It contains six strands: an initiator, a responder, and one instance of each of the four penetrator strands M0 (access to the intruder’s initial knowledge), D Intheaboveproof, eachmoveissimulatedbytheappli- (decryption), M (access to public information) and E (en- cationofanumberoflinearlogic rules. This(cid:12)nergranular- cryption). A detailed discussion of penetrator strands can ityisahindrancewhenconsideringaderivationthatrelates be found in [7]. Constants are indicated using a di(cid:11)erent the encoding of two con(cid:12)gurations, and trying to read o(cid:11) font than variables (e.g. nA as opposed to nA). In this con- the move sequences that have actually been applied: these (cid:12)guration,theinitiatorhasexecutedits(cid:12)rstaction,strands micro-steps can be intermingled in arbitrary ways. This M0 andD havebeencompleted,strandsM andE arefully forces us to break our completeness proof into a numberof instantiatedbutstillhavetoexecutetheir(cid:12)rstaction,while stages aimed at disentangling the given linear logic deriva- the responder strand has been only partially instantiated. tion. First we reduce ourselves to a purely multiplicative The only message in transit (thefringe) is (nA;kA). settingbypushingdlandthequanti(cid:12)errulesatthebottom ] of thegivenderivation. Thesecondboxin(cid:12)gure5showstheencodingof((cid:27);(cid:27) ) in linear logic. Observe that, whenever the border between ] Lemma 5.2 Let S be a set of parametric strands and (cid:27)Q(aun(cid:26)id)c(cid:27)orrnes(cid:27)pocnrodsisnegstaonthaectiinvteersstercatnedd,=t)he-eadtgoemaicppfoeramrsualas ((cid:27)1;(cid:27)1])(cid:6), ((cid:27)2;(cid:27)2])(cid:6);~n two con(cid:12)gurations over S. If there p ] q is a cut-free derivation D of the sequent a conjunct in (cid:27) n(cid:27) . Similarly, each terminated strand contributes an occurrence of stop. The residual of every p q p ] q p ] q active strand yields a formula with implications. Finally, S ; (cid:5); ((cid:27)1;(cid:27)1)(cid:6) ‘(cid:6) 9~n: ((cid:27)2;(cid:27)2)(cid:6);~n (cid:10) (cid:5) notice that the representation of the partially instantiated then there exists an instantiation of variables ~n with fresh responderstrandaccountsfortheonlyquanti(cid:12)ersappearing 0 ] in p((cid:27);(cid:27)])q. distinctconstants(cid:6),acon(cid:12)guration((cid:27)0;(cid:27)0)(cid:6);(cid:6)0,andacut- (cid:3) free derivation D of the sequent 5 Soundness and Completeness p q p 0 ] q S ;(cid:1)‘(cid:6);(cid:6)0 [(cid:6)=~n]((cid:27)2;(cid:27)2)(cid:6);(cid:6)0 (cid:10) (cid:5) We will now show that, given the above encoding, reach- p ] q p ] q ability among con(cid:12)gurations is mapped to the derivability where (cid:1)=(cid:5); ((cid:27)1;(cid:27)1)(cid:6) ; ((cid:27)0;(cid:27)0)(cid:6);(cid:6)0 , that does use nei- of their representation in linear logic, and vice versa. Con- ther dl nor any of the quanti(cid:12)er rules 8l, 9l, 9r. structing a derivation that mimics a sequence of moves in the strand world, formally stated in the following theorem, Proof: Weexploittherelativepermutabilityoftheseinfer- is fairly simple. encerules,asdescribedin[25]. Moreprecisely,weapplythe following four steps: Theorem 5.1 (Soundness) ] 1. We permute rule dl below every other rule. The re- Let S be a set of parametric strands and ((cid:27)1;(cid:27)1)(cid:6), ] sulting derivation consists then of a sequence of appli- ((cid:27)2;(cid:27)2)(cid:6);n~ two con(cid:12)gurations over S. If there is a move cations of dl followed bya subderivation D0 that does sequence ~o such that notuse thisrule. Theapplications of dl correspondto ] ~o (cid:3) 0 ] committingtotheparametricstrandsthatwillbeused ((cid:27)1;(cid:27)1)(cid:6)7(cid:0)!S;(cid:5)[(cid:6)=~n]((cid:27)2;(cid:27)2)(cid:6);(cid:6)0 toproduce((cid:27)2;(cid:27)2])(cid:6);~n (onceinstantiated,theywillcor- ] forsomeinstantiation ofvariables~nwithfreshdistinct con- respond to ((cid:27)0;(cid:27)0)(cid:6);(cid:6)0). 0 stants (cid:6),thenthere exists alinearlogicderivation D ofthe 0 2. Wepermuterule9ltothebottomofD,whichenables sequent 00 ustoconsiderasubderivationD thatdoesnotcontain p q p ] q p ] q theserules. Theseuses of9l correspondtopickingthe S ; (cid:5); ((cid:27)1;(cid:27)1)(cid:6) ‘(cid:6) 9~n: ((cid:27)2;(cid:27)2)(cid:6);~n (cid:10) (cid:5): 0 new constants thatappear in (cid:6) beforehand. 6 0 Initiator M D M E Responder (cid:0)1 (cid:0)1 (cid:0)1 (cid:0)1 (kA;kA ;kI;nA;nB) (kI ) ((nA;kA);kI;kI ) (kB) ((nA;kA);kB) (kB;kB ;kA;nB;nA) > > > > > > _ Q(qA0) Q(qM00) _ Q(qD0) fnA;kAgkI >fnA;kAgkI Q(qD1) Q(qE0) _ _ k(cid:0)I 1 >k(cid:0)I 1 Q(qM0) Q(qD2) Q(qB0) _ _ (nA;kA) >(nA;kA) Q(qA1) Q(qE1) _ _ kB kB Q(qE2) _ _ stop fnA;kAgkB fkA;nAgkB stop Q(qB1) _ _ fnA;nBgkA stop fnA;nBgkA Q(qA2) stop Q(qB2) _ _ fnBgkI fnBgkB stop stop _ _ _ _ _ _ ? ? ? ? ? ? p q N((nA;kA)) Fr((cid:27)) = A Q(u1) (cid:10) ( p(cid:27)]n(cid:27)q=8>>>>>>>>>>>>>>>>>>>>>>< (cid:10)(cid:10)(cid:10)(cid:10) ssQQttoo((uuppM0E0QQ))(((cid:10)uu(cid:10)A1E0QQ())(Q(((cid:10)(cid:10)uu(A2E1qNN))M0(cid:0)(((cid:10))(f(cid:14)n(cid:0)nNAN(cid:14)A;((;NkfknA(nBBkB))gB)g(cid:0)k)(cid:0)Ak(cid:14)I(cid:14))(cid:10))Q(cid:0)Q(cid:10)((cid:14)s(utuQE2osE1tp)()ou)(cid:10)pA2(cid:10))))(((cid:10) ( 9=;9>=IEMMDn(i((0(t((kninakBAAt(cid:0)I);o;1krk)A(Ak))A;;k;kBkI;(cid:0)A)k1(cid:0)I;1k)I;nA;nB) E >>>>>>>>>>>>>>>>>>>>>>: (cid:10) (8kB(cid:10);k(cid:25)B(cid:0)B1Q(;k(kBuAB0;QQ;k)nB(((cid:0)(cid:10)Auu12B1:;QN))k(cid:0)((cid:0)(Auf(cid:14)(cid:14))B2kNQ(cid:0))A((cid:14)(;(cid:10)funn(cid:10)B2AAN);(cid:25)g((cid:10)kkBfABn(gNBk)kgB(B(cid:0)fk)(cid:14);nBkQ(cid:10)A)B(cid:0)(;(cid:0)1usn(cid:14);tB1Boks)gpAtok)(cid:10))Ap)))(cid:10))())(cid:10))Q((uB0) (cid:10) ( >;9>>>=>>>;Responder(kB;kB(cid:0)1;kA;nB;nA) where pM0q= 9q0:8x: P0(x)(cid:0)(cid:14)P0(x) (cid:10) Q(q0) (cid:10) ( Q(q0)(cid:0)(cid:14)N(x) (cid:10) stop) pDq= 9q0;q1;q2:8m;k;k0: PrivK(k;k0)(cid:0)(cid:14)PrivK(k;k0) (cid:10) Q(q0) (cid:10) ( Q(q0) (cid:10) N(fmgk)(cid:0)(cid:14)Q(q1) (cid:10) ( Q(q1) (cid:10) N(k0)(cid:0)(cid:14)Q(q2) (cid:10) ( Q(q2)(cid:0)(cid:14)N(m) (cid:10) stop))) p q M = 9q0:8k: PubK(k)(cid:0)(cid:14)PubK(k) (cid:10) Q(q0) (cid:10) ( Q(q0)(cid:0)(cid:14)N(k) (cid:10) stop) p q E = 9q0;q1;q2:8m;k: PubK(k)(cid:0)(cid:14)PubK(k) (cid:10) Q(q0) (cid:10) ( Q(q0) (cid:10) N(m)(cid:0)(cid:14)Q(q1) (cid:10) ( Q(q1) (cid:10) N(k)(cid:0)(cid:14)Q(q2) (cid:10) ( Q(q2)(cid:0)(cid:14)N(fmgk) (cid:10) stop))) Figure 5: A Translation: Lowe’s attack on the Needham-SchroederProtocol 7 00 3. We permute rules 9r to the end of D , obtaining a id 000 subderivation D that does not mention these rules. 0 The applications of 9r correspond to hiding (cid:6) in the (cid:10)r overall derivation. (cid:10)l 4. Finally, we permute every use of 8r down past every (cid:3) (cid:10)l;:::;(cid:10)l;(cid:0)(cid:14)l otherrule,makingexplicitasubderivationD withthe 9 preleqtueirtehdecinhsatraancttieartisiotincso.f (T(cid:27)h0e;(cid:27)a0]p)(cid:6)p;l(cid:6)ic0a.tions of 8l com2- (cid:10)l;::::;:(cid:10):l;(cid:0)(cid:14)l >>= ; S=R 8l >>; ; Ci o When interpreted at the strand level, Lemma 5.2 speci(cid:12)es that amovesequencecanberearranged sothatparametric 9r strands are chosen and instantiated before any message is exchanged. More speci(cid:12)cally, all uses of Cf happen (cid:12)rst, 9l ; Cf o followed by all applications of Ci. Only then, can S- and dl R-movestakeplace. The next stepconsists ingrouping together the rule ap- plicationsthatcorrespondtoeachmoveinthemultiplicative Figure 6: Completeness Argument part of the given derivation. This provides a simple way of identifying movesS andR. Lemma 5.3 Let S be a set of parametric strands and A (cid:12)ne analysis of this proof reveals that linear logic ] ] derivationsenableaformofabstractionthatmovesequences ((cid:27)1;(cid:27)1)(cid:6), ((cid:27)2;(cid:27)2)(cid:6) two con(cid:12)gurations over S. If there is (cid:3) do not achieve. Indeed, the tree structure of a derivation a cut-free derivation D of the sequent doesnotalwaysimposeatotalorderonindependenttransi- p q p ] q p ] q tions. Thisisaverymildformofnon-determinismcompared S ; (cid:5); ((cid:27)1;(cid:27)1)(cid:6) ‘(cid:6) ((cid:27)2;(cid:27)2)(cid:6) (cid:10) (cid:5) withtheexplicitconcurrencypresentinbundles[7]. Weex- pecttoget amodel closer tobundlesbyconsidering graph- that uses only rules fromthe lefthalfofFigure 3,then there (cid:3)(cid:3) based formulations of linear logic such as proof nets [16]. exists a cut-free derivation D of this sequent such that Furthermore,game-theoreticinvestigationsoflinearlogic[2] (cid:15) Every use of (cid:10)r appear just below id, 1r or (cid:10)r; have produced methods for obtaining very strong forms of completeness which couldbe relevantin this setting. (cid:15) Rules 1l and (cid:10)l are applied eagerly. 6 Interpreting Multiset Rewriting in Linear Logic Proof: Again, we take advantage of the permutability re- sults in [25]. Rule (cid:10)r can be pushed up past any other In this section, we brie(cid:13)y describe how multiset rewriting rule (exceptid and 1r). Onthe other hand, (cid:10)l and 1l can techniquescanbeconvenientlyusedtoexpresssecuritypro- always be permuted down, as long as the nesting of sub- tocols (Section6.1). Wethenshow howtheresulting speci- formulas is respected (clearly if the left-hand side contains (cid:12)cationistranslatedintolinearlogicandstatetheexpected a formula (A (cid:10) B)(cid:0)(cid:14)C, a proof fragment that dismantles this formula mustapply (cid:10)l above (cid:0)(cid:14)l). 2 correctness results (Section 6.2). Finally, we compare the linear logic expressions we derive from the strand and mul- tiset rewriting speci(cid:12)cations of a protocol (Section6.3). Atthispoint,wehavethemeanstoextractasequenceof movesfromalinearlogicderivationthatrelatestheencoding 6.1 Multiset Rewriting for Cryptoprotocols of two con(cid:12)gurations. A multiset M is an unordered collection of objects or ele- ments, possibly with repetitions. The empty multiset does Theorem 5.4 (Completeness) ] not contain any object and will be written \(cid:1)". We accu- Let S be a set of parametric strands and ((cid:27)1;(cid:27)1)(cid:6), ] mulate the elements of two multisets M and N by taking ((cid:27)2;(cid:27)2)(cid:6);n~ two con(cid:12)gurations over S. If there is a linear theirmultisetunion,denoted\M;N". Theelementswewill logic derivation D of the sequent consider here will be (cid:12)rst-order atomic formulas A(~t) over p q p ] q p ] q some signature. S ; (cid:5); ((cid:27)1;(cid:27)1)(cid:6) ‘(cid:6) 9~n: ((cid:27)2;(cid:27)2)(cid:6);~n (cid:10) (cid:5) In its simplest form, a multiset rewrite rule r is a pair of multisetsF andG, respectivelycalledits antecedent and then there exists an instantiation of variables ~n with fresh 0 consequent. We will consider a slightly more elaborate no- distinct constants (cid:6) and a move sequence ~o such that tion in which F and G are multisets of (cid:12)rst-order atomic ] ~o (cid:3) 0 ] formulaswithvariablesamong~x. Weemphasizethisaspect ((cid:27)1;(cid:27)1)(cid:6)7(cid:0)!S;(cid:5)[(cid:6)=~n]((cid:27)2;(cid:27)2)(cid:6);(cid:6)0: by writing them as F(~x) and G(~x). Furthermore, we shall beabletomarkvariablesintheconsequentsothattheyare Proof: The use of Lemma 5.2 followed by Lemma 5.3 to instantiated to \fresh" constants, that have not previously D yields a derivation structured as in Figure 6, from which beenencountered,eveniftheruleisusedrepeatedly. Arule moves over con(cid:12)guration can easily be read o(cid:11) (shown on assumes thenthe form the rightof theschematic derivation). 2 r: F(~x)(cid:0)!9~n:G(~x;~n) 8 Initiator (cid:0)1 (cid:0)1 (cid:0)1 rA0: (cid:25)A0(KA;KA ) (cid:0)! A0(KA;KA );(cid:25)A0(KA;KA ) (cid:0)1 (cid:0)1 rA1: A0(KA;KA );(cid:25)A1(KB) (cid:0)! 9NA:A1(KA;KA ;KB;NA);N(fNA;KAgKB);(cid:25)A1(KB) (cid:0)1 (cid:0)1 rA2: A1(KA;KA ;KB;NA);N(fNA;NBgKA) (cid:0)! A2(KA;KA ;KB;NA;NB) (cid:0)1 (cid:0)1 rA3: A2(KA;KA ;KB;NA;NB) (cid:0)! A3(KA;KA ;KB;NA;NB);N(fNBgKB) Responder (cid:0)1 (cid:0)1 (cid:0)1 rB0: (cid:25)B0(KB;KB ) (cid:0)! B0(KB;KB );(cid:25)B0(KB;KB ) (cid:0)1 (cid:0)1 rB1: B0(KB;KB );N(fNA;KAgKB);(cid:25)B1(KA) (cid:0)! B1(KA;KB;KB ;NA);(cid:25)B1(A) (cid:0)1 (cid:0)1 rB2: B1(KA;KB;KB ;NA) (cid:0)! 9NB:B2(KA;KB;KB ;NA;NB);N(fNA;NBgKA) (cid:0)1 (cid:0)1 rB3: B2(KA;KB;KB ;NA;NB);N(fNBgKB) (cid:0)! B3(KA;KB;KB ;NA;NB) where (cid:25)A0(KA;KA(cid:0)1) = PubK(KA);PrvK(KA;KA(cid:0)1) (cid:25)B0(KB;KB(cid:0)1) = PubK(KB);PrvK(KB;KB(cid:0)1) (cid:25)A1(KB) = PubK(KB) (cid:25)B1(KA) = PubK(KA) Figure 7: Multiset Rewriting Speci(cid:12)cation of the Needham-SchroederProtocol where r is a label and 9~n indicates that the constants that Persistent information: We express persistent informa- instantiate~noughttobefresh. Amultiset rewriting system tionexactlyaswedidinthecaseofstrandsinSection2, R is a set of rewrite rules. i.e.bymeansof a multiset(cid:5) of ground facts. Rewriterulesallowtransformingamultisetintoanother We represent each role (cid:26) in a protocol by meansof a single multiset by making localized changes to the elements that role generation rule and a (cid:12)nite number of protocol execu- appear in it. Given a multiset of ground facts M over a tion rules. The purpose of the former is to prepare for the signature (cid:6), a rule r: F(~x)(cid:0)!9~n:G(~x;~n) is applicable if M = F(~t);M0, for terms ~t. Then, applying r to M yields execution of an instance of role (cid:26). Ithas theform themultisetN =G(~t;~c);M0 wheretheconstants~carefresh r(cid:26)0: (cid:25)(~x)(cid:0)!A(cid:26)0(~x);(cid:25)(~x): (inparticular,theydonotappearinM),~xand~nhavebeen where, as in previous sections, (cid:25)(~x) denotes a multiset instantiated with~tand~crespectively, andthefacts F(~t)in of persistent atomic formulas that may mention variables M havebeen replaced with G(~t;~c) to produce N. The new among ~x. Notice how persistent information is preserved. signature is (cid:6);~c. Wedenote theapplication of a single rule Theexecutionrulesdescribethemessagessentandexpected and of zero or more rewrite rules by means of the one-step by the principal acting in this role. For i =0:::l(cid:26)(cid:0)1, we and multistep transition judgments: havea rule r(cid:26)i+1 of either of thefollowing two forms: r ~r (cid:3) send: A(cid:26)i(~x);(cid:25)(~x;~z) M(cid:6)(cid:0)!RN(cid:6)0 M(cid:6)(cid:0)!RN(cid:6)0 (cid:0)! 9~n:A(cid:26)i+1(~x;~z;~n);N(m(~x;~z;~n));(cid:25)(~x;~z) 0 respectively, where (cid:6) and (cid:6) are the signatures over which receive: A(cid:26)i(~x);N(m(~x;~y));(cid:25)(~x;~y;~z) M andN arerespectivelyde(cid:12)ned. Thelabels r and~r iden- (cid:0)! A(cid:26)i+1(~x;~y;~z);(cid:25)(~x;~y;~z) tify which rule(s) have been applied and the terms ~t used to instantiate ~x. Thus, ~r acts as a complete trace of the where m(~v) stands for a message pattern with variables execution. among ~v. In the (cid:12)rst type of rules, we rely on the exis- tential operator 9~n to model the ability of a principal to Wemodelprotocolsbymeansofspeci(cid:12)callytailoredmul- create nonces when sending a message. This principal can tiset rewriting systems. Wecall this approachMSR. With- alsoincludesomepersistentdata~z (e.g.thenameandpub- out loss of generality, we consider here a slightly simpli(cid:12)ed lic key of an interlocutor), possibly related to information versionofthemodelintroducedin[6,12]. Werelyuponthe it already possesses (~x). In the second rule template, the following atomicformulas: principal should be able to access persistent information ~z related to data in the received message ~y (e.g. the sender’s Network messages: Network messages are modeled by public key) or previously known information ~x. Situations thepredicateN(m),wheremisamessagebeingtrans- whereaprincipalbothsendsandreceiveamessage,orsends mitted. multiplemessages, can easily be expressedbythese rules. Aprotocolisspeci(cid:12)edasasetRofsuchroles. Asanex- Role states: We (cid:12)rst choose a set of role identi(cid:12)ers ample,Figure7showstheencodingofourrunningexample (cid:26)1;:::;(cid:26)n for the di(cid:11)erent roles constituting the pro- in the MLR notation. tocol. Then, for each role (cid:26), we havea (cid:12)nite family of The behavior of the intruder according to the Dolev- role state predicates fA(cid:26)i(m~) j i = 0:::l(cid:26)g. They are Yao model [11, 34] is similarly speci(cid:12)ed as a set of rewrite intendedtoholdtheinternalstateofaprincipalinrole rules[6]. Wewill referto themas I. Astate is thena mul- (cid:26) duringthesuccessive steps of theprotocol. tisetofgroundfactsS =(cid:5);A;N;I,whereAisamultisetof Intruder knowledge: The adversary’s knowledge is held rolestates A(cid:26)i(~t),N ismultisetofmessages N(m)currently inadistributedwayinfactsoftheformI(m),wherem intransit, andI summarizestheintruder’sknowledgeI(m). is some piece of information captured or fabricated by Inparticulartheinitialstateisjust(cid:5);I0,whereI0 contains the intruder. theinformation (e.g. keys)initially knownto theintruder. 9

See more

The list of books you might like

Upgrade Premium
Most books are stored in the elastic cloud where traffic is expensive. For this reason, we have a limit on daily download.
DMCA & Copyright: Dear all, most of the website is community built, users are uploading hundred of books everyday, which makes really hard for us to identify copyrighted material, please contact us if you want any material removed.
Copyright @ PDFdrive.to, 2022 | We love our users