BRICS RS-02-25 H. Hüttel: Deciding Framed Bisimilarity BRICS

Basic Research in Computer Science

Deciding Framed Bisimilarity

Hans Hüttel BRICS Report Series RS-02-25 ISSN 0909-0878 May 2002 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2002, Hans Hüttel.

BRICS, Department of Computer Science University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/02/25/

Deciding Framed Bisimilarity

Hans Hüttel^{∗}

BRICS, Department of Computer Science, Aalborg University Fredrik Bajers Vej 7E, 9220 Aalborg Øst, Denmark

May 2002

Abstract

The spi-calculus, proposed by Abadi and Gordon, is a process calculus based on the π-calculus and is intended for reasoning about the behaviour of cryptographic protocols. We consider the finite-control fragment of the spi-calculus, showing it to be Turing-powerful (a result which is joint work with Josva Kleist, Uwe Nestmann, and Björn Victor.) Next, we restrict our attention to finite (non-recursive) spicalculus. Here, we show that framed bisimilarity, an equivalence relation proposed by Abadi and Gordon, showing that it is decidable for this fragment.

1 Introduction

The spi-calculus, originally proposed by Abadi and Gordon [AG97a], is a process calculus based on the π-calculus [MPW92] and is intended for describing and reasoning about the behaviour of cryptographic protocols.

An important insight of the spi-calculus is that correctness properties can be expressed as statements of behavioural equivalence. For instance, a protocol P (M) transmitting the message x satisfies the secrecy property w.r.t. M if we cannot distinguish between two instances of P which transmit different messages. Expressed using behavioural equivalence, this reduces to stating that

∗hans@cs.auc.dk

∀M_{1}, M_{2}.P (M_{1}) ∼ P (M_{2})

Deciding correctness properties of cryptographic protocols now amounts to deciding the behavioural equivalence ∼.

Various notions of behavioural equivalence have been put forward. Abadi and Gordon [AG97a] choose may-testing equivalence (originally proposed by De Nicola and Hennessy [NH83]). While may-testing is ideal from a philosophical point of view – processes are equivalent iff they behave in the same way under all attacks/observations – this equivalence is defined via universal quantification over observer processes and is therefore less ideal from the perspective of actually determining the equivalence of processes.

Consequently, in [AG98b] Abadi and Gordon define a bisimulation-style equivalence, framed bisimilarity, and show it to be as a sound approximation of may-testing equivalence. A main motivation behind their work was to define a notion of behavioural equivalence which has a useful proof technique and is decidable.

The main focus of this paper is to examine to which extent the latter is the case.

As the full spi-calculus is Turing-powerful one can only hope for a positive decidability result within a proper subcalculus. A natural candidate would be the finite-control spi-calculus, the spi-calculus counterpart of regular CCS; finite-control processes have a bounded number of parallel components and, because of the presence of recursion, are able to describe multiple protocol runs.

However, even the finite-control spi-calculus is Turing-powerful [HKNV97]. In this paper we first demonstrate this by presenting an encoding of Minsky’s two-counter machines into the finite-control calculus, a result which is joint work with Josva Kleist, Uwe Nestmann, and Björn Victor.

Next, we restrict our attention to finite spi-calculus processes and show that framed bisimilarity is decidable in this fragment. The finite spi-calculus processes are the recursion-free processes of the spi-calculus, corresponding to single runs of a cryptographic protocol.

In [AL00] Amadio and Lugiez consider a finite spi-calculus similar to ours and show that its associated reachability problem is decidable (albeit NP-hard). As further work they mention finding an algorithm for deciding bisimilarity.

A main problem in obtaining our result stems from matching input transitions, since two processes must be equivalent under all value instantiations; we overcome this problem by showing that only finitely many values need be considered.

2 The spi-calculus

The spi-calculus extends the π-calculus [MPW92, Mil99] with primitives for encryption and decryption. As in the π-calculus, communication takes place over channels that can either be public or restricted. Messages may be decrypted; the perfect encryption hypothesis is adopted in the spi-calculus – an attacker cannot guess the key of an encrypted message.

2.1 Syntax

In this section we present the two fragments of the spi-calculus that we shall study in the rest of the paper. Our syntax largely follows that of [AG97a]. We only consider shared key cryptography since the definitions related to framed bisimilarity in [AG98b] only use shared key cryptography. However, an extension of the results in the present paper should be straightforward.

2.1.1 Terms

Common to our two fragments is the set of terms that can be communicated by processes. Unlike the π-calculus, the spi-calculus allows us to communicate composite terms. The set of terms, T , has its syntax defined by the following grammar.

L, M, N ::= x | n | {M}_{N} | (M, N)

In the above, x ranges over the set of variables, n ranges over the set of names, {M}_{N} denotes the term M encrypted using key N and (M, N) denotes the pair whose components are the terms M and N.

2.1.2 The finite-control spi-calculus

The finite-control spi-calculus is a straightforward extension of the finitecontrol π-calculus introduced by Lin [Lin91].

As the definition below shows, a finite-control process consists of a fixed number of sequential processes running in parallel.

Definition 1 The set of finite-control spi-calculus processes is given by the grammar

