Automated verification of equivalence properties of cryptographic protocols
Rohit Chadha, University of Missouri
Vincent Cheval, University of Kent
S¸ tefan Ciob ˆac ˘a, University “Alexandru Ioan Cuza”
Steve Kremer, Inria Nancy - Grand-Est
Indistinguishability properties are essential in formal verification of cryptographic protocols. They are needed to model anonymity properties, strong versions of confidentiality and resistance against offline guessing attacks. Indistinguishability properties can be conveniently modeled as equivalence properties.
We present a novel procedure to verify equivalence properties for a bounded number of sessions of cryp- tographic protocols. As in the applied pi-calculus, our protocol specification language is parametrized by a first-order sorted term signature and an equational theory which allows formalization of algebraic properties of cryptographic primitives. Our procedure is able to verify trace equivalence for determinate cryptographic protocols. On determinate protocols, trace equivalence coincides with observational equivalence which can therefore be automatically verified for such processes. When protocols are not determinate our procedure can be used for both under- and over-approximations of trace equivalence, which proved successful on examples.
The procedure can handle a large set of cryptographic primitives, namely those whose equational theory is generated by an optimally reducing convergent rewrite system. The procedure is based on a fully abstract modelling of the traces of a bounded number of sessions of the protocols into first-order Horn clauses on which a dedicated resolution procedure is used to decide equivalence properties. We have shown that our procedure terminates for the class of subterm convergent equational theories. Moreover, the procedure has been implemented in a prototype tool A-KiSs (Active Knowledge in Security Protocols) and has been effec- tively tested on examples. Some of the examples were outside the scope of existing tools, including checking anonymity of an electronic voting protocol due to Okamoto.
Categories and Subject Descriptors: D.2.4 [Software Engineering]: Software/Program Verification; F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs; F.3.2 [Logics and Meanings of Programs]: Semantics of Programming Languages
General Terms: Security, Verification
Additional Key Words and Phrases: applied pi calculus, automated verification, process equivalence, security protocols
ACM Reference Format:
ACM-Reference-Format-JournalsACM Trans. Comput. LogicV, N, Article A (January YYYY), 33 pages.
DOI:http://dx.doi.org/10.1145/0000000.0000000
1. INTRODUCTION
Cryptographic protocols are distributed programs that rely on the use of cryptography to secure electronic transactions such as those that arise in electronic commerce and
Parts of this work has been done while the first, third and fourth author were affiliated to LSV, CNRS & Inria
& ENS Cachan and the second author was affiliated to LORIA, CNRS & Inria & Universit´e de Lorraine.
Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies show this notice on the first page or initial screen of a display along with the full citation. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is per- mitted. To copy otherwise, to republish, to post on servers, to redistribute to lists, or to use any component of this work in other works requires prior specific permission and/or a fee. Permissions may be requested from Publications Dept., ACM, Inc., 2 Penn Plaza, Suite 701, New York, NY 10121-0701 USA, fax+1 (212) 869-0481, or [email protected].
c
YYYY ACM 1529-3785/YYYY/01-ARTA $15.00 DOI:http://dx.doi.org/10.1145/0000000.0000000
wireless communication. They are also being applied in new domains such as in In- ternet voting. For example, French citizens living abroad were allowed to vote via the Internet in the parliamentary elections in 2012 [Fre 2015]. In Estonia, Internet voting has been allowed in parliamentary elections since 2007 [Est 2015]. Internet voting was also deployed in the state elections in New South Wales, Australia in 2015 [Halderman and Teague 2015]. This has led to increasing demands on the complexity of desired security properties, leading to more complex cryptographic protocols. Given the socio- economic-political consequences and the history of incorrect design of cryptographic protocols, the need for formal proofs of correctness of protocols is of great importance and has been widely recognized. Formal reasoning about cryptographic protocols is challenging as one has to reason against all potentially malicious behavior—all com- munication between protocol participants is assumed to be under the control of an adversary.
In order to make the task of formal analysis amenable to automation, usually the assumption of back-box cryptography and unbounded computational power on the part of the adversary is made. This adversarial model is often called the Dolev-Yao model as it is derived from the positions that Dolev and Yao took in their seminal paper [Dolev and Yao 1981]. It has proved extremely successful, and there are several automated tools [Blanchet 2001; Armando et al. 2005; Cremers 2008; Escobar et al. 2009] that can automatically check trace-properties such as (weak forms of) confidentiality and au- thentication. While these trace-based properties are certainly important, many crucial security properties can only be expressed in terms of indistinguishability (or equiv- alence). They include strong flavors of confidentiality [Blanchet 2004]; resistance to guessing attacks in password based protocols [Baudet 2005]; and anonymity proper- ties in private authentication [Abadi and Fournet 2004], electronic voting [Delaune et al. 2009b; Backes et al. 2008], vehicular networks [Dahl et al. 2010; Dahl et al. 2011]
and RFID protocols [Arapinis et al. 2010; Bruso et al. 2010]. More generally, indistin- guishability allows to model security by the means of ideal systems, which are correct by construction [Abadi and Gordon 1999; Delaune et al. 2009a]. Indistinguishability properties of cryptographic protocols are naturally modeled by the means ofobserva- tionalandtesting equivalencesin cryptographic extensions of process calculi, e.g., the spi [Abadi and Gordon 1999] and the applied-pi calculus [Abadi and Fournet 2001].
While we have good tools for automated verification of trace properties, the situation is different for indistinguishability properties. This paper is an attempt to address this concern.
State-of-the-art.Many results have been obtained in the restricted case of a pure eavesdropper, i.e., a passive adversary: forstatic equivalencemany decidability results have been shown [Abadi and Cortier 2006; Cortier and Delaune 2007; Arnaud et al.
2007] and exact [Baudet et al. 2009; Ciob ˆac ˘a et al. 2011] and approximate [Blanchet et al. 2005] tools exist for a variety of cryptographic primitives. In the case we con- sider indistinguishability in the presence of an active adversary, who can interact in an arbitrary way with honest participants less results are known. H ¨uttel [H ¨uttel 2002] showed undecidability of observational equivalence in the spi calculus, even for the finite control fragment, as well as decidability for the finite, i.e., replication-free, fragment of the spi calculus. The decidability result however only holds for a fixed set of cryptographic primitives and does not yield a practical algorithm. Current re- sults [Blanchet et al. 2005; Cheval and Blanchet 2013; Santiago et al. 2014] allow to approximate observational equivalence for an unbounded number of sessions. How- ever, this approximation does not suffice to conclude for many applications,e.g., [De- laune et al. 2009b; Arapinis et al. 2010]. Our approach overcomes these limitations for some applications in [Delaune et al. 2009b]. We still cannot conclude for the e-passport
example in [Arapinis et al. 2010], albeit for a different reason: our procedure does not currently handle else branches in protocols.
Symbolic bisimulations have also been devised for the spi [Borgstr¨om et al. 2004;
Borgstr¨om 2008; Tiu and Dawson 2010] and applied pi calculus [Delaune et al. 2010;
Liu and Lin 2010] to avoid unbounded branching due to adversary inputs. However, only [Delaune et al. 2010; Tiu and Dawson 2010] and [Borgstr¨om et al. 2004] yield a decision procedure, but again only approximating observational equivalence. The results of [Delaune et al. 2010] have been further refined to show a decision proce- dure on a restricted class of simple processes [Cortier and Delaune 2009]. In par- ticular they rely on a procedure deciding the equivalence of constraint systems, in- troduced by Baudet [Baudet 2005], for the special case of verifying the existence of guessing attacks. Baudet’s procedure allows arbitrary cryptographic primitives that can be modeled as a subterm convergent rewrite system [Abadi and Cortier 2006].
An alternate procedure achieving the same goal was proposed by Chevalier and Rusi- nowitch [Chevalier and Rusinowitch 2010]. However, both procedures are highly non- deterministic and do not yield a reasonable algorithm which could be implemented.
Therefore, Cheval et al. [Cheval et al. 2010] have designed a new procedure and a prototype tool to decide the equivalence of constraint systems, but only for a fixed set of primitives. Tools have also been implemented for checking testing equiva- lence [Durante et al. 2003], open bisimulation [Tiu and Dawson 2010] and trace equiv- alence [Cheval et al. 2011] for a bounded number of sessions but only a limited set of primitives. One may note that [Cheval et al. 2011] is the only decision procedure to consider negative tests, i.e., else branches, which are crucial in several case stud- ies [Arapinis et al. 2010; Abadi and Fournet 2004].
Our contribution. In this paper we introduce a new procedure for verifying equiv- alence properties for processes specified in a cryptographic process calculus (without replication). The messages in the calculus are modeled as terms equipped with an equational theory, similar to the applied pi calculus. Our main contributions are as follows.
— Our procedure checks for two equivalences which over- and under-approximate the standard notion of trace equivalence≈tfor cryptographic protocols: the under- approximation can be used to prove protocols correct while the over-approximation can be used to rule out incorrect protocols.
— Cortier and Delaune have shown in [Cortier and Delaune 2009] that observational equivalence coincides with≈tfor the class ofdeterminateprocesses. They also give a decision procedure for a strict sub-class of determinate processes, namely, sim- ple processes. We show that the coarser relation coincides with ≈t, and thus our procedure can be used to verify observational equivalence for the whole class of determinate processes.
— A novelty of our procedure is that it is based on a fully abstractmodeling of sym- bolic traces for aboundednumber of sessions infirst-order Horn clauses. This is in contrast to the constraint-solving techniques employed by Tiuet al.[Tiu and Daw- son 2010], Cheval et al. [Cheval et al. 2010; Cheval et al. 2011], Baudet [Baudet 2005] and Chevalier et al. [Chevalier and Rusinowitch 2010] for verifying under- approximations of observational equivalence. Techniques based on Horn clauses have been extensively used, e.g., by Blanchet [Blanchet 2001], Weidenbach [Wei- denbach 1999] and Goubault [Goubault-Larrecq 2005], in the case of an unbounded number of sessions. Affeldt and Comon [Affeldt and Comon-Lundh 2009] faithfully encode a bounded protocol into Horn clauses with rigid variables. Of these tools, only Blanchet [Blanchet 2001] can verify an equivalence property, which happens to be an under-approximation of observational equivalence. Horn clause modeling
of an unbounded number of sessions of security protocols may allow false attacks.
On the other hand, we have proven our modeling of a bounded number of sessions to be precise.
— Our modelling is fully abstract for arbitrary cryptographic primitives that can be modeled as a convergent rewrite system which has the finite variant property [Comon-Lundh and Delaune 2005; Escobar et al. 2012]. This allows us to handle a larger class of cryptographic primitives than [Tiu and Dawson 2010; Cheval et al.
2010; Cheval et al. 2011; Baudet 2005; Chevalier and Rusinowitch 2010]. Following our work, the recent work by Santiago et al. [Santiago et al. 2014] also provides support for rewrite systems which have thefinite variant property. They addition- ally cover associative-commutative theories, even though their experimental eval- uation suggests that these theories yield frequent non termination problems for the associative-commutative theories. Moreover, they only provide support for a re- stricted class of processes. We were also able to show termination of our procedure for the sub-class of subterm convergent rewrite systems. Please note that deduca- bility and hence static equivalence is undecidable even for the class of optimally reducing convergent rewrite systems [Anantharaman et al. 2007]. Optimally re- ducing convergent rewrite theories generalize subterm convergent rewrite systems, while maintaining the finite variant property. Moreover, even though our termina- tion proof does not apply, our tool terminated on specific protocols whose crypto- graphic primitives can be modeled as a convergent rewrite theories. These included the electronic voting protocols by Okamoto [Okamoto 1997] and Fujioka et al. [Fu- jioka et al. 1992] which use trapdoor commitment and blind signature respectively.
— Our procedure is implemented in the AKISS(Active Knowledge in Security proto- cols) prototype tool and we used it among others to successfully prove anonymity in an electronic voting protocol [Fujioka et al. 1992]. For this electronic voting protocol, this is the first automated proof.
An extended abstract of the paper [Chadha et al. 2012] authored by R. Chadha, S. Kremer and S¸ . Ciob ˆac ˘a appeared in the European Symposium of Programming in 2012. In addition to the proofs that were not present in the extended abstract, this paper also contains the proof of termination for subterm convergent rewrite theories.
The proof of termination is due to V. Cheval.
2. PRELIMINARIES
We recall some standard definitions and establish some notations that we shall be using throughout the paper.
2.1. Terms
Let F be a signature, i.e., a finite set of function symbols and let ar be a function which assigns to each function symbol a natural number. Given a function symbol f ∈ F, we say ar(f) ∈ N is the arity of f. A function symbol of arity 0 is called a constant. Given a set of atoms A and a signature F, we denote by TF,A the set of terms built inductively fromAby applying functions symbols inF. Given sets of atoms A1,A2, . . . ,An, we denote the setTF,∪1≤i≤nAibyTF,A1,A2,...An.We assume that we have the following countably infinite pairwise disjoint sets: a setN of private names, a set Mofpublic names, a setCof publicchannel names, a setWofparameters, and a setX of message variables. Intuitively, elements of the setN represent nonces generated by honest principals of a protocol, elements ofMrepresent nonces available both to the adversary and to the honest participants and elements ofC represent names of public channel (e.g. the name of a public network). Elements ofW are pointers used by the adversary to refer to messages output by the honest participants in a protocol. We fix
an enumeration w1,w2, . . .of the elements ofW. We letx, y, z range overX. We also define the following sets.
Definition 2.1. The set TF,N,M,W,X, denoted Terms, is the set of all terms, the
set TF,N,M, denoted Messages, is the set of messages and the set TF,N,M,X, denoted
SMessages, is the set ofsymbolic messages.
Iftis a term, we denote byvars(t)the set of variables appearing int, bynames(t)the set of names (public or private) appearing intandst(t)the set of all subterms oft. The functionsvars,names andstare extended as expected to sequences and sets of terms.
Apositionis a string of positive natural numbers anddenotes the empty string. The set pos(t) of positions of a term t is defined as usual [Baader and Nipkow 1998]. If p∈pos(t)thent|pis the subterm oftat positionp.
Example 2.2. Consider the signatureF ={enc,dec,pair,fst,snd}wherear(enc) = 3, ar(dec) = ar(pair) = 2 and ar(fst) = ar(snd) = 1. The term t = pair(enc(a, k1, r1),enc(b, k2, r2)) models the pair of the encryptions of public names a and b with keys k1, resp. k2 and randomness r1, resp. r2. The set of positions pos(t) ={,1,11,12,13,2,21,22,23}andt|=t,t|1=enc(a, k1, r1)andt|23=r2.
Substitutions. A substitution is a partial function σ : W ∪ X → Terms. We only consider substitutions which map elements ofWto elements inMessagesand elements ofX to elements ofSMessages.The domain ofσ, denoted bydom(σ), is defined as usual:
dom(σ) ={o∈ W ∪X |σ(o)6=o}.For our purposes, we only consider substitutions with finite domains. We letrange(σ) ={σ(u)∈ T |u∈dom(σ)}.Ifdom(σ) ={u1, u2, . . . , un} andti =σ(ui)for each1 ≤i ≤nthen we shall writeσas{u1 7→t1, . . . , un 7→tn}.σ is said to begroundifrange(σ)⊆Messages.The notationnames(σ)will denote the set names(range(σ)).A substitutionσcan be extended to a (total) functionσext:W ∪ X → Termsby lettingσext(x) =xifx /∈dom(σ)andσext(x) =σ(x)ifx∈dom(σ).As usual,σ extends homomorphically to a functionapplyσ :Terms →Termsobtained by “applying”
σexthomomorphically. Givent∈Terms, we denoteapplyσ(t)bytσ.Ifσis a substitution andX ⊆ W∪X, we denoted byσ[X]the substitution whose domain is restricted at most toX. Given two substitutionsσandτ, the substitution obtained bycomposingσand τ, denotedστ, is the unique substitution such thatστ(x) = (σ(x))τfor allx∈ W ∪ X. 2.2. Rewriting and unification
Two termssandtare (syntactically)unifiableif there exists a substitutionσsuch that sσ=tσ. We denote bymgua function which associates to any two unifiable termssand ta most general unifierσofsandtsuch thatσ=σ[vars(s, t)]. It is well known [Baader and Nipkow 1998; Baader and Snyder 2001] that for any two unifiable termssandt, there is a most general unifier, unique up to variable renaming.
A rewrite systemRis a set of rewrite rules of the form`→rwhere`, r∈Messages, names(l, r) =∅andvars(r)⊆vars(`). A termtcan be rewritten in one step tou, denoted t→R u, if there exist a positionp∈pos(t), a rule`→rinRand a substitutionσsuch thatt|p =`σanduis obtained fromt by replacing the subtermt|pbyrσ.→∗R denotes the transitive and reflexive closure of→R. A rewrite system is said to be confluentif for any t, t1, t2 such thatt →∗R t1 and t →∗R t2 there existsu such thatt1 →∗R uand t2 →∗R u. A rewrite system is said to be terminatingif it does not admit any infinite sequencet0 →R t1 →R t2 →R . . .. It is said to beconvergentif it is both confluent and terminating. In a convergent rewrite systemR, for every termtthere is a unique term t0such thatt→∗Rt0 and there is nousuch thatt0 →Ru. t0is said to be thenormal form oft.We denote byt↓R the normal form of the termt. Two termssandtare said to be
equal moduloR, writtens=Rt, ifs↓R=t↓R. Given a substitutionσwe denote byσ↓Ra substitution such thatdom(σ↓R)⊆dom(σ)and for allu∈dom(σ), σ↓R(u) =σ(u)↓R.
Example 2.3. Continuing Example 2.2, consider the rewrite system R = {dec(enc(x, y, z), y)→ x,fst(pair(x, y))→x,snd(pair(x, y))→y}. The first rewrite rule models that a message can be decrypted, provided decryption uses the same key (repre- sented by variabley) as encryption. The two last rules model projection of the first and second component of a pair. Then we have thatt = fst(pair(dec(enc(a, k, r), k), b))→R
fst(pair(a, b))→Ra=t↓R.
We recall the notions of optimally reducing [Narendran et al. 1997] and subterm convergent[Abadi and Cortier 2006] rewrite systems.
Definition 2.4. A rewrite systemRis said to be optimally reducingif for any ` → r ∈ Rand any substitutionθ such that all proper subterms of`θ are in normal form, we have thatrθis in normal form.
Definition 2.5. A rewrite systemRis said to besubterm convergentifRis conver- gent and for each rule`→r∈R, we have that eitherr∈st(`)orris a constant.
We immediately note that any subterm convergent rewrite system Rcan be easily converted into an equivalent optimally reducing rewrite system by replacing every rewrite rule`→rinRby`→r↓R.
Example 2.6. The rewrite system R = {dec(enc(x, y, z), y) → x,fst(pair(x, y)) → x,snd(pair(x, y))→y}given in Example 2.3 is subterm convergent. We shall give exam- ples of convergent rewrite systems that are not subterm convergent when we discuss the case studies on electronic voting in Section 6.2.
Remark 2.7. WhenRis clear from the context or unimportant we will simply drop the subscriptRin→Rand↓R.
2.3. The finite variant property
Given a convergent rewrite system, we now define the notion of complete set of vari- ants, which was introduced by Common-Lundh and Delaune [Comon-Lundh and De- laune 2005]. Our notion is slightly stronger than the notion defined in [Comon-Lundh and Delaune 2005] and was first introduced in [Escobar et al. 2012]. See [Cholewa et al. 2014] for a comparison of the various definitions of variants.
Definition 2.8. A set of substitutions variants(t1, . . . , tk) is called a complete set of variants of the terms t1, . . . , tk if for any substitution ω there exist σ ∈ variants(t1, . . . , tk) and a substitution τ such that for all 1 ≤ j ≤ k we have that ω[vars(tj)]↓= (σ↓τ)[vars(tj)]and(tjω)↓= (tjσ)↓τ.
Intuitively if variants(t) = {σ1, σ2, . . . σk} then the set of terms preterms(t) = {tσ1↓, tσ2↓, . . . , tσk↓ } represent pre-computations of all possible instances oft in the following sense: If ω is a substitution and tω is the term tω↓ then there is a term t0 ∈ preterms(t)and a substitutionτ such thatt0τ is thesyntactictermtω.No rewrite rules are needed to computetωfromt0τ.
Example 2.9. Consider the rewrite system introduced in Example 2.3 and lett = dec(fst(x), y). We have thatvariants(t) ={∅, σ1, σ2}where∅denotes the identity substi- tution and
σ1={x7→pair(z1, z2)}, and σ2={x7→pair(enc(z1, y, z2), z3)}
Intuitively, the substitution ∅ covers the cases where both the decryption and pro- jection may fail, σ1 corresponds to the situation where the projection succeeds, but decryption may fail, andσ2 accounts for the situations where both projection and de- cryption succeed. Note that the case where projection fails and decryption succeeds is not possible.
In [Ciob ˆac ˘a 2011], Ciob ˆac ˘a presents an algorithm for computing such complete sets of variants which is correct whenever the rewrite system isoptimally reducing[Naren- dran et al. 1997]. Optimally reducing rewrite systems include subterm convergent systems [Abadi and Cortier 2006] (and hence the classical Dolev Yao theories for en- cryption, signatures and hash functions), as well as a theory for modeling blind sig- natures [Kremer and Ryan 2005]. Moreover, complete sets of variants can be used to perform unification moduloR[Escobar et al. 2012; Ciob ˆac ˘a 2011].
Definition 2.10. Given sets of terms{si}i∈I and{ti}i∈I,letX =vars({si, ti}i∈I). A set of substitutions mguR({si
=? ti}i∈I)is called acomplete set of unifiers moduloRof the system of equations{si
=? ti}i∈I if each of the following holds:
(1) dom(σ)⊆vars(X)for eachσ∈mguR({si
=? ti}i∈I) (2) siσ=Rtiσfor eachi∈Iand for eachσ∈mguR({si
=? ti}i∈I).
(3) For any substitutionθsuch thatsiθ=Rtiθfor everyi∈I, there exists a substitution σ∈mguR({si
=? ti}i∈I)and a substitutionτwithθ[X] =R (στ)[X].
For singleton systems, we also writemguR(s, t)instead ofmguR({s=? t}).
For the remaining of the paper, we assume that the rewrite system is convergent and has the finite variant property.
2.4. Frames, deducibility and static equivalence
Recall that we have fixed an enumerationw1,w2, . . .of the elements of the setW. As in [Abadi and Fournet 2001], we will use the notion of aframeto represent messages which have been recorded by the attacker.
Definition 2.11. A frame ϕ is a substitution {w1 7→ t1, . . . ,wn 7→ tn} where ti ∈ Messages(1≤i≤n).
Intuitively, wi in a frame points to the i-th message recorded by the attacker in a protocol run. Note that in our definition, every frame with|dom(ϕ)|=nhasdom(ϕ) = {w1, . . . ,wn}. We denote the set of all frames as Frames. The adversary can use the public names as well as recorded messages to construct new messages. This is modeled as the deducibility relation.
Definition 2.12. Any term inTF,M,W is said to be arecipe. We say thata messaget is deducible fromϕwith a reciper(written asϕ`r t) ift ∈Messagesandrϕ=R t. We writeRecipesfor the setTF,M,W.
Intuitively, the recipe r tells how the attacker can construct the message t from the recorded messages. Note that the same termtcan be constructed using different recipes. A frameϕ0 ={w17→t01, . . . ,wm7→t0m}extendsa frameϕ={w17→t1, . . . ,wn7→
tn}ifm≥nand ift0i =tifor all1 ≤i ≤n. It is easy to see that ifϕ0 extendsϕand if ϕ`rtthenϕ0`rt.
Example 2.13. Consider the signatureF and the rewrite systemRin Example 2.3.
Letϕ={w17→enc(s, k, r),w27→k}wheres, k, r∈ N are private names. Then we have
thatϕ`dec(w1,w2) s. Note thatdec(w1, k)6∈Recipesask ∈ N. If we had thats∈ Mwe would also have thatϕ`ssreflecting that public names are always deducible.
We now recall static equivalence of frames [Abadi and Fournet 2001] to capture indistinguishability of frames. Recall that two terms can be indistinguishable to an attacker even if the two terms are distinct. For example,0encrypted using a symmetric key unknown to the attacker and1encrypted using the same key are indistinguishable to the attacker. Thus, instead of checking of direct equality between messages, the attacker can perform a series of tests to distinguish between two frames. This is the intuition behind the following definition:
Definition 2.14. Letr1, r2∈Recipes. Atestr1
=? r2holdsin a frameϕ(written(r1 = r2)ϕ) ifϕ`r1 tandϕ`r2 tfor somet,i.e.,r1andr2are recipes for the same term inϕ.
Frames ϕ1 and ϕ2 are statically equivalent (written ϕ1 ≈s ϕ2) iff for all r1, r2 ∈ Recipeswe have that(r1=r2)ϕ1iff(r1=r2)ϕ2.
Example 2.15. Leta, b∈ Mandr, k, k0 ∈ N. We have that{w1 7→enc(a, k, r),w27→
k} 6≈s {w1 7→enc(b, k, r),w2 7→k}because the test (dec(w1,w2)=? a)distinguishes the two frames. However,{w17→enc(a, k, r),w27→k0} ≈s{w17→enc(b, k, r),w27→k0}.
3. A CRYPTOGRAPHIC PROCESS CALCULUS
We shall assume that cryptographic protocols are modeled using a simple process cal- culus which has similarities with the applied pi-calculus [Abadi and Fournet 2001].
The applied pi-calculus has proven to be useful for specifying and verifying crypto- graphic protocols; there are tools that automate verification of protocols in this model [Blanchet 2001]. We shall further restrict our attention to the finite,i.e., replication- free fragment of applied pi-calculus. This restriction is important because observa- tional equivalence becomes undecidable with replication [H ¨uttel 2002]. With this re- striction, one can model a bounded number of protocol instances.
In this section we define our process calculus. We begin by defining its syntax.
Syntax. Recall that we have fixed a first-order signatureF, a setN ofprivate names, Mofpublic names, a setCof public channel names, a setWofparameters, and a setX of message variables (see Section 2). The terms of the setTF,N,M,W,Xare also identified modulo a fixed subterm convergent rewrite systemR(see Section 2).
We model a bounded number of instances of a cryptographic protocol as afiniteset of traces. Traces are defined using sequences of actions generated by the following grammar (note that hereinandoutare fresh symbols not occurring inF):
a ::= in(c, x) receive action out(c, t) send action [s=? t] test action
wherex∈ X, s, t∈SMessages, c∈ C. AtraceT is a sequence of actionsT =a1.a2. . . . .an. As usual, a receive action in(c, x) acts as a binding construct for the variable x. We assume the usual definitions of free and bound variables for traces. We also assume that each variable is bound at most once. A trace isgroundif it does not contain any free variables. The set of ground traces shall be represented as GndTraces. We also assume the usual definition of a name occurring in a trace.
AprocessP is defined to be a set of tracesP ={T1, . . . , Tn}. We say that a process is ground if all of its traces are ground. We identify traces with singleton processes.
Remark 3.1. Contrary to the applied pi calculus [Abadi and Fournet 2001] we do not have anν operator for generating new names: as we only consider a finite number of sessions we can simply use private names inN. We have also not explicitly included the parallel operator|and the choice operator+. One could include these and generate the corresponding set of traces. Thus, there is no loss in expressivity. However, we note that an explicit enumeration of the traces can result in an exponential number of traces.
Semantics. The semantics of a process is defined using the semantics of its traces.
The semantics of a trace is given in terms of a labeled transition systemT. We assume that all interactions between protocol participants are mediated by the adversary. The labeled transition system records the interaction of the protocol participants with the adversary. The set of labels ofT is defined using the set Recipes. Recall that the set Recipesis the setTF,M,W (see Section 2). The set of labels,Labels, is
Labels={in(c, r),out(c),test|r∈Recipes, c∈ C }.
The labeled transition system T is a subset of (GndTraces ×Frames) ×Labels × (GndTraces×Frames)and we shall write(T, ϕ)−→` (T0, ϕ0)whenever((T, ϕ), `,(T0, ϕ0))∈ T.The frame in the transition system is used to record the messages that the protocol participants have sent in the past. The relation−→` is defined as follows:
RECEIVE
ϕ`rt
(in(c, x).T, ϕ)−−−−→in(c,r) (T{x7→t}, ϕ)
SEND
(out(c, t).T, ϕ)−−−−→out(c) (T, ϕ∪ {w|dom(ϕ)|+17→t})
TEST s=Rt
([s=? t].T, ϕ)−−→test (T, ϕ)
The labelin(c, r)indicates a message sent by the adversary over the channelcand ris the recipe that adversary uses to create this message. The labelout(c)indicates a message sent over the public channel c and the transition rule SEND records the message sent in the frame. Finally, the rule TESTis an internal action.
As usual, we shall write (T0, ϕ0) −−−−−→`1,...,`n (Tn, ϕn) when (T0, ϕ0) −→`1 (T1, ϕ1). . . −→`n (Tn, ϕn) and we say that`1. . . `n is a runof (T0, ϕ0). We shall write(T, ϕ) =⇒` (T0, ϕ0) when either (T, ϕ) test
∗,`,test∗
−−−−−−−−→ (T0, ϕ0) and ` 6= test or (T, ϕ) test
∗
−−−→ (T0, ϕ0) and ` = test, wheretest∗denotes an arbitrary number oftestactions. We write(T, ϕ)====`1,...,`⇒n (Tn, ϕn)when(T, ϕ)=⇒`1 (T1, ϕ1)=⇒`2 . . . =`⇒n (Tn, ϕn). IfP ={T1, . . . , Tm}is a process, we write (P, ϕ) −−−−−→`1,...,`n (T0, ϕ0)(resp. ====`1,...,`⇒n (T0, ϕ0)) if there exists a traceT ∈ P such that(T, ϕ)−−−−−→`1,...,`n (T0, ϕ0)(resp.(T, ϕ)====`1,...,`⇒n (T0, ϕ0)).
Process equivalences.In this section we will define various flavors of trace equiva- lence which will be useful in this paper. We first recall the standard definition of trace equivalence in cryptographic process algebras.
Definition3.2 (Trace equivalence). A ground processP is said to betrace-included in a ground process Q(written P vt Q) if whenever (P,∅) ====`1,...,`⇒n (T, ϕ)then there
exist T0, ϕ0 such that (Q,∅) ====`1,...,`⇒n (T0, ϕ0) andϕ ≈s ϕ0. Two processes P andQ are trace-equivalent(writtenP ≈tQ) ifPvtQandQvtP.
We will also define two other notions of trace equivalence, one coarser and one more fine-grained. The coarser trace equivalence, which we denote by≈ctis the trace equiv- alence that can actually be verified by our procedure.
Definition3.3 (Coarse trace equivalence). Given ground processesPandQ, we say thatP vctQif whenever(P,∅)====`1,...,`⇒n (T, ϕ)and(r1=r2)ϕfor some recipesr1, r2then there existT0, ϕ0 such that(Q,∅)====`1,...,`⇒n (T0, ϕ0)and(r1 =r2)ϕ0. We say thatP ≈ctQ ifP vctQandQvctP.
The following example illustrates the difference between≈tand≈ct. Example 3.4. LetP andQbe the ground processes defined as follows:
P = {out(c, a).out(c, a)}and
Q = {out(c, a).out(c, a), out(c, a).out(c, b)}
ClearlyP vctQ. Observe also thatQvctP. Indeed, only trivial equalities hold on the frame{w1 7→a,w2 7→b}, and therefore these also hold on{w1 7→a,w2 7→a}. Thus, we have thatP≈ctQwhileP6≈tQ.
We will however show that these two notions coincide for a class ofdeterminate pro- cesses. In the context of the applied pi calculus determinate processes were previously studied by Cortier and Delaune in [Cortier and Delaune 2009].
Definition3.5 (Determinate process). We say that a ground process P is determi- nateif whenever(P,∅)====`1,...,`⇒n (T, ϕ)and(P,∅)====`1,...,`⇒n (T0, ϕ0)thenϕ≈sϕ0.
Intuitively, determinate processes are processes in which the adversary’s static knowl- edge at any instance is completely determined by its past interaction with the protocol participants. The following is immediate from the definition.
PROPOSITION 3.6. A ground trace, i.e, a ground process consisting of single trace, is determinate.
As already mentioned above, it was demonstrated in [Cortier and Delaune 2009] that trace equivalence coincides with observational equivalence for determinate processes.
We show that≈tand≈ctalso coincide for this class of processes.
THEOREM 3.7. If P and Q are ground processes then P ≈t Q implies P ≈ct Q.
Furthermore ifP andQare determinate, thenP ≈ctQimpliesP ≈tQ.
PROOF.
(⇒) Follows immediately from definition of≈tand≈ct.
(⇐) Let P and Qbe determinate processes. We need to show that P ≈ct Q implies P ≈tQ. We proceed by contradiction. Suppose thatP ≈ctQandP 6≈tQ. We suppose P 6vt Q(the case ofQ6vtP being symmetric). AsP 6vt Qwe have that there exist
`1, . . . , `n,T,ϕ, such that(P,∅)====`1,...,`⇒n (T, ϕ)and
(1) either there exist noϕ0, T0 such that(Q,∅)====`1,...,`⇒n (T0, ϕ0),
(2) or for allϕ0, T0such that(Q,∅)====`1,...,`⇒n (T0, ϕ0)we have thatϕ6≈sϕ0.
In the first case we have thatP 6≈ct Q, contradicting our hypothesis. In the second case, asϕ 6≈s ϕ0, there existr, r0 such that(r =r0)ϕand(r 6=r0)ϕ0 (or vice-versa, the other case is symmetric). AsP vctQ, we have that there existT00, ϕ00such that
(Q,∅)====`1,...,`⇒n (T00, ϕ00)and(r=r0)ϕ00. AsQis determinate, we have thatϕ0 ≈sϕ00. This yields a contradiction, as(r6=r0)ϕ0and(r=r0)ϕ00would implyϕ06≈sϕ00. Additionally, we introduce a more fine-grained notion of trace equivalence, denoted
≈ft.
Definition3.8 (fine-grained trace equivalence). Given ground processes P and Q, we say that P vft Q if for each trace T ∈ P there exists a trace T0 ∈ Qsuch that T ≈tT0. We say thatP ≈ft QifP vft QandQvftP.
It follows directly from the definition that ≈ft⊂≈t. The difference between these two relations is illustrated by the following example.
Example 3.9. LetP andQbe ground processes defined as follows:
P ={ out(c, enc(a, k)).out(c, enc(b, k)).in(c, x).[x=enc(a, k)].out(c, k), out(c, enc(a, k)).out(c, enc(b, k)).in(c, x).[x=enc(b, k)].out(c, k)}
Q ={ out(c, enc(a, k)).out(c, enc(b, k)).in(c, x).[x=enc(dec(x, k), k)].out(c, k)}
where k ∈ N is a private name anda, b are constants. The test x = enc(dec(x, k), k) simply checks whether x is an encryption with key k. It is not difficult to see that P ≈tQbutP 6≈ft Q.
As already mentioned our procedure is able to check ≈ct which coincides with ≈t
when processes are determinate. In the case where processes are not determinate we can use our procedure to check≈ct and≈ft in order to over- and under-approximate
≈t. Indeed, as traces are determinate processes a procedure for checking ≈ct can be used to verify≈ft.
4. MODELING TRACES AS HORN CLAUSES
Our decision procedure is based on a fully abstract modelling of a trace in first-order Horn clauses. We give the details of this modelling; we start by giving some definitions that we need for defining the predicates used in the logic.
Symbolic labels and symbolic runs.We define the set ofsymbolic labelsas SLabels={in(c, t),out(c),test|t∈SMessages, c∈ C}
and the set ofsymbolic runs, SRuns, as the set of finite sequences of symbolic labels (see Figure 1). The empty sequence is denoted by . Sometimes we simply write (empty space) for. Intuitively, a symbolic label stands for a set of possible labels, and a symbolic run stands for a set of possible runs of the protocol.
Symbolic Recipes. We assume a set Y of recipe variables disjoint from X. The set of terms TF,M,W,Y shall be called symbolic recipes and denoted by SRecipes. We use capital lettersX, Y, Zto range overY. Intuitively, a symbolic recipe stands for a set of recipes.
We extend the definition of substitutions to include variables fromY in its domain.
However, we only consider substitutions that map variables inYtoSRecipes. A ground substitution must map variables inYtoRecipes.The notion of most general unifiers is extended to symbolic recipes as expected.
Predicates. The predicates used in our modelling and the semantics of the predicates are given in Figure 1. The ground predicates are interpreted over a pair– a traceT and a frameϕ.A predicatePwith free variables, is interpreted over a triple- a traceT,a frameϕand a substitutionσ:
(T, ϕ0, σ)|=Piff(T, ϕ0)|=Pσ.
We consider four kinds of predicates, all of which have a symbolic run as an argument.
Intuitively, thereachability predicate rw says that each run represented bywis pos- sible, i.e., does not block due to a test that fails. The intruder knowledge predicate kw(R, t)says that whenever a run represented bywhappens, the (symbolic) messaget can be constructed by the intruder using the (symbolic) recipeR.The identity predicate iw(R, R0)says that whenever the (symbolic) runwis executed, the (symbolic) recipes RandR0are recipes for the same (symbolic) term. Observe that the termtin the defi- nition of the predicateiw(R, R0), if it exists, must be unique (moduloR). The reachable identity predicateriw(R, R0)is a short form for the conjunction of the predicatesrwand iw(R, R0).
Formulas and statements. We consider first-order formulas built using the above predicates and the usual connectives (conjunction, disjunction, negation, implication, existential and universal quantification). As in the case of predicates, a formula is interpreted over a triple consisting of a traceT, a frame ϕand a substitution σ; and the semantics is defined as expected.
Note that in case f is a ground formula, we shall omit σ as we do not need the substitutionσ. If in addition to f being ground, we have that dom(ϕ) =∅, we simply writeT |=f for(T,∅)|=f.
Symbolic Runs (w∈SRuns, `∈SLabels):
w:=|`, w
Predicates (w∈SRuns, R∈SRecipes, t∈SMessages):
rw (Reachability predicate) kw(R, t) (Intruder knowledge predicate) iw(R, R0) (Identity predicate)
riw(R, R0) (Reachable identity predicate)
Semantics for ground predicates (`i∈SLabels, R∈SRecipes, t∈SMessages, T ∈GndTraces, ϕ∈Frames):
(T, ϕ0)|=r`1,...,`n if(T, ϕ0)−L−→1 (T1, ϕ1)−L−→2 . . .−−→Ln (Tn, ϕn) such that`i=RLiϕi−1for all1≤i≤n (T, ϕ0)|=k`1,...,`n(R, t) if when(T, ϕ0)−L−→1 (T1, ϕ1)−L−→2 . . .−−→Ln (Tn, ϕn)
such that`i=RLiϕi−1for all1≤i≤n thenϕn`Rt
(T, ϕ0)|=i`1,...,`n(R, R0) if there existstsuch that (T, ϕ0)|=k`1,...,`n(R, t)and (T, ϕ0)|=k`1,...,`n(R0, t)
(T, ϕ0)|=ri`1,...,`i(R, R0) if(T, ϕ0)|=r`1,...,`nand(T, ϕ0)|=i`1,...,`n(R, R0) Fig. 1:Predicates
We now identify a subset of the formulas, which we shall callstatements. Statements will take the form of Horn clauses, and we shall be mainly concerned with them.
Definition 4.1. Astatementis a Horn clause of the formH ⇐B1, . . . , Bnwhere:
(1) H ∈ {rl1,...,lk,kl1,...,lk(R, t),il1,...,lk(R, R0),ril1,...,lk(R, R0)}.
(2) For each1≤i≤n, Bi=kl1,...,lji(Xi, ti)
for some l1, . . . , lk ∈ SLabels, t ∈ SMessages, R, R0 ∈ SRecipes, ji ≤ k, t1, . . . , tn ∈ SMessages and X1, . . . , Xn ∈ Y.Furthermore X1, . . . , Xn are distinct variables and if H =k`1,...,`k(R, t)thenvars(t)⊆vars(t1, . . . , tn).
We implicitly assume that in a Horn clause all variables are universally quantified.
Hence, all statements are closed formulas.
Remark 4.2. We sometimes abuse language and callσa closing substitution for a statementH ⇐B1, . . . , Bnifσis closing for each of the formulasH, B1, . . . Bn.
Remark 4.3. Letf =H ⇐B1, . . . , Bnbe a statement.
— f is said to be areachability statementifHis of the formrl1,...,lk.
— f is said to be adeduction statementifH is of the formkl1,...,lk(R, t).
— f is said to be anequational statementifH is of the formil1,...,lk(R, R0).
— f is said to be areachable identity statementifHis of the formril1,...,lk(R, R0).
4.1. The set of seed statements
As mentioned above, our decision procedure is based on a fully abstract modelling of a trace in first-order Horn clauses. In this section, given a trace T we will give a set of statementsseed(T)which will serve as a starting point for the modelling. We shall also establish that the set of statements seed(T)is a sound and (partially) complete abstraction of the traceT.In order to formally defineseed(T), we start by fixing some notational conventions.
Let T = a1.a2. . . . .an be a ground trace. We assume w.l.o.g. the following naming conventions:
(1) ifaiis a receive action thenai=in(ci, xi).
(2) xi6=xj for anyi6=j.
(3) ifaiis a send action thenai =out(ci, ti).
(4) ifaiis a test action thenai= [si
=? ti].
Moreover, for each1≤i≤nlet`i∈SLabelsbe as follows:
`i=
in(ci, xi) ifai=in(ci, xi) out(ci) ifai=out(ci, ti) test ifai= [si
=? ti] .
For each 0 ≤ m ≤ n, let the sets RcvT(m), SendT and TestT(m) respectively denote the indices of the receive actions, send actions and test actions amongst a1, . . . , am. Formally,
RcvT(m) = {i|1≤i≤m, ai=in(ci, xi)}
SendT(m) = {i|1≤i≤m, ai=out(ci, ti)}
TestT(m) = {i|1≤i≤m, ai= [si=? ti]}
.
Given a set of public names M0 ⊆ M, theset of seed statementsassociated toT and M0, denotedseed(T,M0), is defined to be the set of statements given in Figure 2. If M0=M, thenseed(T,M)is said to be the set of seed statements associated toT and in this case we writeseed(T)as a shortcut forseed(T,M).
Remark 4.4. Please note that while constructing the set of seed statements, we apply the most general unifier modulo Rto all tests. In addition, we also apply finite variants. This allows us toget ridof rewriting in our procedure.
Example 4.5. As an example consider the signatureF ={pair,fst,snd,h,a}where ar(pair) = ar(h) = 2,ar(fst) = ar(snd) = 1, andar(a) = 0equipped with the rewrite systemR={fst(pair(x, y))→x,snd(pair(x, y))→y}and the trace
T =in(c, x).[fst(x)=? a].out(c,h(s,snd(x))).out(c, s).
Note thatsis a private name. The setseed(T,∅)(ignoring public names) consists of the following clauses:
rin(c,x)⇐k(X, x) (1)
rin(c,pair(a,x)).test⇐k(X,pair(a, x)) (2) rin(c,pair(a,x)).test.out(c)⇐k(X,pair(a, x)) (3) rin(c,pair(a,x)).test.out(c).out(c)⇐k(X,pair(a, x)) (4) kin(c,pair(a,x)).test.out(c)(w1,h(s, x))⇐k(X,pair(a, x)) (5) kin(c,pair(a,x)).test.out(c).out(c)(w2, s)⇐k(X,pair(a, x)) (6)
kw(a,a)⇐ (7)
kw(fst(Y),fst(y))⇐kw(Y, y) (8) kw(fst(Y), y1)⇐kw(Y,pair(y1, y2)) (9) kw(snd(Y),snd(y))⇐kw(Y, y) (10) kw(snd(Y), y2)⇐kw(Y,pair(y1, y2)) (11) kw(pair(Y1, Y2),pair(y1, y2))⇐kw(Y1, y1),kw(Y2, y2) (12) kw(h(Y1, Y2),h(y1, y2))⇐kw(Y1, y1),kw(Y2, y2) (13) wherew∈ {u| ∃v. uv=in(c,pair(a, x)).test.out(c).out(c)}.
We may note that in the first block of 4 reachability statements (1–4), in order to satisfy the test[fst(x)=? a], the attacker needs to be able to construct a pairpair(a, x).
This condition is obtained by computing mguR({fst(x) = a}) = {x 7→ pair(a, x)}.
The second block of clauses adds a knowledge clause for each send action in the trace. The third block of clauses represents the attacker capabilities. It computes the set of variants on f(y1, . . . , yk)for each function symbolf in the signature, e.g., variants(fst(x)) ={∅,{x7→pair(x, y)}}(where∅denotes the identity substitution).
We shortly show that the set of seed statements is a sound and (partially) complete modelling of a trace. However, we need one more definition to state this fact.
Definition 4.6. LetKbe a set of statements. We defineH(K)to be the smallest set of ground terms such that:
SIMPLECONSEQUENCE
f =
H ⇐B1, . . . , Bn
∈K
σgrounding forf B1σ∈ H(K) . . . Bnσ∈ H(K) Hσ∈ H(K)
EXTENDK ku(R, t)∈ H(K) kuv(R, t)∈ H(K)
(Equivalently, H(K) is the least Herbrand model of K ∪ {k`1,...,`n+1(X, x) ⇐ k`1,...,`n(X, x)}n∈N.)
r`1στ↓,...,`mστ↓⇐ {k`1στ↓,...,`j−1στ↓(Xj, xjστ↓)}j∈RcvT(m)
for all0≤m≤n
for allσ∈mguR({sk=tk}k∈TestT(m)) for allτ∈variants(`1σ, . . . , `mσ)
k`1στ↓,...,`mστ↓(w|SendT(m)|, tmστ↓)⇐ {k`1στ↓,...,`j−1στ↓(Xj, xjστ↓)}j∈RcvT(m)
for allm∈SendT(n)
for allσ∈mguR({sk=tk}k∈TestT(m)) for allτ∈variants(`1σ, . . . , `mσ, tmσ) k(c, c)⇐
for all public namesc∈ M0
k`1,...,`m(f(Y1, . . . , Yk), f(y1, . . . , yk)τ↓)⇐ {k`1,...,`m(Yj, yjτ↓)}j∈{1,...,k}
for all0≤m≤n
for all function symbolsf of arityk for allτ∈variants(f(y1, . . . , yk)).
Fig. 2:Seed statements
We show that as far as reachability predicates and intruder knowledge predicates are concerned, the setseed(T)is a complete abstraction of a trace (please see the Elec- tronic Appendix for the proof):
THEOREM 4.7. LetT be a ground trace.
— (Soundness.) For any statementf ∈seed(T)∪ H(seed(T)),T |=f.
— (Completeness.) If(T,∅)−−−−−−→L1,...,Lm (S, ϕ)then:
(1) rL1ϕ↓,...,Lmϕ↓∈ H(seed(T)).
(2) ifϕ`RtthenkL1ϕ↓,...,Lmϕ↓(R, t↓)∈ H(seed(T)).
Remark 4.8. Please note that the setseed(T)is only partially complete in that we have not shown in Theorem 4.7 that ifϕ `R tandϕ `R0 t theniL1ϕ↓,...,Lmϕ↓(R, R0) ∈ H(seed(T)).
We will shortly show how the completeness ofseed(T)can be built upon to achieve a) full abstraction of the traceT and b) a procedure for checking equivalences≈ctand
≈ft.
5. PROCEDURE FOR DECIDING TRACE EQUIVALENCE
We shall now describe a procedure for deciding trace equivalence. At a high level, this consists of two steps.
(1) A saturation procedure which constructs a set ofsimple statements from the set seed(T)which we will callsolvedstatements. The saturation procedure ensures that the set of solved statements is a complete abstraction ofT.
(2) Given two processesP andQ, we saturate the set of seed statements for traces of P andQand then use the solved statements to decide whetherP andQare trace equivalent.
We shall now give the details of the procedure. We start by the saturation procedure.
5.1. Knowledge bases and saturation
The saturation procedure manipulates a set of statements called a knowledge base:
Definition 5.1. Given a statementf =H ⇐B1, . . . , Bn,
— f is said to be solvedif for all1 ≤ i ≤ n,Bi = k`1,...,`ji(Xi, xi)for some variables xi∈ X, Xi∈ Y.
— f is said to bewell-formedif one of the following holds:
(1) f is not solved.
(2) f is a solved reachability, equational and reachable identity statement.
(3) f is a solved deduction statement such that ifH =k`1,...,`k(R, t)thent6∈ X. A set ofwell-formedstatements is called aknowledge base. IfK is a knowledge base, we define Ksolved = {f ∈ K | f is solved} to be the knowledge base restricted to the solved statements.
Given an initial knowledge baseK, the saturation procedure produces another knowl- edge basesat(K).The saturation procedure proceeds as follows. First new statements aregeneratedand then the knowledge base isupdatedwith the new statements. This two-step process continues until a fixed-point is achieved. We describe the two steps in the procedure.
Generating new statements. Given a knowledge baseK, new statementsf are gen- erated by applying the rules in Figure 3. Each of the rule generates a new statementh.
The rule RESOLUTIONapplies the standard rule of resolution from first-order logic to an unsolved and a solved deduction statement and allows us to propogate constraints imposed from a partial execution of a trace to its possible extensions. The rule EQUA-
TIONallows us to derive new identities on recipes that may be imposed by the execu- tion of the protocol. The rule TESTallows us to conclude which identities necessarily hold in an execution of the protocol. Once the statement h is generated, we update the knowledge base K with h. The process of updatingK with h, denoted K⊕h, is explained below.
RESOLUTION
f ∈K, g∈Ksolved, f =
H ⇐kuv(X, t), B1, . . . , Bn g=
kw(R, t0)⇐Bn+1, . . . , Bm
σ= mgu(ku(X, t),kw(R, t0)) t6∈ X K:=K⊕hwhereh=
(H ⇐B1, . . . , Bm)σ
EQUATION
f, g∈Ksolved, f =
ku(R, t)⇐B1, . . . , Bn
g=
ku0v0(R0, t0)⇐Bn+1, . . . , Bm
σ= mgu(ku(, t),ku0(, t0))
K:=K⊕hwhereh=
(iu0v0(R, R0)⇐B1, . . . , Bm)σ
TEST
f, g∈Ksolved, f =
iu(R, R0)⇐B1, . . . , Bn
g=
ru0v0 ⇐Bn+1, . . . , Bm
σ= mgu(u, u0)
K:=K⊕hwhereh=
(riu0v0(R, R0)⇐B1, . . . , Bm)σ
Fig. 3:Saturation rules
