=Paper=
{{Paper
|id=Vol-2243/paper22
|storemode=property
|title=Deciding Hedged Bisimilarity
|pdfUrl=https://ceur-ws.org/Vol-2243/paper22.pdf
|volume=Vol-2243
|authors=Alessio Mansutti,Marino Miculan
|dblpUrl=https://dblp.org/rec/conf/ictcs/MansuttiM18
}}
==Deciding Hedged Bisimilarity==
https://ceur-ws.org/Vol-2243/paper22.pdf
Deciding Hedged Bisimilarity
Alessio Mansutti1,2? and Marino Miculan1??
1
DMIF, University of Udine, Italy
2
LSV, CNRS, ENS Paris-Saclay, Université Paris-Saclay, France
Abstract. 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.
1 Introduction
The spi-calculus is a formal model for the description and analysis of crypto-
graphic protocols [1]. In this model, the verification of security properties can be
reduced to the verification of suitable behavioural equivalences between spi pro-
cesses; for instance, if P (M ) represents a system of processes exchanging message
M , the system guarantees strong confidentiality of the message if an attacker
cannot observe any effective difference between P (M ) and P (M 0 ), for any M, M 0 .
To this end, several behavioural equivalences for the spi-calculus have been
proposed; we refer to [3] for a detailed comparison. In particular, in loc. cit.
Borgström and Nestmann defined hedged bisimilarity; this bisimilarity is shown
to be equivalent to barbed equivalence [7] and hence it is well suited to capture
the interaction of an attacker with the system and model his knowledge.
In this paper we prove that hedged bisimilarity (and hence barbed equiva-
lence) is decidable on finite processes (i.e. processes without replication). Our
result extends a similar one by Hüttel for framed bisimilarity, an equivalence
strictly finer than hedged bisimilarity [5]. Moreover, our algorithm can be read-
ily applied to different encryption/decryption schemata just by changing the
congruence over terms, as long as some mild conditions are satisfied; these con-
ditions are introduced in Section 2, where we recall also the syntax and semantics
of spi-calculus. Another difference with respect to previous work is that in our
formulation terms are typed and processes can inspect these types by means
of type-checking predicates; this corresponds to the fact that observers (even
attackers) can deduce the structure of a message, even if encrypted, from its
size or from the encoding algorithm. Moreover, we adopt a late operational se-
mantics, which allows for a simpler definition of hedged bisimilarity, as we will
see in Section 3. In Section 4 we show that hedged bisimilarity is decidable on
?
Project completed at University of Udine before being contracted by CNRS.
??
Partially supported by UniUd PRID 2017 ENCASE.
finite spi-calculus processes; to this end, we will introduce the notion of canoni-
cal 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
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 | x t ::= A | (t1 , t2 ) | π1 (t) | π2 (t) | {t1 }t2 | Dt2 (t1 )
φ ::= true | ¬φ | φ1 ∧ φ2 | [t1 = t2 ] | isname(t) | ispair(t) | isenc(t)
Intuitively, {t1 }t2 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 [1], reflect the
fact that often a process (e.g., an attacker) can easily infer if a term is a name,
a pair or an encrypted value, by observing its structure or by knowing how data
are encoded (in accordance to Kerckhoffs’s principle).
Moreover, we extend further the calculus by abstracting from the syntactical
equality normally used for [t1 = t2 ], see [1,3,5]. To do so we introduce a typing
system for ground terms. Types are defined by the grammar:
τ ::= N | B | τ1 × τ2 | C(τ )
where N, B are the base types of names and boolean values respectively, τ1 ×τ2 is
the pair type and C(τ ) is the type of encrypted terms of type τ . Figure 1 shows
the rules for the typing judgment t : τ over ground terms. For well-typed terms
t, we denote with keys(t) the set of names that are used as keys. Formally,
keys(t) = {key(t2 ) | there is t1 s.t. Dt2 (t1 ) or {t1 }t2 are a subterm of t}
where key(a) = a, key(πi (t1 , t2 )) = key(ti ) and key(Dt3 ({t1 }t2 )) = key(t1 ).
Ground terms are taken up-to some computable structural congruence ∼ =.
We can think of two terms in the same equivalence class of ∼ = as being computa-
tionally 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
2
a∈N φ:B φ1 : B φ2 : B
a:N true : B ¬φ : B φ1 ∧ φ2 : B [t1 = t2 ] : B
t1 : τ1 t2 : τ2 t : τ1 × τ2 t1 : τ t 2 : N t1 : C(τ ) t2 : N
i = 1, 2
(t1 , t2 ) : τ1 × τ2 πi (t) : τi {t1 }t2 : C(τ ) Dt2 (t1 ) : τ
isname(t) : B ispair(t) : B isenc(t) : B
Fig. 1. Typing judgment of terms.
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 ) ∧ ∀a ∈ keys(t)∀b ∈ N \ (n((t, t0 ))) : t{b/a} ∼ = t0 {b/a}
where t{b/a} is the substitution replacing all occurrences of a in t with b.
3. Deterministic decryption erasing all encryptions and decryption and ap-
plying the same projections leads to the same term, i.e. after applying the
rewriting rules πi ((t1 , t2 )) → ti , Dt2 (t1 ) → t1 and {t1 }t2 → t1 in all subterms
of t and t0 we obtain two syntactically equivalent terms.
It is easy to check that the equivalence used in [1,3,5] respects all these conditions.
Other encryption algorithms (and other abstract data types) can be considered
by adapting the congruence relation, as long as it respects the properties above.
For example commutative ciphers (like Elgamal encryption) can be considered
by adding the axiom ∀M ∈ G ∀a, b ∈ N : {{M }a }b ∼ = {{M }b }a .
Definition 1 (Processes). The spi-calculus processes are defined as follows:
P ::= 0 | A(x).P | Ahti.P | P1 |P2 | P1 + P2 | (νm)P |!P | φ.P | let x = t in P
where t and φ are respectively a term and a boolean formula, x is a variable, m
is a list of names and A can be both a name or a variable.
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
[8], with these differences:
– input/output operations exchange terms, not only names;
– φ.P is the guard operator, that behaves as P if the boolean formula φ holds;
– let x = t in P is the let operator that computes the value of t, binds the
variable x to it and then executes P .
Processes of the spi-calculus are taken up-to the usual structural congruence
familiar from the π-calculus theory and shown in Figure 2.
3
(νm)0 ≡ 0 P |0 ≡ P !P ≡ P |!P P |Q ≡ Q|P (P |Q)|R ≡ P (Q|R)
P +Q ≡ Q+P (P +Q)+R ≡ P +(Q+R) (νm)(P |Q) ≡ (νm)P |Q if m 6∈ fn(Q)
P and Q are α-equivalent P ≡Q
(νm)(νn)P ≡ (νn)(νm)P
P ≡Q P |R ≡ Q|R
P ≡Q P ≡Q P ≡Q P ≡Q Q≡R
P +R≡Q+R (νm)P ≡ (νm)Q Q≡P P ≡R
Fig. 2. Structural congruence of processes
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) = {true, false}, whereas for pairs and encryp-
tions it is defined as:
I(C(τ )) = {{M }a | M ∈ I(C(τ )), a ∈ N }/∼ =
I(τ1 × τ2 ) = {(M1 , M2 ) | M1 ∈ I(τ1 ), M2 ∈ I(τ2 )}/∼
=
Definition 2 (Evaluation). The evaluation for well-typed ground terms and
boolean expressions is a partial function [[·]] defined recursively as follows:
[[a]] = a ∈ N [[(t1 , t2 )]] = ([[t1 ]], [[t2 ]])
[[true]] = true [[π1 (t)]] = v1 if [[t]] = (v1 , v2 )
[[φ1 ∧ φ2 ]] = [[φ1 ]] ∧ [[φ2 ]] [[π2 (t)]] = v2 if [[t]] = (v1 , v2 )
[[¬φ]] = ¬[[φ]] [[{t1 }t2 ]] = {[[t1 ]]}[[t2 ]]
[[Dt2 (t1 )]] = t ∈ τ if [[t2 ]] = a ∈ N and [[t1 ]] ∼ = {t}a ∈ I(C(τ ))
[[[t1 = t2 ]]] = true if [[t1 ]] ∼ [[t
= 2 ]]; false otherwise
[[isname(t1 )]] = true if [[t1 ]] ∈ N ; false otherwise
[[ispair(t1 )]] = true if [[t1 ]] ∈ I(τ1 × τ2 ) for some τ1 and τ2 ; false otherwise
[[isenc(t1 )]] = true if [[t1 ]] ∈ I(C(τ )) for some τ ; false otherwise
Following [1,5] we define a late input operational semantics for spi-calculus
processes. We first define the reduction relation, which describes how processes
unfold and execute internal computations.
φ well-typed [[φ]] = true ∼v
t well-typed [[t]] = P > P0
φ.P > P let x = t in P > P {v/x} P ≡ P0
Then, the late operational semantics of the spi-calculus is represented by a la-
α
belled transition relation P −→ Q, where α ∈ {a, a | a ∈ N } ∪ {τ } 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.
4
a∈N t well-typed [[t]] ∼
=M a∈N
(input) a (output) a
a(x)P −→ (x)P ahtiP −→ (ν)hM iP
n n
P −→ (x)P 0 Q −→ (νm)hM iQ0
(interaction) τ {m} ∩ fn(P 0 ) = ∅
P |Q −→ (νm)(P 0 {M/x}|Q0 )
α α
P −→ D α 6∈ m ∪ m P −→ P 0
(restriction) α (parallel) α
(νm)P −→ (νm)D P |Q −→ P 0 |Q
α α
P −→ P 0 P ≡Q Q −→ Q0 Q0 ≡ P 0
(sum) α 0
(equivalence) α 0
P + Q −→ P P −→ P
Fig. 3. Late operational semantics of the spi-calculus.
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 {M/x}. 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:
(νm)(x)P , (x)(νm)P
(
(νa, m)hM iP if n ∈ fn(M )
(νa)(νm)hM iP ,
(νm)hM i(νa)P otherwise
R|(x)P , (x)(R|P ) where x 6∈ fv(R)
R|(νm)hM iP , (νm)hM i(R|P ) where {m} ∩ fn(R) = ∅
As usual, we denote with P =⇒ Q the transitive closure of the τ -transition
α α
whereas P =⇒ Q denotes P =⇒−→ Q.
3 Hedged bisimilarity
We now define the hedged bisimilarity, firstly introduced in [3]. A hedge is a finite
subset of M × M (where M is the set of all messages); we denote by H the
set of all hedges. A hedge h expresses a relation between messages used by two
processes P and Q, so that if (M, N ) ∈ h then M has the same effects on P
that N has on Q. For this reason not all hedges are well-formed (e.g. a hedge
that associates a name with a pair) and a notion of consistency is needed to
understand which hedges are really relevant for the bisimulation.
Definition 3 (Consistent Hedge). A hedge h is consistent if and only if it is
pair-free (i.e. all messages in h are not pairs) and for (M, N ) ∈ h we have that:
5
– M ∈ N ⇐⇒ N ∈ N ;
– for all (M 0 , N 0 ) ∈ h, if M ∼= M 0 or N ∼
= N 0 then M = M 0 and N = N 0 ;
∼ 0 ∼ 0
– if M = {M }k e N = {N }j then k 6∈ π1 (h) and j 6∈ π2 (h).
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 ) ∈ S(h), (k, j) ∈ S(h) and k, j ∈ N then ({M }k , {N }j ) ∈ S(h);
– if (M1 , N1 ) ∈ S(h) and (M2 , N2 ) ∈ S(h) then ((M1 , M2 ), (N1 , N2 )) ∈ S(h).
We write h ` M ↔ N for (M, N ) ∈ 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 ({M }k , {N }j ) ∈ A(h) and (k, j) ∈ A(h) then (M, N ) ∈ A(h);
– if ((M1 , N1 ), (M2 , N2 )) ∈ A(h) then (M1 , M2 ) ∈ A(h) and (N1 , N2 ) ∈ A(h).
Moreover, we define the irreducible I(h) of a hedge h as
I(h) , A(h) \ ({(C, D) ∈ A(h) | C ∼
= {M }k , D ∼
= {N }j , (k, j) ∈ A(h)}
∪ {((M1 , N1 ), (M2 , N2 )) ∈ A(h)})
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) ∈ R. Moreover, we say that R is
consistent if, for all h ∈ 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 0 RQ0 ;
a
– if P −→ (νm)hM iP 0 and m ∩ (fn(P ) ∪ n(π1 (h))) = ∅ then there exist b ∈ N
and a concretion (νn)hN iQ0 such that h ` a ↔ b, n∩(fn(Q)∪n(π2 (h))) = ∅,
b
Q =⇒ (νn)hN iQ0 and I(h ∪ {(M, N )}) ` P 0 RQ0 ;
6
a
– if P −→ (x)P 0 then there exist b ∈ N and an abstraction (y)Q0 such that
b
h ` a ↔ b, Q =⇒ (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 0 {M/x}RQ0 {N/y}.
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 [3].
Definition 7 (Hedged bisimulation/bisimilarity). A hedged simulation R
is a hedged bisimulation if R−1 = {(h−1 , Q, P ) | h ` P RQ} is also a hedged sim-
ulation (where h−1 = {(N, M )|(M, N ) ∈ h}). The hedged bisimilarity, written
∼, is the greatest hedged bisimulation, i.e. the union of all hedged bisimulations.
4 Decidability of hedged bisimulation for finite processes
Clearly, bisimilarity is undecidable for general processes (see [5]). Hence, we focus
on finite ones, i.e. without the “!” operator. Even on finite processes decidability
of hedged bisimilarity is not obvious, since the third condition in Definition 6
requires to check the equivalence of two abstractions for an infinite number of
messages w.r.t. any finite set of fresh names. In this section we show that this
problem can be avoided as there is only a finite number of names and messages
that need to be considered in deciding if two processes are hedged bisimilar.
The idea behind our result, and similar to that in [5] for framed bisimilarity,
is the following: if (x)P is finite, then it can inspect a message (using let and
guard operators) up to a certain depth k. If a message M with more than k
nested constructors is received by (x)P , then it can only be partially analysed
by P . Hence, all messages M 0 equivalent to M up to depth k will not cause
any difference in the execution of (x)P , apart from output messages. Indeed,
P {M/x} and P {M 0 /x} can output different messages (i.e. different parts of
M and M 0 respectively), but the two outputs are derived from M and M 0 by
applying the same operations, and only messages obtained through decryption
are interesting, since they can update the hedge h yielding a richer theory.
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.
7
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((t1 , t2 )) = max(mcd(t1 ), mcd(t2 )) + 1
mcd(x) = 0 mcd({t1 }t2 ) = mcd(t1 ) + 1
and then extended to boolean formulas as follows:
mcd(true) = 0 mcd(φ1 ∧ φ2 ) = max(mcd(φ1 ), mcd(φ2 ))
mcd(¬φ) = mcd(φ) mcd([x = M ]) = mcd(M )
mcd([x = y]) = 0 mcd(isname(x)) = 1
mcd(ispair(x)) = 1 mcd(ispair(x)) = 1
Definition 10 (k-homologous). Given h ∈ H and M, N ∈ M, we define
4
h `k M ↔ N ⇐⇒ 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 ∈ H and M, N ∈ 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 B 0 ⊂ N such that |B 0 | ≤ 2k
and satisfying the same three properties.
Proof. Suppose |B| ≥ 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 repre-
sented as binary trees with height k and with therefore at most 2k leafs. Hence
B can be reduced to a set B 0 such that |B 0 | ≤ 2k and h ∪ idB 0 `k M ↔ N . As
B 0 ⊆ B, it also holds that h ∪ idB 0 is consistent and B 0 ∩ n(h) = ∅. t
u
8
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 0 RQ0 ;
a
– if P −→ (νm)hM iP 0 and m ∩ (fn(P ) ∪ n(π1 (h))) = ∅ then there exist b ∈ N
and a concretion (νn)hN iQ0 such that h ` a ↔ b, n∩(fn(Q)∪n(π2 (h))) = ∅,
b
Q =⇒ (νn)hN iQ0 and I(h ∪ {(M, N )}) ` P 0 RQ0 ;
a
– if P −→ (x)P 0 then there exist b ∈ N and an abstraction (y)Q0 such that
b
h ` a ↔ b, Q =⇒ (y)Q0 and for all B ⊂ N , where |B| ≤ 2d , B ∩ (fn(P ) ∪
fn(Q) ∪ n(h)) = ∅ and h ∪ idB is consistent, for all pairs (M, N ) of ground
terms, if ∃k ≤ d h ∪ idB `k M ↔ N then h ∪ idB ` P 0 {M/x}RQ0 {N/y}.
Definition 12 (d-hedged bisimulation/bisimilarity). A d-hedged bisimu-
lation is a d-hedged simulation R such that R−1 = {(h−1 , Q, P ) | h ` P RQ} is
also a d-hedged simulation (where h−1 = {(N, M )|(M, N ) ∈ h}). 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 ∃h ∈ H h ` P ∼d Q ⇒ ∃h ∈ 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 |t| + 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(P |Q) = ad(P ) + ad(Q)
ad((νm)P ) = ad(P ) ad(φ.P ) = ad(P )
ad(M hti.P ) = ad(P ) ad(P + Q) = max(ad(P ), ad(Q))
ad(M (x).P ) = ad(P ) ad(let x = t in P ) = ad(P ) + mdd(t)
9
where the maximal destructor depth mdd of a term is defined as follows:
mdd(n) = 0 mdd({t1 }t2 ) = max(mdd(t1 ), mdd(t2 ))
mdd(x) = 0 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) = min{k | for all (M, N ) ∈ h : h `k M ↔ N }
mcd(P ) = max{mcd(φ) | P (≡ ∪ =⇒)Q and φ occurs in Q}
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,
a b
given a hedge h we can correlate two input P −→ (x)P 0 and Q −→ (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 ∈ 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 ) ∈ h, and otherwise as:
pr0 (h, M, N ) = (h ∪ id{a} , a, a) where a ∈ N is fresh
prd+1 (h, {U }J , {V }K ) = (h0 , {M 0 }J , {N 0 }K )
where (J, K) ∈ h and prd (h, U, V ) = (h0 , M 0 , N 0 )
prd+1 (h, (L1 , R1 ), (L2 , R2 )) = (h00 , (L01 , R10 ), (L02 , R20 ))
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 .
10
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 ){M/x} > P {M/x} if and only if (φ.P ){N/x} > P {N/x};
– (let y = t in P ){M/x} > P {M/x}{[[t{M/y}]]} if and only if
(let y = t in P ){N/x} > P {N/x}{[[t{N/y}]]}
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
n n
– P {M/x} −→ (y)P 0 {M/x} if and only if P {N/x} −→ (y)P 0 {N/x};
n n
– Q{M/x} −→ ((νm)htiQ0 ){M/x} iff Q{N/x} −→ ((νm)htiQ0 ){N/x}.
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.
n n
P {M/x} −→ ((y)P 0 ){M/x} Q{M/x} −→ ((νm)htiQ0 ){M/x}
τ
(P |Q){M/x} −→ ((νm)(P 0 {t/y}|Q0 )){M/x}
Lemma 4 Lemma 4
n n
P {N/x} −→ ((y)P 0 ){N/x} Q{N/x} −→ ((νm)htiQ0 ){N/x}
τ
(P |Q){N/x} −→ ((νm)(P 0 {t/y}|Q0 )){N/x}
We can then reduce hedged bisimulation to d-hedged bisimulation.
Theorem 1. Let P and Q be two finite processes, and h ∈ H a consistent hedge.
There is an integer d such that h ` P ∼d Q, if and only if h ` P ∼ Q.
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:
P, Q finite and ∃h0 ∈ H ∃P 0 , Q0 ∈ P ∃M, N ∈ M s.t.
0 0 0 0 0
(h, P, Q) P = P {M/x}, Q = Q {N/y}, (h , M , N ) = prd (h, M, N ),
h0 ` P 0 {M 0 /x} ∼d Q0 {N 0 /y}, for d = CD(h, P, Q)
t
u
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 ∈ 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.
11
1 HB(h, P, Q) = H(h, P 0 , Q0 ) ∧ H(h−1 , Q0 , P 0 )
2 H(h, P, Q) =
τ
3 f o r each P −→ P 0 s e l e c t Q =⇒ Q0 such that HB(h, P 0 , Q0 )
a b
4 f o r each P −→ (νm)htiP 0 s e l e c t Q =⇒ (νn)ht0 iQ0 such that
5 (a, b) ∈ I(h) , h0 := I(h ∪ {([[t]], [[t0 ]])}) consistent and HB(h0 , P 0 , Q0 )
a
6 f o r each P −→ (x)P 0
b
7 l e t d = CD(h, P, Q) and s e l e c t ( Q =⇒ (x)Q0 and B ⊂ N ) such that
8 (a, b) ∈ I(h) , |B| = 2d , B ∩ (fn(P ) ∪ fn(Q) ∪ n(h) ∪ {a, b}) = ∅ , h0 := h ∪ idB consistent
9 and f o r each (M, N ) s . t . (∃k ≤ d : h0 `k M ↔ N ) : HB(h0 , P 0 {M/x}, Q0 {N/x})
Fig. 4. Algorithm to decide hedged bisimilarity. The select statement implements a
non-deterministic exploration of the (finite) possible choices of its argument, until the
condition is satisfied; it returns true if successful, false otherwise.
5 Conclusions and further work
In this paper we have proved that hedged bisimilarity (and hence barbed equiv-
alence) is decidable on finite processes of the spi-calculus. As we generalised the
spi-calculus to abstract from the syntactical equality between terms, our algo-
rithm 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 expres-
sive calculi, in particular the applied π-calculus (which is used in tools such as
ProVerif [2]) and calculi with quantitative aspects [6,4]. Also considering larger
fragments of the spi-calculus beyond finite processes, e.g. depth- and restriction-
bounded processes, seems particularly promising.
References
1. M. Abadi and A. D. Gordon. A calculus for cryptographic protocols: The spi cal-
culus. Inf. Comput., 148(1):1–70, 1999.
2. B. Blanchet, M. Abadi, and C. Fournet. Automated verification of selected equiva-
lences for security protocols. In Proc. 20th LICS, pages 331–340. IEEE, 2005.
3. J. Borgström and U. Nestmann. On bisimulations for the spi calculus. Mathematical
Structures in Computer Science, 15(3):487–552, 2005.
4. T. Brengos, M. Miculan, and M. Peressotti. Behavioural equivalences for coalgebras
with unobservable moves. J. Logica. Algebraic Methods Program., 84:826–852, 2015.
5. H. Hüttel. Deciding framed bisimilarity. In Proceedings of Infinity’02, volume 68 of
Electronic Notes in Theoretical Computer Science, pages 1–18, 2003.
6. M. Miculan and M. Peressotti. GSOS for non-deterministic processes with quanti-
tative aspects. In Proc. QAPL, volume 154 of ENTCS, pages 17–33, 2014.
7. R. Milner and D. Sangiorgi. Barbed bisimulation. In ICALP, volume 623 of Lecture
Notes in Computer Science, pages 685–695. Springer, 1992.
8. D. Sangiorgi, D. Walker. The π-calculus: a Theory of Mobile Processes. CUP, 2001.
12