R ::= M(x).R | \overline{M}⟨N⟩.R | (νn)R
| D(M) | 0 | [M = N] R | R_{1} + R_{2}
| let (x, y) = M in R | recD(M).R
| case L of {x}_{N} in R
P ::= R | (νn)P | P |P

The spi-calculus distinguishes between variables x, y, z, … ∈ V and names c, m, n, k … N. Names refer to a key or a channel, whereas variables are instantiated to messages. When concerning channels, a name c is used for input and its co-name \overline{c} used for output.

The spi-calculus has two communication primitives. \overline{M}⟨N⟩.P is output; N is emitted on the channel M. M(x).P is input; the variable x is received on the channel M, and x is bound in P.

While encryption is handled at the level of message terms, decryption is a process construct. case L of {x}_{N} in P is used to decrypt terms; x is bound in P. The other term destructor is let (x, y) = M in P which allows us to split a pair; the variables x and y are bound in P.

The remaining process constructs are also found in the π-calculus: (νn)P is the restriction construct. The new name n is bound in P. P | Q denotes parallel composition and 0 is the empty process. Finally, the match construct [M = N] P can proceed as P iff M is equal to N.

In the finite-control calculus we allow two additional constructs, namely nondeterministic choice, R_{1}+R_{2} and recursively defined processes, recD(M).R. D(M) ranges over recursion constants which may be parameterised by a term.

We identify processes up to renaming of bound names and variables. A process without any free variables is closed; we let P denote the set of closed processes. Furthermore we let fn[[P]] denote the set of free names in P, and fv[[P]] the free variables in P. For any set of terms S, we let n(S) denote the set of names occurring in S, free as well as bound. P [M/x] denotes the substitution of the term M for all free occurrences of x in the process P and is defined as expected.

The original presentation of the spi-calculus in [AG97a] introduces natural numbers into the syntax. This, however, is unimportant as we can encode the naturals using encryption and decryption. Let a, b be fresh names. We then let

[[0]] = a
[[n + 1]] = [[{[[n]]}_{b}]]

The test-for-zero process construct now becomes

[[case v of 0 : P suc(x) : Q]] = case v of {x}_{b} in P + [v = a]Q

In our undecidability proof in section 3 we use natural numbers freely by implicit appeal to this encoding.

2.1.3 Finite processes

The syntax of processes in the finite spi-calculus omits nondeterministic choice and recursion from the finite-control fragment.

P, Q, R ::= (νn)P | \overline{M}⟨N⟩.P | M(x).P | P | Q
| [M = N] P | 0 | let (x, y) = M in P | case L of {x}_{N} in P

2.1.4 Agents

An agent can be a process, an abstraction or a concretion. The syntax of agents is defined by the following grammar:

A, B ::= P | C | F
F, G ::= (x)P
C, D ::= (νm⃗)⟨M⟩P

(x)P is an abstraction, which needs to bind a term to x before proceeding. (νm⃗)⟨M⟩P is a concretion, which is immediately able to output the term M. A will denote the set of closed agents.

2.2 Semantics

Our labelled commitment semantics of the spi-calculus is that of [AG98b].

2.2.1 Reduction and structural congruence

The reduction relation describes how processes unfold and make preparations for a reaction. In particular, the rules describe how the term deconstructors behave (Table 1) and, for finite-control processes, how nondeterministic choice is resolved and that a recursive process proceeds by unfolding the recursive definition (Table 2) . In the case of a decryption we only proceed if the key is a name. See Table 1.

[M = M] > P
let(x, y) = (M, N) in P > P [M/x][N/y]
case {M}_{n} of {x}_{n} in P > P [M/x]

Table 1: The reduction rules for term destructors

\begin{aligned}recD(x).P & > & P [recD(M_{i}).P /D(M_{i})] \\ P_{1} + P_{2} & > & P_{1} \\ P_{1} + P_{2} & > & P_{2} \end{aligned}

Table 2: The reduction rules for recursion and choice

Structural congruence, ≡, is defined in Table 3. It captures the identities that should intuitively hold.

2.2.2 The commitment relation

The commitment transition system (P, {⟶^{α}| α ∈ N ∪ {τ}}, A) has its transition relation defined inductively by the rules in Definition 4.

In Definition 4 we use the interaction operator • defined by

C • F ≜ (νn⃗)(Q | P [N/x]) F • C ≜ (νn⃗)(P [N/x] | Q),

when {n⃗} ∩ fn[[P]] = ∅. Here, we extend restriction and composition as follows:

(νn)(x)P ≜ (x)(νn)P
Q | (x)P ≜ (x)(Q | P)
(νn)(νm⃗)⟨M⟩P ≜ \begin{cases}(νn, m⃗)⟨M⟩P & if n ∈ fn[[M]] \\ (νm⃗)⟨M⟩(νn)P & otherwise \end{cases}
Q | (νm⃗)⟨M⟩P ≜ (νm⃗)⟨M⟩(Q | P)

P | 0 ≡ P  P | Q ≡ Q | P
P | (Q | R) ≡ (P | Q) | R  (νm)(νn)P ≡ (νn)(νm)P
(νn)0 ≡ 0  P | (νn)Q ≡ (νn)(P | Q) if n ∉ fn[[P]]
\frac{P > Q}{P ≡ Q}  \frac{P ≡ Q Q ≡ R}{P ≡ R}
\overline{P ≡ P}  \frac{P ≡ Q}{Q ≡ P}
\frac{P ≡ Q}{P | R ≡ Q | R}  \frac{P ≡ Q}{(νn)P ≡ (νn)Q}

