The spi-calculus is a formal model which allows to reduce the verification of security properties of cryptographic protocols to the verification of observational equivalences between spi processes. In this paper we prove that hedged bisimilarity, which is equivalent to barbed equivalence, is decidable on finite spi-calculus processes. The algorithm we provide works with any term equivalence satisfying a simple set of conditions, thus encompassing many different encryption schemata.
finite spi-calculus processes; to this end, we will introduce the notion of canonical processes as canonical representatives of congruence classes. Finite canonical processes can be analyzed to determine the (finite) space of terms and names which have to be considered at each step of the bisimulation game. Based on this result, we provide the algorithm for the verification of hedged bisimulation. 2
The spi-calculus extends the -calculus terms with primitives for encryption and decryption. Formally, let N be a countable set of names (typically of channels) ranged over by a; b; c; : : : , and V a countable set of variable symbols, ranged over by x; y; z; : : : . The set of spi-calculus terms is given by the grammar A ::= a j x
t ::= A j (t1; t2) j 1(t) j 2(t) j ft1gt2 j Dt2 (t1) ::= true j : j 1 ^ 2 j [t1 = t2] j isname(t) j ispair(t) j isenc(t) Intuitively, ft1gt2 denotes the term t1 encrypted using key t2, and (t1; t2) is the pair composed by t1 and t2. The decryption Dt2 (t1) opens t1 using the key t2, and 1(t), 2(t) are the two projections. We call the encryption and pairing operators constructors, and the projection and decryption operators destructors.
We denote by fv(t), n(t) the sets of (free) variables and names in term t,
respectively. As usual, a term t is ground if fv(t) = ;. A ground term is moreover
said to be a message whenever no destructor appears in it. We denote with T
and G respectively the sets of all terms and ground terms. M denotes the set of
all messages, ranged over by M; N; : : : . Lastly, ranges over boolean expression,
where [t1 = t2] is the equality test between terms and isname(t), ispair(t) and
isenc(t) check whether a term t is a name, a pair of an encryption respectively.
These last three operators, not present in the original definition [
Moreover, we extend further the calculus by abstracting from the syntactical
equality normally used for [t1 = t2], see [
Ground terms are taken up-to some computable structural congruence =. We can think of two terms in the same equivalence class of = as being computationally equivalent, i.e. executing the encryption/decryption algorithms on them leads to the same value. With this novelty we aim to account for different types true : B t : 1 i(t) : i
: B : : B 2 i = 1; 2 1 : B 2 : B
1 ^ 2 : B t1 : t2 : N ft1gt2 : C( ) [t1 = t2] : B t1 : C( ) t2 : N
Dt2 (t1) : isname(t) : B ispair(t) : B
isenc(t) : B of encryption schemata, which can be expressed by considering different = as long as, for any t : 1 and t0 : 2 such that t = t0, it respects the three properties: 1. Type equivalence t and t0 have the same type, i.e. 1 = 2; 2. Key equivalence the same names are used as keys and, by changing any of them with a fresh name we obtain two equivalent terms. Formally, keys(t) = keys(t0) ^ 8a 2 keys(t)8b 2 N n (n((t; t0))) : tfb=ag = t0fb=ag where tfb=ag is the substitution replacing all occurrences of a in t with b. 3. Deterministic decryption erasing all encryptions and decryption and applying the same projections leads to the same term, i.e. after applying the rewriting rules i((t1; t2)) ! ti, Dt2 (t1) ! t1 and ft1gt2 ! t1 in all subterms of t and t0 we obtain two syntactically equivalent terms.
It is easy to check that the equivalence used in [
We extend fv on processes, so that fv(P ) is the set of free variables occurring in
P , and denote with fn(P ) the set of free names of P (i.e. names not occurring in
the scope of a ( m) operator). The syntax above is the usual one from -calculus
[
Processes of the spi-calculus are taken up-to the usual structural congruence familiar from the -calculus theory and shown in Figure 2.
QjP (P jQ)jR
P (QjR) P +Q
Q+P (P +Q)+R
P +(Q+R) ( m)(P jQ) ( m)P jQ if m 62 fn(Q) ( m)( n)P ( n)( m)P
P and Q are -equivalent
P Q
P P + R
Q Q + R
P ( m)P
Q ( m)Q
P Q
Q P
P
P
P jR Q Q P R
Q QjR R
To define the operational semantics of the spi-calculus we need to evaluate ground terms and boolean expressions. The evaluation is defined over well-typed terms, where each type denotes a set of values. The interpretation of base types is defined as I(N) = N and I(B) = ftrue; falseg, whereas for pairs and encryptions it is defined as:
I( 1
I(C( )) = ffM ga j M 2 I(C( )); a 2 N g==
2) = f(M1; M2) j M1 2 I( 1); M2 2 I( 2)g==
Definition 2 (Evaluation). The evaluation for well-typed ground terms and
boolean expressions is a partial function [[ ]] defined recursively as follows:
[[a]] = a 2 N
[[true]] = true
[[ 1 ^ 2]] = [[
2) for some 1 and 2; false otherwise
[[isenc(t1)]] = true if [[t1]] 2 I(C( )) for some ; false otherwise
Following [
well-typed [[ ]] = true :P > P
t well-typed [[t]] = v let x = t in P > P fv=xg
P > P 0 P P 0 Then, the late operational semantics of the spi-calculus is represented by a labelled transition relation P ! Q, where 2 fa; a j a 2 N g [ f g is the name of a channel (for both input and output) or the silent transition (also called -transition), and Q ranges over processes, concretions and abstractions (see below). The rules of this operational semantics are in Figure 3. (input)
a 2 N a(x)P a! (x)P (output) t well-typed [[t]] = M ahtiP a! ( )hM iP (interaction) (restriction)
P P
P jQ
! D ( m)P (sum)
P P + Q ! P 0 ! P 0 n! (x)P 0 Q
n! ( m)hM iQ0 ! ( m)(P 0fM=xgjQ0)
fmg \ fn(P 0) = ; 62 m [ m ! ( m)D (equivalence)
(parallel) P
Q Q
P P jQ ! P 0 ! P 0jQ ! Q0 Q0
P 0 P ! P 0
Concretions are “message-continuation” pairs resulting from an output: a process executing an output transition yields the concretion ( )hM iQ (where ( ) is a restriction on a empty set of names) which can be seen as a process ready to send a message and to continue as Q. On the other hand, an abstraction (x)P is a “process with a hole”, resulting from an input transition; it can be seen as process waiting to receive a message M and continue as P fM=xg. An abstraction (x)P and a concretion ( m)hM iQ, where m is a list of names, can synchronize resulting in a process where the message M is received by (x)P . In order to define this interaction, we need to extend restriction and parallel composition operators to abstractions and concretions, as follows: ( a)( m)hM iP , ( m)(x)P , (x)( m)P (( a; m)hM iP ( m)hM i( a)P if n 2 fn(M ) otherwise Rj(x)P , (x)(RjP )
where x 62 fv(R) Rj( m)hM iP , ( m)hM i(RjP ) where fmg \ fn(R) = ;
As usual, we denote with P =) Q the transitive closure of the -transition whereas P =) Q denotes P =) ! Q. 3
We now define the hedged bisimilarity, firstly introduced in [
Here (and afterward), we abuse the projection operators i to be used on any tuple, also outside of the calculus. The first condition requires a consistent hedge to match names with names. The second one requires that elements are taken up to equivalence on terms =. The last one requires that all encrypted messages cannot be decrypted using keys in h: encrypted messages in a consistent hedge cannot be reducible. Alongside hedges, we define synthesis, analysis, irreducible. The synthesis of a hedge h is the set of message pairs that can be built from h. Definition 4 (Synthesis). The synthesis S(h) of a hedge h is the least set s.t.: – h S(h); – if (M; N ) 2 S(h), (k; j) 2 S(h) and k; j 2 N then (fM gk; fN gj) 2 S(h); – if (M1; N1) 2 S(h) and (M2; N2) 2 S(h) then ((M1; M2); (N1; N2)) 2 S(h). We write h ` M $ N for (M; N ) 2 S(h), and in this case we say that M and N are homologous w.r.t. h.
The analysis of a hedge is the set of all message pairs obtained by “opening" the messages of h via decryption or projection. The irreducible are those elements in the analysis of a hedge that cannot be reduced further. Formally: Definition 5 (Analysis). The analysis A(h) of a hedge h is the least set s.t.: – h A(h); – if (fM gk; fN gj) 2 A(h) and (k; j) 2 A(h) then (M; N ) 2 A(h); – if ((M1; N1); (M2; N2)) 2 A(h) then (M1; M2) 2 A(h) and (N1; N2) 2 A(h). Moreover, we define the irreducible I(h) of a hedge h as
I(h) , A(h) n (f(C; D) 2 A(h) j C = fM gk; D = fN gj; (k; j) 2 A(h)g [ f((M1; N1); (M2; N2)) 2 A(h)g) It should be noted that all elements that can be reduced in the analysis can be derived from the irreducible via synthesis, i.e. S(I(h)) = S(A(h)). Lastly, since every hedge is a finite set, its analysis and irreducible are also finite.
A hedged relation R is a subset of H P P, where P is the set of all processes. We write h ` P RQ when (h; P; Q) 2 R. Moreover, we say that R is consistent if, for all h 2 H, h ` P RQ implies that the hedge h is consistent. Definition 6 (Hedged simulation). A consistent hedged relation R is a hedged simulation if, whenever h ` P RQ we have that: – if P ! P 0 then there exists Q0 such that Q =) Q0 and h ` P 0RQ0; – if P a! ( m)hM iP 0 and m \ (fn(P ) [ n( 1(h))) = ; then there exist b 2 N and a concretion ( n)hN iQ0 such that h ` a $ b, n\(fn(Q)[n( 2(h))) = ;, Q =)b ( n)hN iQ0 and I(h [ f(M; N )g) ` P 0RQ0;
a! (x)P 0 then there exist b 2 N and an abstraction (y)Q0 such that
h ` a $ b, Q =)b (y)Q0 and for all B N finite such that B \ (fn(P ) [
fn(Q) [ n(h)) = ; and h [ idB is consistent, for all pairs (M; N ) of ground
terms, if h [ idB ` M $ N then h [ idB ` P 0fM=xgRQ0fN=yg.
The first condition requires that for each -transition from P there is a path of
-transitions from Q such that the two target processes are in the simulation R.
The second condition requires that for each output transition of P , labelled with
a, there is an output transition from Q labelled with b (and possibly preceded by
some silent transitions); moreover, a and b are homologous in h and the processes
after the two output operations are paired in R w.r.t. a consistent hedge that
extends h by pairing the two messages M and N . The last condition requires
that for each input transition of P with label a, there is an input transition from
Q labelled with b (and possibly preceded by some silent transitions); moreover,
a and b are homologous in h and for all finite set B of fresh names w.r.t. P ,
Q and h, the abstractions (x)P 0 and (x)Q0 are paired in the simulation R for
each input messages (M; N ) homologous by h [ idB. Hedges simulation leads
to the definition of hedged bisimulation and bisimilarity. Remarkably, hedged
bisimilarity coincides with barbed equivalence [
Definition 7 (Hedged bisimulation/bisimilarity). A hedged simulation R is a hedged bisimulation if R 1 = f(h 1; Q; P ) j h ` P RQg is also a hedged simulation (where h 1 = f(N; M )j(M; N ) 2 hg). The hedged bisimilarity, written , is the greatest hedged bisimulation, i.e. the union of all hedged bisimulations. 4
Clearly, bisimilarity is undecidable for general processes (see [
The idea behind our result, and similar to that in [
Before formalizing this idea, we introduce a canonical form of processes and show that any process can be translated into an equivalent one in canonical form. Definition 8 (Canonical form). A process P is in canonical form if in P – any [t1 = t2] is such that t1 and t2 are variables or messages; – constructors do not occur inside terms t of let x = t in Q operators; – destructors do not occur inside any term t of output operators ahtiQ; – for any occurrence of isname(t), ispair(t) and isenc(t) in P , t is a variable. Proposition 1. For all P there is a canonical process Q such that P Q.
The proof is based on defining a rewriting system on processes which preserves congruence and terminates on canonical processes. Thanks to this result, we can restrict ourselves to processes in canonical form without loss of generality.
For terms and boolean expressions, we define their maximal constructor depth. Intuitively, this depth is related to the maximum size of messages that can satisfy a boolean expression when replacing a free variable appearing in it. Definition 9 (Maximal constructor depth). The maximal constructor depth mcd(t) of a term t is defined inductively by the clauses mcd(n) = 0 mcd(x) = 0 mcd((t1; t2)) = max(mcd(t1); mcd(t2)) + 1 mcd(ft1gt2 ) = mcd(t1) + 1 and then extended to boolean formulas as follows: mcd(true) = 0
mcd(: ) = mcd( ) mcd([x = y]) = 0 mcd(ispair(x)) = 1 mcd( 1 ^ 2) = max(mcd( 1); mcd( 2)) mcd([x = M ]) = mcd(M ) mcd(isname(x)) = 1
mcd(ispair(x)) = 1 Definition 10 (k-homologous). Given h 2 H and M; N 2 M, we define h `k M $ N
4 () h ` M $ N and k = max(mcd(M ); mcd(N )) Whenever h `k M $ N we say that M and N are k-homologous in h. The notion of k-homologous terms allows us to deduce an upper bound on the number of names that are required to prove that h ` M $ N .
Lemma 1. Let h 2 H and M; N 2 M be such that max(mcd(M ); mcd(N )) = k. If there is a finite set of names B N such that B \ n(h) = ;, h [ idB is consistent and h [ idB `k M $ N , then there exists B0 N such that jB0j 2k and satisfying the same three properties.
Proof. Suppose jBj 2k and that h ` M $ N does not hold, otherwise the lemma is trivially satisfied. We have that M and N are in the synthesis S(h[idB) and, at worst, all names in M and N are in B. As k = max(mcd(M ); mcd(N )) and both encrypt and pairing are binary constructors, M and N can be represented as binary trees with height k and with therefore at most 2k leafs. Hence B can be reduced to a set B0 such that jB0j 2k and h [ idB0 `k M $ N . As B0 B, it also holds that h [ idB0 is consistent and B0 \ n(h) = ;. tu Lemma 1 leads to the notion of d-hedged bisimilarity : a hedged bisimilarity where size of messages and number of fresh names are bounded. We define first the corresponding simulation; differences with Definition 6 are put in boxes. Definition 11 (d-hedged simulation). For any integer d 0, a consistent hedged relation R is a d-hedged simulation if whenever h ` P RQ we have that: – if P ! P 0 then there exists Q0 such that Q =) Q0 and h ` P 0RQ0; – if P a! ( m)hM iP 0 and m \ (fn(P ) [ n( 1(h))) = ; then there exist b 2 N and a concretion ( n)hN iQ0 such that h ` a $ b, n\(fn(Q)[n( 2(h))) = ;, b
Q =) a( n)hN iQ0 and I(h [ f(M; N )g) ` P 0RQ0; – if P ! (x)P 0 then there exist b 2 N and an abstraction (y)Q0 such that h ` a $ b, Q =)b (y)Q0 and for all B N , where jBj 2d , B \ (fn(P ) [ fn(Q) [ n(h)) = ; and h [ idB is consistent, for all pairs (M; N ) of ground terms, if 9k d h [ idB `k M $ N then h [ idB ` P 0fM=xgRQ0fN=yg. Definition 12 (d-hedged bisimulation/bisimilarity). A d-hedged bisimulation is a d-hedged simulation R such that R 1 = f(h 1; Q; P ) j h ` P RQg is also a d-hedged simulation (where h 1 = f(N; M )j(M; N ) 2 hg). The d-hedged bisimilarity, written d, is the greatest d-hedged bisimulation, i.e. the union of all d-hedged bisimulations.
Since a d-hedged bisimulation is a hedged bisimulation up to a certain bound on the size of messages and fresh names, its definition leads to the following result. Lemma 2. (1) Any hedged bisimulation is a d-hedged bisimulation for all d 0. (2) When d > 0, a d-hedged bisimulation is also a (d 1)-hedged bisimulation.
We now aim to show that for any processes P; Q, there exists d 0 such that 9h 2 H h ` P d Q ) 9h 2 H h ` P Q. This statement is not valid for arbitrary infinite processes since these can analyse messages of arbitrary depth. Therefore, we now consider only the fragment of spi-calculus without replication.
Notice that let and guard operators are the only constructs that can check the structure of messages. For instance, c(y)(let x = 1(Db(y)) in [x = t]:P ) first decompose the message received on the channel c by applying Db(y) and 1, and then test the result against a term t. Therefore, messages with constructor depth greater than jtj + 2 (where 2 refers to the number of destructors in the let expression) will automatically fail the test. For let expressions, this observation leads to the following definition of analysis depth.
Definition 13 (Analysis depth). Let P be a finite (canonical) process. The analysis depth of P , denoted by ad(P ), is defined inductively by the clauses ad(0) = 0 ad(( m)P ) = ad(P ) ad(M hti:P ) = ad(P ) ad(M (x):P ) = ad(P ) ad(P jQ) = ad(P ) + ad(Q) ad( :P ) = ad(P ) ad(P + Q) = max(ad(P ); ad(Q)) ad(let x = t in P ) = ad(P ) + mdd(t) where the maximal destructor depth mdd of a term is defined as follows: mdd(ft1gt2 ) = max(mdd(t1); mdd(t2)) mdd((t1; t2)) = max(mdd(t1); mdd(t2)) mdd( i(t)) = mdd(t) + 1
mdd(Dt2 (t1)) = max(mdd(t1); mdd(t2)) + 1: Analysis depth, together with the maximal constructor depth previously defined, are used to derive the upper-bound on the size of messages that are needed to test in order to correctly decide if two processes are hedged bisimilar. We extend the notion of maximal constructor depth to hedges and processes, where the latter is well-defined as our processes are finite. For any hedge h and process P , mcd(h) = minfk j for all (M; N ) 2 h : h `k M $ N g mcd(P ) = maxfmcd( ) j P ( [ =))Q and occurs in Qg Definition 14 (Critical depth). Let P and Q be two finite processes and let h be a hedge. The critical depth CD(h; P; Q) is defined by
CD(h; P; Q) , mcd(h) + max(ad(P ) + mcd(P ); ad(Q) + mcd(Q)) As we will formally see below, when checking if a d-hedged simulation exists, given a hedge h we can correlate two input P a! (x)P 0 and Q !b (x)Q0, simply by testing the equivalence between P 0 and Q0 w.r.t. messages with maximal constructor depth less or equal than CD(h; P; Q). Moreover, Lemma 1 limits the number of fresh names we must consider to 2CD(h;P;Q). Messages that exceed these bounds can indeed be pruned without affecting the behaviour of processes. Definition 15 (d-pruning). Let M; N 2 M and h be a consistent hedge such that h ` M $ N . For d 0, the d-pruning of M , N w.r.t. h, denoted by prd(h; M; N ), is defined as (h; M; N ) if (M; N ) 2 h, and otherwise as: pr0(h; M; N ) = (h [ idfag; a; a) where a 2 N is fresh prd+1(h; fU gJ ; fV gK ) = (h0; fM 0gJ ; fN 0gK ) prd+1(h; (L1; R1); (L2; R2)) = (h00; (L01; R10); (L02; R20)) where (J; K) 2 h and prd(h; U; V ) = (h0; M 0; N 0) where prd(h; L1; L2) = (h0; L01; L02) and prd(h0; R1; R2) = (h00; R10; R20): Intuitively, the d-pruning of a message pair (M; N ) generates a message pair (M 0; N 0) where subterms appearing at levels greater than d are replaced by fresh names w.r.t. h, M and N . Then, the d-pruning is unique up to fresh names. Critical depth and d-pruning are readily extended to single processes and messages as CD(h; P ) , CD(h; P; P ) and prd(h; M ) , prd(h; M; M ). As stated in the next two lemmata, pruning terms that exceeds CD(h; P ) do not modify the behaviour of the process P . Lemma 3. Let (x)P be an abstraction of a finite process, h be a hedge and d CD(h; P ). For every message M the pruning N = 2(prd(h; M )) does not affect the reduction relation. That is, – ( :P )fM=xg > P fM=xg if and only if ( :P )fN=xg > P fN=xg; – (let y = t in P )fM=xg > P fM=xgf[[tfM=yg]]g if and only if
(let y = t in P )fN=xg > P fN=xgf[[tfN=yg]]g Lemma 4. Let (x)P be an abstraction of a finite process, h be a hedge and d CD(h; P ). For every message M the pruning N = 2(prd(h; M )) is so that – P fM=xg n! (y)P 0fM=xg if and only if P fN=xg n! (y)P 0fN=xg; – QfM=xg n! (( m)htiQ0)fM=xg iff QfN=xg n! (( m)htiQ0)fN=xg. This lemma also implies that -transitions are preserved, because -transitions are introduced only by the interaction rule (Figure 3); as shown in the diagram below, the conclusions of this rule are preserved because the premises are.
P fM=xg n! ((y)P 0)fM=xg QfM=xg n! (( m)htiQ0)fM=xg (P jQ)fM=xg ! (( m)(P 0ft=ygjQ0))fM=xg
P fN=xg n! ((y)P 0)fN=xg QfN=xg n! (( m)htiQ0)fN=xg
(P jQ)fN=xg ! (( m)(P 0ft=ygjQ0))fN=xg We can then reduce hedged bisimulation to d-hedged bisimulation. Theorem 1. Let P and Q be two finite processes, and h 2 H a consistent hedge. There is an integer d such that h ` P d Q, if and only if h ` P Q.
h0 ` P 0fM 0=xg Proof. (() A hedged bisimulation is a d-bisimulation for all d. ()) By Lemmata 3, 4 and the fact that the following is a hedged bisimulation: <>8(h; P; Q) PP; =Q Pfi n0fitMe =axngd; Q9h=02QH0fN9P=y0;gQ;(0h20; MP 09;MN ;0)N=2prMd(hs;.tM.; N );=>9 >: >; d Q0fN 0=yg; for d = CD(h; P; Q) tu As every quantification is bounded, d-hedged bisimilarity is decidable on finite processes. Then, so is hedged bisimilarity.
Corollary 1. Let P and Q be two finite processes and h 2 H a consistent hedge. It is decidable whether h ` P Q.
An algorithm to decide hedged bisimilarity is shown in Figure 4. For P; Q two finite (canonical) processes and h a hedge (which represents the initial knowledge of the attacker, e.g. public channels, known keys, nonces, etc.), HB(h; P; Q) = true if and only if there is a d such that (h; P; Q) are d-hedged bisimilar. Hence, by Theorem 1 we have h ` P Q if and only if HB(h; P; Q) = true. 2 H(h; P; Q) = 3 for each P
! P 0 s e l e c t Q =) Q0 such that HB(h; P 0; Q0) 4 for each P a! ( m)htiP 0 s e l e c t Q =)b ( n)ht0iQ0 such that
(a; b) 2 I(h) , h0 := I(h [ f([ t] ; [ t0] )g) consistent and HB(h0; P 0; Q0) 5 7 8 9 6 for each P a! (x)P 0 l e t d = CD(h; P; Q) and s e l e c t (Q =)b (x)Q0 and B N ) such that (a; b) 2 I(h) , jBj = 2d , B \ (fn(P ) [ fn(Q) [ n(h) [ fa; bg) = ; , h0 := h [ idB consistent and for each (M; N) s . t . (9k
d : h0 `k M $ N) : HB(h0; P 0fM=xg; Q0fN=xg)
In this paper we have proved that hedged bisimilarity (and hence barbed equivalence) is decidable on finite processes of the spi-calculus. As we generalised the spi-calculus to abstract from the syntactical equality between terms, our algorithm can be readily applied to different encryption/decryption schemata just by changing the congruence rules, as long as some mild conditions are satisfied.
Thanks to this extension, we believe that the approach followed in this paper
can be applied to decide hedged bisimilarity between processes of more
expressive calculi, in particular the applied -calculus (which is used in tools such as
ProVerif [