Table 3: Rules defining structural congruence

where we assume x ∉ fv[[Q]], n ∉ {m⃗} and {m⃗} ∩ fn[[Q]] = ∅. The dual composition A | Q is defined symmetrically.

3 The finite-control fragment is Turing-powerful

As the finite-control spi-calculus calculus is the spi-calculus analogue of the finite-control fragment of the π-calculus, introduced by [Lin91], one might expect the situation to be same as in the π-calculus. Here, Dam [Dam97] has shown that late and early bisimilarity [MPW92] as well as open bisimilarity [San96] are all decidable. Dam’s result depends on the fact that it is always suffices to consider a finite set of names due to the bounded parallelism of a finite-control process.

However, the finite-control spi-calculus is in fact Turing-powerful, destroying all hope of obtaining positive decidability results for any non-trivial notion of behavioural equivalence. The encoding presented here is joint work with Josva Kleist, Uwe Nestmann, and Björn Victor.

3.1 Encoding two-counter machines in the finite-control fragment

For our proof of this fact, we consider another universal model of computation, namely the two-counter machines of [Min67]. A two-counter machine is a simple imperative program consisting of a sequence of labelled instructions that can modify the values of two nonnegative integer counters, c_{0} and c_{1}. Two instructions are singled out, namely Lstart and Lstop. The program

(Input) m(x).P ⟶^{m} (x)P  _{(Output)} \overline{m}⟨M⟩.P ⟶^{\overline{m}} (ν)⟨M⟩P

(Com-1)  \frac{P ⟶^{m} F Q ⟶^{\overline{m}} C}{P | Q ⟶^{τ} F • C}  (Com-2)  \frac{P ⟶^{\overline{m}} C Q ⟶^{m} F}{P | Q ⟶^{τ} C • F}

(Par-1)  \frac{P ⟶^{α} A}{P | Q ⟶^{α} A | Q}  (Par-2)  \frac{Q ⟶^{α} A}{P | Q ⟶^{α} P | A}

(Res) \frac{P ⟶^{α} A α ∉ \{m, \overline{m}\}}{(νm)P ⟶^{α} (νm)A}  (Red)  \frac{P > Q ⟶^{α} A}{P ⟶^{α} A}

Table 4: The commitment semantics of the spi-calculus

starts with the line Lstart and halts if Lstop is reached. The instruction set consists of two different types of instructions (in the indices of the counter variables we always assume addition and subtraction modulo 2):

1. L : c_{k} := c_{k} + 1; goto L_{n}

2. L : if c_{k} = 0 thengoto L_{n}^{1} else c_{k} := c_{k} − 1; goto L_{n}^{2}

We can always assume that a type 1 instruction has L ≠ L_{n} (if L = L_{n} the machine would loop forever) and that a type 2 instruction has L ≠ L_{n}^{1} (here, too, if L = L_{n}^{1} the machine would loop forever) and L ≠ L_{n}^{2} (we can simply duplicate the instruction in question.)

Theorem 2 Any two-counter machine can be simulated in the finite-control spi-calculus.

Proof: We define an encoding [[]] from two-counter machine instructions into the finite-control spi-calculus. The idea is simply that the two counters are represented by processes and the each instruction corresponds to a process that communicates with the counters.

We assume the following set of names, which we denote by n:

• For every instruction label L_{n} we introduce the name l_{n}, used to signal a goto, and the constant D_{l_{n}}.

• For counter c_{k} we introduce the names

d_{k} indicating that the counter is decremented

c_{k} indicating that the counter is incremented

r_{k} indicating that the value of the counter is being read

A counter c_{k} is represented as the process

C_{k} = recD_{k}(x).(\overline{r_{k}}⟨x⟩.D_{k}(x) + d_{k}.D_{k}(x − 1) + i_{k}.D_{k}(x + 1))

Instructions are encoded as

[[L : c_{k} := c_{k} + 1; goto L_{n}]] = recD_{l}.l.i_{k}. \overline{l_{n}} .D_{l}

[[L : if c_{k} = 0 then

          goto L_{n}^{1} else

c_{k} := c_{k} − 1; goto L_{n}^{2}]] = recD_{l}.l.r_{k}(y).([y = 0] \overline{l_{n}^{1}} .D_{n} + [y ≠ 0] \overline{d_{k}} . \overline{l_{n}^{2}} .D_{n})

Suppose that a two-counter machine M is composed of a sequence of instructions S_{1}, …, S_{m}. Then the encoding of the machine is given by

[[M]] = (νn) ∏_{i=1}^{m}[[S_{i}]] | C_{0} | C_{1}

It is now easy see that the two-counter machine can reach a state where c_{0} = v_{0} and c_{1} = v_{1} if and only if [[M]] ⟶^{τ}^{∗} P′ where the term P′ has counter constants whose values are D_{k}(v_{0}) and D_{k}(v_{1}), respectively. □

Corollary 3 Any nontrivial notion of behavioural equivalence is undecidable in the finite-control spi-calculus.

4 Framed bisimilarity

Framed bisimilarity was introduced by Abadi and Gordon in [AG98b].

4.1 Frames and theories

Processes are related with respect to a frame-theory pair which represents the knowledge of the environment.

Definition 4 A frame fr is a finite set of names. A theory th is a finite set of pairs of terms (M, N). We let e range over the set of frame-theory pairs.

(Ind Var)  \overline{e ⊢ x ↔ x}

(Ind Frame)  \frac{n ∈ fr}{e ⊢ n ↔ n}  (Ind Theory)  \frac{(M, N) ∈ th}{e ⊢ M ↔ N}

(Ind Pair) \frac{e ⊢ M ↔ M′ e ⊢ N ↔ N′}{e ⊢ (M, N) ↔ (M′, N′)} (Ind Enc) \frac{e ⊢ M ↔ M′ e ⊢ N ↔ N′}{e ⊢ \{M\}_{N} ↔ \{M′\}_{N′}}

Table 5: Rules defining the indistinguishability relation

Intuitively, when comparing processes P and Q, the elements of the frame are the names from P and Q that the attacker knows. If (M, N) ∈ th the attacker cannot distinguish the term M coming from P and the term N coming from Q.

In what follows, when given an environment e we refer to its frame part as fr_{e} and its environment part as th_{e}.

Definition 5 Let e = (fr, th) be an environment. Terms M and N are indistinguishable under e, written e ⊢ M ↔ N, if it can be derived by the rules in Table 5.

An environment must be consistent. This is captured by

Definition 6 Environment e is ok, written e ⊢ ok, if:

1. ∀(M, N) ∈ th it must hold that M is closed, ∃M_{1}, M_{2} : M = {M_{1}}_{M_{2}} and ∄N_{2} : e ⊢ M_{2} ↔ N_{2}. The converse must also hold for N.

2. whenever (M, N) ∈ th and (M′, N′) ∈ th, M = M′ iff N = N′.

Definition 7 Let e and e′ be environments. e′ extends e, written e ≤ e′, iff ∀M, N : e ⊢ M ↔ N ⇒ e′ ⊢ M ↔ N.

A framed process pair is a quadruple (fr, th, P, Q), where P, Q ∈ P. If R is a set of framed process pairs, we write e ⊢ P RQ when (fr, th, P, Q) ∈ R. A framed relation is a set R of framed process pairs, such that e ⊢ ok whenever e ⊢ P RQ.

4.2 Framed simulations and bisimulations

Framed simulation is a late simulation [MPW92]; the choice of a matching transition for an input transition does not depend on the value that will eventually be received.

Definition 8 A framed simulation is a framed relation S such that, whenever e ⊢ P SQ, the following three conditions hold

1. If P ⟶^{τ} P′ then there exists a process Q′ such that Q ⟶^{τ} Q′ and e ⊢ P′SQ′.

2. If P ⟶^{c} (x)P′ and c ∈ fr then there exists an abstraction (x)Q′ with Q ⟶^{c} (x)Q′ and, for all sets {n⃗} disjoint from fn[[P]] ∪ fn[[Q]] ∪f ∪fn(th) and all closed terms M and N, if (fr ∪{n⃗}, th) ⊢ M ↔ N then (f ∪ {n⃗}, th) ⊢ P′[M/x]SQ′[N/x].

3. If P ⟶^{\overline{c}} (νm⃗)⟨M⟩P′, c ∈ fr and \{m⃗\} ∩ (fn[[P]] ∪ fn(π_{1}(th)) ∪ fr) = ∅ then there exists a concretion (νn⃗)⟨N⟩Q′ with Q ⟶^{\overline{c}} (νn⃗)⟨N⟩Q′ and {n⃗} ∩ (fn[[Q]] ∪ fn(π_{2}(th)) ∪ f) = ∅. Furthermore ∃e′ : e ≤ e′, e′ ⊢ M ↔ N, and e′ ⊢ P′SQ′.

Definition 9 A framed bismulation is a framed simulation S such that S^{−1} = {e′ ⊢ QSP | e ⊢ P SQ ∧ e′ = (fr, {(M, N) | (N, M) ∈ th})} is also a framed simulation.

Definition 10 Framed bisimilarity is the greatest framed bisimulation, written ∼_{f}.

5 A decidability result

Definitions 8 and 9 do not provide us with a straightforward means of checking bisimilarity. The goal of the rest of our paper is to address this issue. More precisely, we shall show that in the case of finite processes

• we only need to consider finitely many terms when matching input transitions.

• we only need to consider finitely many possible frame extensions when matching input transitions

• we only need to consider finitely many frame-theory extensions when matching output transitions

Taken together, these observations will allow us to obtain a simple decision procedure for framed bisimilarity.

5.1 Matching input transitions

Assume that we are trying to determine whether (fr, th) ⊢ P ∼_{f} Q. We have an input commitment P ⟶^{c} (x)P′, have a candidate for a matching commitment, Q ⟶^{c} (x)Q′, and now need to determine whether P′ ∼_{f} Q′.

Assume that the maximal number of successive term destructors in P and Q is m, and that the maximal number of term constructors of any term in th is d. Then we need only consider the finitely many terms of depth ≤ m + d constructed from (fr, th) and a bounded number of new names in order to determine if (fr, th) ⊢ P′ ∼_{f} Q′. This must hold as the process can only inspect any input term up to m levels of encryption/pairing and because the environment may ask us to regards terms whose depth is up to d as indistinguishable.

5.1.1 The depth of terms and processes

The notion of the maximal constructor depth of a term is as expected. It counts the level of encryption and the level of pairing. The level of decryption takes precedence over the level of pairing and only the level of decryption within the contents of a ciphertext matters, as terms appearing in key position must be names. Otherwise, they will cause the process not to evolve any further.

Definition 11 The maximal constructor depth d(M) of a term M is defined inductively by the clauses

d(n) = 0
d(x) = 0
d({M}_{N}) = d(M) +1
d((M, N)) = max(d(M), d(N))

The above definition easily extends to frame-theory pairs.

Definition 12 Let (fr, th) be a frame-theory pair where fr = {(M_{1}, N_{1}), …, (M_{k}, N_{k})}. The maximal constructor depth of (fr, th) is defined b

d((fr, th)) = max{max(d(M_{i}), d(N_{i})) | 1 ≤ i ≤ k}

The maximal destructor depth of a process P is the maximal number of encryptions and pairing operators that can ever be removed along the process P. Decryption and pair splitting operations each contribute by 1, whereas a parallel composition P | Q may contribute with decryptions from both P and Q.

Definition 13 Let P be a finite process. The maximal destructor depth of P is denoted by mdd(P) and defined inductively by the clauses

mdd(0) = 0
mdd((νn)P) = mdd(P)
mdd(\overline{M}⟨N⟩.P) = mdd(P)
mdd(M(x).P) = mdd(P)
mdd(P | Q) = mdd(P) + mdd(Q)
mdd([M = N] P) = mdd(P)
mdd(let (x, y) = M in P) = mdd(P) +1
mdd(case L of {x}_{N} in P) = mdd(P) +1

5.1.2 d-framed bisimilarity

d-framed bisimilarity is a variant of framed bisimilarity that only requires input transitions to be matched for transmitted message terms up to a certain depth.

Definition 14 Let k be a nonnegative integer and let e be a frame-theory pair such that e ⊢ ok. We write e ⊢ M ↔^{k} N if e ⊢ M ↔ N and max(d(M), d(N)) = k. Whenever e ⊢ M ↔^{k} N we say that M and N are k-indistinguishable in e.

Since we only consider terms up to a certain depth, we need only consider finitely many extensions of the frame. This is expressed in the following lemma.

Lemma 15 Let (fr, th) be a frame-theory pair and assume that max(d(M), d(N)) = k. If there is a (fr ∪{n⃗}, th) such that (fr ∪{n⃗}, th) ⊢ M ↔^{k} N, then we may choose a {n⃗} where |n⃗| ≤ 2k satisfying (fr ∪{n⃗}, th) ⊢ M ↔^{k} N.

Proof: If M and N are not indistinguishable under (fr, th), this must be amended by applying the constructor rules, the rule (Ind Theory) and the rule (Ind Frame) to new names. Every application of a constructor rule can introduce at most two new names, so at most 2k new names can be introduced. □

Lemma 15 leads to the following definition of d-framed simulation.

Definition 16 For any nonnegative integer d, a d-framed simulation is a framed relation S such that, whenever (fr, th) ⊢ P SQ, the following three conditions hold

1. If P ⟶^{τ} P′ then there exists a process Q′ such that Q ⟶^{τ} Q′ and e ⊢ P′SQ′.

2. If P ⟶^{c} (x)P′ and c ∈ fr then there exists an abstraction (x)Q′ with Q ⟶^{c} (x)Q′ and, for all sets {n⃗} disjoint from fn[[P]] ∪ fn[[Q]] ∪ fr ∪ fn(th) such that |n⃗| ≤ 2d and all closed terms M and N, if (fr ∪{n⃗}, th) ⊢ M ↔^{i} N and 0 ≤ i ≤ d then (fr ∪{n⃗}, th) ⊢ P′[M/x]SQ′[N/x].

3. If P ⟶^{\overline{c}} A ≡ (νm⃗)⟨M⟩P′, c ∈ fr and \{m⃗\} ∩ (fn[[Q]] ∪ fn(π_{1}(th)) ∪ fr) = ∅ then there is a concretion B ≡ (νn⃗)⟨N⟩Q′ such that Q ⟶^{\overline{c}} B, the set {n⃗} is disjoint from fn[[Q]] ∪ fn(π_{2}(th)) ∪ fr and e′ ⊢ P′SQ′ for some e′ ≥ (fr, th) where e′ ⊢ M ↔ N.

Definition 17 A d-framed bisimulation is a d-framed simulation S such that S^{−1} = {e′ ⊢ QSP | e ⊢ P SQ ∧ e′ = (fr_{e}, {(M, N) | (N, M) ∈ th_{e}})} is also a d-framed simulation.

Definition 18 d-framed bisimilarity is the greatest d-framed bisimulation, written ∼_{f}^{d}.

Our goal is to show that for finite processes P and Q we have that P and Q are framed bisimilar iff they are d-bisimilar where d is the critical depth.

The critical depth of (e, P, Q) is the maximal depth of terms that must be considered as inputs when determining whether P and Q are framed bisimilar under e.

Definition 19 Let (e, P, Q) be a framed process pair. The critical depth of (e, P, Q) is defined by

cd(e, P, Q) = d(e) + max(mdd(P), mdd(Q))

We let

cd(e, P) = cd(e, P, P)

When considering the result of an input commitment, we only need to consider instantiations with terms whose depths do not exceed the critical depth. Intuitively, this suffices as all subterms occurring below the critical depth are inaccessible by the destructors of a process.

If two terms are indistinguishable, their subterms appearing at depth d can be replaced by fresh names for any d such that the resulting terms will still be indistinguishable. This is the idea behing d-pruning.

Example 20 Let M = {{a}_{b}}_{c} and N = {{d}_{e}}_{f} and assume that we have (M, N) ∈ th for some theory th. Let fr = {h}. Then we have (fr, th) ⊢ {M}_{h} ↔ {N}_{h}. We also have (fr ∪{g}, th) ⊢ {{g}_{g}}_{h} ↔ {{g}_{g}}_{h} where g is a fresh name not found in fr. ((fr ∪{g}, th), {g}_{h} ↔ {g}_{h}) is the 1-pruning of (e, M, N).

The pruning of a pair of terms (M, N) at depth d generates a pair of pruned terms (M′, N′). M′ and N′ are constructed by replacing subterms appearing at levels greater than d by encryptions of arbitary fresh names by the same fresh names. The fresh names are then added to the frame.

Definition 21 Let M and N be closed terms and let e ⊢ ok. Further assume that e ⊢ M ↔ N, that all subterms appearing in key position in M and N are names and that d is a nonnegative integer. The d-pruning of (e, M, N), denoted by pr_{d}((e, M, N)), is defined inductively by the clauses

pr_{0}(((fr, th), n, n))  = ((fr, th), n, n)
pr_{0}(((fr, th), M, N))  = ((fr, th), M, N)  if (M, N) ∈ th

pr_{0}(((fr, th), M, N))

= ((fr ∪{a}, th), {a}_{a}, {a}_{a})

if (M, N) ∉ th and a is fresh

pr_{d+1}((fr, th), {M_{1}}_{k}, {N_{1}}_{k}) = (e′, {M′}_{k}, {N′}_{k}) where (e′, M′, N′) = pr_{d}(((fr, th), M_{1}, N_{1}))

If M is an open term, we define pr_{d}((e, M)) = (e, M).

The pruning operator extends to single terms by defining pr_{d}((e)(M)) = pr_{d}((e)(M, M)).

Note that, because of the usage of unspecified fresh names, the pruning operator as defined here does not generate a unique pair of terms. This can be dealt with by means of introducing suitable bookkeeping.

Note also how the definition exploits the fact that only names are allowed in key position.

Lemma 22 If e ⊢ M ↔ N, d = max(d(M), d(N)) and pr_{d}((e, M, N)) = (e′, M′, N′) then e′ ⊢ M′ ↔^{d} N′.

Proof: A straightforward induction in d, appealing to Definition 21. □

We can extend the pruning operation to pairs of term vectors. This is done inductively; we prune the components of the vectors successively, extending the frame as we proceed.

Definition 23 Let |M⃗| = |N⃗| = k. Then pr_{d}((M⃗, N⃗)) is defined inductively by

pr_{d}((e, (M_{1}, …, M_{k}), (N_{1}, …, N_{k}))) = (e′, (M′_{1}, …, M′_{k}), (N′_{1}, …, N′_{k}))

where

(e′′, M′_{1}, N′_{1}) = pr_{d}((e, M_{1}, N_{1}))

and

(e′, (M′_{2}, …, M′_{k}), (N′_{2}, …, N′_{k})) = pr_{d}((e′′, (M_{2}, …, M_{k}), (N_{2}, …, N_{k})))

Lemma 24 Let P be a process such that P = A[M⃗/x⃗] and let d = cd(e, P). P > A iff P_{1} > A_{1} where P_{1} = A[N⃗/x⃗] where pr_{d}((e, M⃗)) = (e′, N⃗) and A_{1} = A[N⃗/x⃗].

Proof: Both implications are seen to hold by an inspection of the clauses in the definition of the reduction relation. The interesting case is the decryption clause:

case {M}_{k} of {y}_{k} in P′ > P′[M/y]

If P = case {M}_{k} of {y}_{k} in P′, then the definition of the pruning operator tells us that P_{1} = case {N}_{k} of {y}_{k} in P′_{1} where P′ = A′_{1}[M⃗/x⃗] and P′_{1} = A′[N⃗/x⃗] for some A′_{1}. We now see that

case {N}_{k} of {y}_{k} in P′_{1} > P′_{1}[N/y]
□

Lemma 25 Let P = A[M⃗/x⃗] and let d = cd(e, P). P ⟶^{α} A′ iff P_{1} ⟶^{α} A′_{1} where P_{1} = A[N⃗/x⃗] where pr_{d}((e, M⃗)) = (e′, N⃗) and A′_{1} = B[N⃗/x⃗] and A′ = B[M⃗/x⃗] for some B.

Proof: In the case of both implications, the proof proceeds by transition induction. The induction hypothesis in the case concerning the rule (Red) uses Lemma 24. The only other interesting cases are the prefix axioms. □

Theorem 26 Let P and Q be finite spi processes and let d = cd(e, P, Q) where e ⊢ ok. We have that e ⊢ P ∼_{f} Q iff e ⊢ P ∼_{f}^{d} Q.

Proof: By definition, any framed bisimulation is also a d-framed bisimulation. It therefore suffices to establish that e ⊢ P ∼_{f} Q whenever e ⊢ P ∼_{f}^{d} Q. We show that

R = \{(e, P, Q) | ∃e′, A, B, M⃗, N⃗. \begin{matrix}P = A[M⃗/x⃗], Q = B[N⃗/y⃗] \\ e′ ⊢ A[M⃗′/x⃗] ∼_{f}^{n} B[N⃗′/y⃗] \\ (e′, (M⃗′, N⃗′)) = pr_{d}((e, M⃗, N⃗)) \\ d = cd(e, P, Q) \end{matrix} \}

is a framed bisimulation. This follows from Lemma 25. □

5.2 Matching output transitions

Next, we have to deal with matching output transitions. Fortunately, there are only finitely many candidates for an environment extension in the case of the output clause.

Unfortunately, as was shown in [BN02], the characterization of framed bisimilarity presented in [EHHN99] is sound but not complete. We are therefore unable to fall back on the algorithm for computing environment extensions presented in [EHHN99]. Instead we use

Lemma 27 Let e ⊢ ok and let M, N ∈ T . It is decidable whether there is an e ≤ e′ such that e ⊢ M ↔ N.

Proof: To construct an e′ such that e′ ⊢ M ↔ N, we only need to add pairs of the form (M_{1}, N_{1}) where max(d(M_{1}), d(N_{1})) ≤ max(d(M), d(N)) and such that n[[M_{1}]] ∪ n[[N_{1}]] ⊆ n[[M]] ∪ n[[N]]. Only finitely many such candidate pairs exist. □

6 Deciding framed bisimilarity

We can now state the main results of our paper.

Theorem 28 Let e ⊢ ok and let P and Q be finite spi-calculus processes. For any d ≥ 0 it is decidable whether e ⊢ P ∼_{f}^{d} Q.

Proof: Table 6 presents a nondeterministic recursive algorithm B((e, (P, Q)) for determining if e ⊢ P ∼_{f}^{d} Q.

As the algorithm encodes the ‘bisimulation game’ of Definition 16, e ⊢ P ∼_{f}^{d} Q iff there exists a successful evaluation of B((e, (P, Q))). The algorithm always terminates, as Lemma 15 and Lemma 27 guarantee that the checks performed in the conditional statements of the algorithm are effective

B(((fr, th), (0, 0))) = tt B(((fr, th), (P_{1}, P_{2}))) =

let (fr, th) = e in

for each P_{i} ⟶^{a} (x)P′_{i} where a ∈ fr

select a P_{i+1} ⟶^{a} (y)P′_{i+1}

if no such P′_{i+1} exists

then fail else for each n⃗ where |n⃗| ≤ d, n⃗ ∩ fn[[P_{i}]] ∪ fn[[P_{i+1}]] ∪fn(th) = ∅

for each (fr ∪{n⃗}, th) ⊢ M ↔^{d} N B(((fr ∪{n⃗}, th), (P′_{i}[M/x], P′_{i+1}[N/y])))

for each P_{i} ⟶^{\overline{a}} (νc⃗)⟨M⟩P′_{i} where a ∈ fr

select a P_{i+1} ⟶^{\overline{a}} (νd⃗)⟨N⟩P′_{i+1}

if no such P′_{i+1} exists

then fail else select e ≤ (fr′, th′) such that (fr′, th′) ⊢ M ↔ N

B(((fr′, th′), P′_{i}, P′_{i+1}))

for each P_{i} ⟶^{τ} P′_{i}

select a P_{i+1} ⟶^{τ} P′_{i+1}

if no such P′_{i+1} exists

then fail else

B(((fr, th), P′_{i}, P′_{i+1}))

Table 6: A nondeterministic algorithm for checking bisimilarity

and as all transition sequences examined along recursive calls are finite due to the absence of recursion. □

Corollary 29 Let e ⊢ ok and let P and Q be finite spi-calculus processes. It is decidable whether e ⊢ P ∼_{f} Q.

7 Conclusions and further work

In this paper we have shown that framed bisimilarity is decidable for finite processes. The ideas used in this paper are closely related to those employed in giving symbolic semantics to process calculi. The precise relationship is a topic for further work.

Recent, currently unpublished results [FN01, BN02] establish that the environment sensitive bisimilarity of Boreale et al. [BDP99] corresponds to a variant of framed bisimilarity which omits the frame-component. We therefore conjecture that our results and techniques carry over to environment sensitive bisimilarity.

A topic for further work is how to develop an efficient version of the bisimulation checking algorithm. However, framed bisimulation subsumes the late bisimulation equivalence of the π-calculus and the decision problem for this latter equivalence is known to be PSPACE-complete for a number of recursion-free process calculi with value-passing [BT00].

As we have omitted recursion, we can only study attacks that involve a given number of runs of a protocol. Another topic for further work is therefore to study the class of attacks that can be detected within the finite spi-calculus.

References

[AG97a] M. Abadi and A. D. Gordon. A calculus for cryptographic protocols: The spi-calculus. In Fourth ACM Conference on Computer and Communications Security. ACM Press, 1997.

[AG98b] M. Abadi and A. D. Gordon. A bisimulation method for cryptographic protocols. Nordic Journal of Computing, 5(4), pp. 267-303, Winter 1998.

[AL00] R.M. Amadio, D. Lugiez. On the reachability problem in cryptographic protocols Proceedings of CONCUR 00, LNCS 1877, Springer-Verlag.

[BDP99] Boreale, Michele & De Nicola, Rocco & Pugliese, Rosario. Proof Techniques for Cryptographic Processes (Extended version). Proceedings of LICS 99, pp. 157–166, 1999.

[BT00] M. Boreale and L. Trevisan A Complexity Analysis of Bisimilarity for Value-passing Processes Theoretical Computer Science, Vol. 238, Number 1-2, pp. 313-345, May 2000.

[BN02] J. Borgström and U. Nestmann On Bisimulations for the Spi Calculus Submitted for publication.

[Dam97] Mads Dam On the Decidability of Process Equivalences for the π-Calculus Theoretical Computer Science, vol. 183, 1997, pp. 215–228.

[EHHN99] A.S. Elkjær, H. Hüttel, M. Höhle and K. O. Nielsen. Towards automatic bisimilarity checking in the spi calculus. Proceedings of DMTCS’99 and CATS’99. Australian Computer Science Communications, 21(3), Springer, 1999.

[FN01] U. Frendrup and J. Nyholm Jensen. Bisimilarity in the Spi-Calculus Masters’ Thesis, Department of Computer Science, Aalborg University, June 2001.

[HKNV97] Hans Hüttel, Josva Kleist, Uwe Nestmann and Björn Victor. A symbolic semantics for the spi-calculus. Unpublished manuscript.

[Lin91] Huimin Lin Complete Proof Systems for Observation Congruences in Finite-Control Pi-calculus. In Kim G. Larsen and Mogens Nielsen (editors), Automata, Languages and Programming, 25th Colloquium. Volume 1443 of Lecture Notes in Computer Science, pages 443-454, Aalborg, Denmark, July 1998, Springer-Verlag.

[MPW92] Robin Milner, Joachim Parrow and David Walker. A Calculus of Mobile Processes, Parts I and II. Information and Computation, vol. 100(1), 1992, pp. 1–77.

[Mil99] Robin Milner. Communicating and mobile systems: the πcalculus. Cambridge University Press, 1999.

[Min67] Marvin Minsky. Computation: Finite and Infinite Machines. Prentice-Hall 1967.

[NH83] Rocco De Nicola and Matthew C. B. Hennessy. Testing equivalence for processes. In Josep Díaz (editor) Automata, Languages and Programming, 10th Colloquium. Volume 154 of Lecture Notes in Computer Science, pages 548–560, Barcelona, Spain, 18–22 July 1983. Springer-Verlag.

[San96] Davide Sangiorgi. A theory of bisimulation for the π-calculus. Acta Informatica, vol. 33, 1996, pp. 69–97.

Recent BRICS Report Series Publications

RS-02-25 Hans Hüttel. Deciding Framed Bisimilarity. May 2002. 20 pp.

RS-02-24 Aske Simon Christensen, Anders Møller, and Michael I. Schwartzbach. Static Analysis of Dynamic XML. May 2002.

RS-02-23 Antonio Di Nola and Laurenţiu Leuştean. Compact Representations of BL-Algebras. May 2002. 25 pp.

RS-02-22 Mogens Nielsen, Catuscia Palamidessi, and Frank D. Valencia. On the Expressive Power of Concurrent Constraint Programming Languages. May 2002. 34 pp.

RS-02-21 ZoltánÉsik and Werner Kuich. Formal Tree Series. April 2002. 66 pp.

RS-02-20 Zoltán Ésik and Kim G. Larsen. Regular Languages Definable by Lindström Quantifiers (Preliminary Version). April 2002. 56 pp.

RS-02-19 Stephen L. Bloom and ZoltánÉsik. An Extension Theorem with an Application to Formal Tree Series. April 2002. 51 pp.

RS-02-18 Gerth Stølting Brodal and Rolf Fagerberg. Cache Oblivious Distribution Sweeping. April 2002. To appear in 29th International Colloquium on Automata, Languages, and Programming, ICALP ’02 Proceedings, LNCS, 2002.

RS-02-17 Bolette Ammitzbøll Madsen, Jesper Makholm Nielsen, and Bjarke Skjernaa. On the Number of Maximal Bipartite Subgraphs of a Graph. April 2002. 7 pp.

RS-02-16 Jiří Srba. Strong Bisimilarity of Simple Process Algebras: Complexity Lower Bounds. April 2002. To appear in 29th International Colloquium on Automata, Languages, and Programming, ICALP ’02 Proceedings, LNCS, 2002.

RS-02-15 Jesper Makholm Nielsen. On the Number of Maximal Independent Sets in a Graph. April 2002. 10 pp.

RS-02-14 Ulrich Berger and Paulo B. Oliva. Modified Bar Recursion. April 2002. 23 pp.