BRICS RS-03-47 Hüttel & Srba: Recursive Ping-Pong Protocols BRICS

Basic Research in Computer Science

Recursive Ping-Pong Protocols

Hans Hüttel Jiří Srba BRICS Report Series RS-03-47 ISSN 0909-0878 December 2003 Copyright \begin{matrix}c \\ ◯ \end{matrix} 2003, Hans Hüttel & Jiří Srba.

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/03/47/

Recursive Ping-Pong Protocols

Hans Hüttel^{⋆} and Jiří Srba^{⋆⋆}

BRICS^{⋆ ⋆ ⋆}, Dep. of Computer Science, University of Aalborg Fredrik Bajersvej 7B, 9220 Aalborg East, Denmark

Abstract. This paper introduces a process calculus with recursion which allows us to express an unbounded number of runs of the ping-pong protocols introduced by Dolev and Yao. We study the decidability issues associated with two common approaches to checking security properties, namely reachability analysis and bisimulation checking. Our main result is that our channel-free and memory-less calculus is Turing powerful, assuming that at least three principals are involved. We also investigate the expressive power of the calculus in the case of two participants. Here, our main results are that reachability and, under certain conditions, also strong bisimilarity become decidable.

1 Introduction

The study of correctness properties of cryptographic protocols has become an increasingly important research topic. Today, research on cryptographic protocols is often conducted using methods from program semantics together with the so-called Dolev-Yao assumptions about protocol principals and intruders introduced in [11]. In the Dolev-Yao model, all communications of a protocol may be visible to the hostile environment which is capable of interfering with the protocol by altering or blocking any message and by creating new messages. Moreover, these are the only kinds of attacks — an intruder cannot exploit weaknesses of the encryption algorithm itself (the ’perfect encryption hypothesis’).

Process calculi have been suggested as a natural vehicle for reasoning about cryptographic protocols. In [1], Abadi and Gordon introduced the spi-calculus (a variant of the π-calculus) and described how properties such as secrecy and authenticity can be expressed via observational equivalence. Alternatively, security properties can be expressed and examined using reachability analysis [4, 6, 14]. An important question is: Given the Dolev-Yao assumptions, to which extent are the properties of cryptographic protocols decidable?

A number of security properties are decidable for the class of finite protocols [4, 16]. In the case of an unbounded number of protocol configurations, the picture is more complex. Durgin et al. showed in [12] that security properties are

⋆ hans@cs.auc.dk ⋆⋆ srba@cs.auc.dk, supported in part by the GACR, grant No. 201/03/1161.

⋆ ⋆ ⋆

Basic Research in Computer Science,

Centre of the Danish National Research Foundation.

undecidable in a restricted class of so-called bounded protocols (that still allows for infinitely many reachable configurations). In [3] Amadio and Charatonik consider a language of tail-recursive protocols with bounded encryption depth and name generation; they show that, whenever certain restrictions on decryption are violated, one can encode two-counter machines in the process language. On the other hand, Amadio, Lugiez and Vanackère show in [5] that the reachability problem is in PTIME for a class of protocols with replication (as opposed to recursion).

Another contribution by Dolev and Yao in [11] is the study of ping-pong protocols. These are memory-less protocols which may be subjected to arbitrarily long attacks. Here, the secrecy of a finite ping-pong protocol can be decided in polynomial time. Later, Dolev, Even and Karp found a cubic-time algorithm [10] by expressing secrecy as emptiness of the intersection of a context-free language with a regular language. The class of protocols studied by Amadio et al. in [5] contains iterative ping-pong protocols and, as a consequence, secrecy properties remain polynomially decidable even in this case.

In this paper we examine decision problems for a process calculus capable of describing exactly the class of recursive ping-pong protocols. We study the calculus from the perspective of equivalence checking (for a general scheme see e.g. [15]) and consider no explicit model of the environment. The reason for considering this tiny calculus is that all negative results for it carry over to richer calculi capable of expressing a wider class of protocols (it is possible to describe an active intruder in the setting of bisimilarity/reachability checking of ping-pong protocols and this will be treated in our forthcoming paper).

The considered calculus is a channel-free process calculus, reminiscent of the tail-recursive processes studied by Amadio and Charatonik [3]. In the case of three principals, we can encode any Turing machine as a ping-pong protocol. Hence even this very restricted formalism is sufficiently expressive to encode universal computations. This implies that any richer calculus (and indeed any reasonable cryptographic calculus should subsume the ping-pong behaviour) is beyond the reach of automatic verification. The underlying idea of our construction is to encode the content of the tape as a series of encryptions and to express the transition function as a series of protocol steps. As a consequence, both reachability and bisimilarity are undecidable.

On the other hand, if the protocol is restricted to two principals, many properties become decidable. In particular, we show that the reachability problem is in PTIME, and under a certain natural observational condition also strong bisimilarity becomes decidable.

2 Basic Definitions

2.1 Transition Systems and Bisimilarity

We describe the semantics of our process calculi using unlabelled transition systems where every state has an associated set of its knowledge, which is an element of a given domain D. Intuitively, knowledge represents observations visible to the environment.

A transition system (with knowledge) is a triple (S, ⟶, kn) where S is a set of states (or processes), ⟶⊆ S × S is a transition relation, written α ⟶ β, for (α, β) ∈⟶, and kn : S ↦ D is a knowledge function from the set of states to the given knowledge domain D.

Let T = (S, ⟶, kn) be a transition system. A binary relation R ⊆ S × S is a (strong) bisimulation iff whenever (α, β) ∈ R then kn(α) = kn(β) and if α ⟶ α′ then β ⟶ β′ for some β′ such that (α′, β′) ∈ R, and if β ⟶ β′ then α ⟶ α′ for some α′ such that (α′, β′) ∈ R.

Processes α_{1}, α_{2} ∈ S are (strongly) bisimilar in T , written (α_{1}, T ) ∼ (α_{2}, T ) (or simply α_{1} ∼ α_{2} if T is clear from the context), iff there is a (strong) bisimulation R such that (α_{1}, α_{2}) ∈ R.

Given a pair of processes α_{1} in a transition system T_{1} = (S_{1}, ⟶_{1}, kn) and α_{2} in T_{2} = (S_{2}, ⟶_{2}, kn) such that S_{1} ∩ S_{2} = ∅ and kn : S_{1} ∪ S_{2} ↦ D, we write

(α_{1}, T_{1}) ∼ (α_{2}, T_{2}) iff (α_{1}, T ) ∼ (α_{2}, T ) such that T =^{def} (S_{1} ∪ S_{2}, ⟶, kn) where

α ⟶ β iff α, β ∈ S_{1} and α ⟶_{1} β, or α, β ∈ S_{2} and α ⟶_{2} β. Similarly if S_{1} and S_{2} are not disjoint, we simply rename the states of one of the transition systems and use the same notation (α_{1}, T_{1}) ∼ (α_{2}, T_{2}).

Bisimilarity has an elegant characterization in terms of bisimulation games [19, 18]. A bisimulation game on a pair of processes (α_{1}, T ) and (α_{2}, T ) is a twoplayer game of an ‘attacker’ and a ‘defender’. The game is played in rounds. In each round the attacker chooses one of the processes and performs a transition in the selected process; the defender must respond by performing a transition in the other process. Now the game repeats, starting from the new processes. If a pair of processes α_{1} and α_{2} such that kn(α_{1}) ≠ kn(α_{2}) is reached during the game, the attacker wins. If a player cannot perform a transition, the other player wins. If the game is infinite, the defender wins.

Processes (α_{1}, T ) and (α_{2}, T ) are bisimilar iff the defender has a winning strategy (and non-bisimilar iff the attacker has a winning strategy).

Two main decidability problems we shall investigate are (strong) bisimilarity checking and reachability analysis. The first problem asks the question (i) Are two given states α and β in a transition system (strongly) bisimilar (α ∼ β) ? and the second problem asks the question (ii) Is a given state β reachable from a state α, i.e., α ⟶^{∗} β ?

2.2 Ping-Pong Protocols

Let T be a set of plain-text messages and let K be a set of encryption keys. We let t range over T and k range over K. The set of messages over T encrypted with the keys from K is denoted by M(T, K) and given by the following abstract syntax.

m ::= t | {m}_{k}

Hence a message m (either a plain-text or an already encrypted message) can be encrypted with a key k, and such a message is written as {m}_{k}.

Let Const be a finite set of process constants. A specification of a ping-pong protocol is a finite set of process definitions Δ such that every process constant P ∈ Const has exactly one process definition of the form

P =^{def} ∑_{i∈I} v_{i}.\overline{w_{i}}.P_{i}

where I is a finite set of indices, v_{i} and w_{i} are messages over a fixed variable name x encrypted with the keys from K (i.e. v_{i}, w_{i} ∈ M({x}, K)), and P_{i} is either a process constant or the empty process ‘0’ (i.e. P_{i} ∈ Const∪{0}). We call v_{i} (resp. \overline{w_{i}}) the input (resp. output) prefix.

Process definitions like these will often be written in their unfolded forms P =^{def} v_{1}.\overline{w_{1}}.P_{1} +v_{2}.\overline{w_{2}}.P_{2} +⋯+v_{n}.\overline{w_{n}}.P_{n} and whenever P_{i} is the empty process 0 then instead of v_{i}.\overline{w_{i}}.0 we write only v_{i}.\overline{w_{i}}. Also, let keys(u) denote the set of keys used in u for u ∈ M(T, K), formally keys(t) =^{def} ∅ and keys({m}_{k}) =^{def} {k} ∪ keys(m).

Example 1. A simple protocol specification may look as follows:

Δ =^{def} \{P =^{def} \{x\}_{k}.\overline{\{\{x\}_{k′}\}_{k}}.P \}

where K =^{def} {k, k′}. The cyclic behaviour of the process constant P is described as follows: P receives a message and decrypts it by using the key k; the decrypted message is encrypted (using first the key k′ and then k), and sent off.

Let us finally also recall that for the prefixes {x}_{k} and {{x}_{k′}}_{k} we have keys({x}_{k}) = {k} and keys({{x}_{k′}}_{k}) = {k, k′}. ⊓ ⊔

A configuration of a ping-pong protocol specification Δ is a parallel composition of process constants, possibly preceded by output prefixes. Formally the set Conf of configurations is given by the following abstract syntax

C ::= P | \overline{w}.P | C||C

where P ∈ Const∪{0} ranges over process constants including the empty process, w ∈ M(T, K) ranges over the set of messages, and ‘||’ is the operator of the parallel composition.

We introduce a structural congruence which identifies configurations that represent the same state of the protocol. ≡ is defined as the least congruence over configurations (≡⊆ Conf × Conf) such that (Conf, ||, 0) is a commutative monoid. We identify configurations up to structural congruence.

The width of a configuration C is the minimal number of the parallel components in the ≡-equivalence class represented by C. Hence e.g. the width of 0 is 0 and the width of P ||0||Q is 2.

We shall now impose two natural restrictions on knowledge functions. We say that a knowledge function kn : Conf ↦ D for a given set D respects structural equivalence if C_{1} ≡ C_{2} implies kn(C_{1}) = kn(C_{2}) for any C_{1}, C_{2} ∈ Conf. Let C ∈ Conf be a configuration with the corresponding specification Δ. The set prefix(C) of available prefixes of C is defined by: prefix(0) =^{def} ∅; prefix(C) =^{def} ∪_{i∈I}\{v_{i}, \overline{w_{i}}\} if C ∈ Const such that (C =^{def} ∑_{i∈I} v_{i}.\overline{w_{i}}.P_{i}) ∈ Δ; prefix(C) =^{def} \{\overline{w}\} if C = \overline{w}.P

for some P ∈ Const; and prefix(C) =^{def} prefix(C_{1}) ∪ prefix(C_{2}) if C = C_{1}||C_{2}. The intuition is that the input/output capabilities of a configuration depend only on the available prefixes and not on the names of process constants. If we consistently rename the process constants in C and Δ and obtain a new configuration C′ and a new specification Δ′, it is the case that prefix(C) = prefix(C′). Hence we say that a knowledge function kn respects renaming of process constants if prefix(C_{1}) = prefix(C_{2}) implies kn(C_{1}) = kn(C_{2}) for any C_{1}, C_{2} ∈ Conf.

We only consider knowledge functions that respect structural congruence and renaming of process constants; we will call such functions respecting.

Example 2. Define the following knowledge functions kn_{∅}, kn_{priv} and kn_{plain}:

– The empty knowledge function kn_{∅} : Conf ↦ {⊥} is defined by kn_{∅}(C) =^{def} ⊥ for all C ∈ Conf.

– The private-keys knowledge function kn_{priv} : Conf ↦ 2^{K} (where K is the set of keys) is defined by kn_{priv}(C) =^{def} ⋃_{i∈I} keys(v_{i}) if C ∈ Const and

C =^{def} ∑_{i∈I} v_{i}.\overline{w_{i}}.P_{i}, kn_{priv}(C) =^{def} kn_{priv}(C_{1}) ∪ kn_{priv}(C_{2}) if C = C_{1}||C_{2}

and kn_{priv}(C) =^{def} ∅ otherwise.

– The plain-text knowledge function kn_{plain} : Conf ↦ 2^{T} (where T is the set of plain-text messages), is defined by kn_{plain}(C) =^{def} \{t\} if C = \overline{t}.P for some t ∈ T and P ∈ Const, kn_{plain}(C) =^{def} kn_{plain}(C_{1}) ∪ kn_{plain}(C_{2}) if C = C_{1}||C_{2} and kn_{plain}(C) =^{def} ∅ otherwise.

It is easy to see that these knowledge functions are respecting. The intuition is that kn_{∅} does not take the knowledge of configurations into account and hence in bisimilarity checking only the branching structure induced by ⟶ is relevant. The knowledge function kn_{priv} makes sure that any two bisimilar configurations have the same decryption keys currently available. Finally, the function kn_{plain} identifies configurations which are currently capable of communicating the same set of plain-text messages. ⊓ ⊔

Example 3. Consider a ping-pong protocol motivated by a simple example mentioned e.g. in [10] and [11]. A participant X wants to send a message m ∈ {0, 1}^{∗} to a participant Y and get a confirmation that the message was received. The protocol is informally described as follows: (i) participant X encrypts the message m by a public key of Y and sends the encrypted message to Y, (ii) participant Y decrypts the received message by his private key and answers to X by the same message m encrypted with X’s public key, (iii) finally X receives the confirmation message and decrypts it by his private key.

In our formalism let T =^{def} {0, 1}^{∗}, K =^{def} {k_{X}, k_{Y} }, and Const =^{def} {X, Y }. The protocol specification Δ is given by two equations

X =^{def} \{x\}_{k_{X}} .\overline{\{x\}_{k_{Y}}} .X Y =^{def} \{x\}_{k_{Y}} .\overline{\{x\}_{k_{X}}}

\frac{(P =^{def} ∑_{i∈I} v_{i}.\overline{w_{i}}.P_{i}) ∈ Δ u = v_{i}[m/x] m ∈ M(T, K) i ∈ I}{P || \overline{u}.Q ⟶ \overline{w_{i}[m/x]}.P_{i} || Q}

\frac{P ⟶ P′}{P ||Q ⟶ P′||Q}

Fig. 1. SOS rules of ping-pong protocols

and the initial configuration of the protocol is \overline{\{m\}_{k_{Y}}} .X || Y for a given m ∈ T.

The intuition is that the process \overline{\{m\}_{k_{Y}}} .X can output the message m encrypted with the key k_{Y} and become the process X. Similarly, Y can input this message and become the process \overline{\{m\}_{k_{X}}} .Y. After the communication is established, the new configuration X || \overline{\{m\}_{k_{X}}} .Y is reached. The conformation phase of the protocol is analogous to the first communication. ⊓ ⊔

Note that we do not distinguish explicitly between private and public keys. This is done implicitly: a key supposed to be a private key for one or more process constants cannot be used in the input prefixes of other process constants. E.g. in our example k_{X} is a private key of X which means the process constant Y can use the key only in its output prefix and vice versa.

A formal semantics of ping-pong protocols is given in terms of transition systems. First, we define inductively a substitution u[m′/x] of the message m′ for the variable x in the prefix u (m′ ∈ M(T, K) and u ∈ M({x}, K)) by

x[m′/x] =^{def} m′ and {m}_{k}[m′/x] =^{def} {m[m′/x]}_{k}.

A given protocol specification Δ determines a transition system T (Δ) =^{def} (S, ⟶, kn) where states are configurations of the protocol modulo the structural congruence (S =^{def} Conf/≡); the transition relation ⟶ is given by the SOS rules in Figure 1 (recall that ‘||’ is commutative); and the knowledge function kn : S ↦ D is assumed to be explicitly given. Note that the width of a configuration does not increase by performing a transition.

Example 4. Let us consider the ping-pong protocol specification from Example 3. The interesting fragment of the transition system T (Δ) is

\xymatrix{\overline{\{m\}_{k_{Y}}} .X || Y \ar[r] & X || \overline{\{m\}_{k_{X}}} .Y \ar[r] & \overline{\{m\}_{k_{Y}}} .X}  ⊓ ⊔

In the rest of this section we will discuss the usefulness of bisimilarity checking with knowledge functions for validation of authenticity and secrecy of ping-pong protocols. The correctness checking of such protocols is done by comparing the protocol specification with its ideal behaviour [2] under an appropriate choice of the knowledge function.

For example, assume that we want to check whether a given protocol specification Δ ever outputs a plain-text message. Let us fix an arbitrary key k ∈ K.

We define an ideal protocol Δ′ which has the same behaviour as Δ but never communicates any plain-text message. This can be achieved e.g. by defining

Δ′ =^{def} \{P =^{def} ∑_{i∈I}\{v_{i}\}_{k}.\overline{\{w_{i}\}_{k}}.P_{i} | (P =^{def} ∑_{i∈I} v_{i}.\overline{w_{i}}.P_{i}) ∈ Δ\}.

For any configuration C ∈ Conf let C′ be a configuration where every occurrence of an output prefix of the form \overline{w}.P is replaced with \overline{\{w\}_{k}}.P. Under the assumption that the plain-text knowledge function kn_{plain} is used, it holds that (C, T (Δ)) ∼ (C′, T (Δ′)) if and only if the protocol Δ starting from its initial configuration C is never capable of outputting any plain-text message.

Assume now that Δ contains input prefixes only of the from {x}_{k} for some key k ∈ K (only one key decryption at a time). The question whether a computation from a given configuration C of the protocol specification Δ never deadlocks and it is always possible to decrypt messages encrypted with a fixed key k can be expressed as follows. Let Δ′ =^{def} \{X =^{def} \{x\}_{k}.\overline{\{x\}_{k}}.X\} and let C′ be the configuration \overline{\{t\}_{k}}.X || X for some t ∈ T. Obviously, from C′ there is exactly one transition leading back to C′ and moreover C′ is always capable of decrypting a message encrypted with the key k. We also define a knowledge function kn : Conf ↦ {0, 1} by kn(C_{1}) =^{def} 1 if k ∈ kn_{priv}(C_{1}); and kn(C_{1}) =^{def} 0 otherwise. Here kn_{priv} is the private-keys knowledge function introduced before. The considered validation question is now equivalent to the problem (C, T (Δ)) ∼ (C′, T (Δ′)).

Remark 1. If instead of kn defined above we use kn_{∅}, the bisimilarity question (C, T (Δ)) ∼ (C′, T (Δ′)) is equivalent to the problem whether there is no terminating computation of the protocol Δ starting in C.

3 Ping-Pong Protocols of Width 3

In this section we show that ping-pong protocols of width at least 3 are surprisingly powerful enough to simulate Turing machines.

Let M = (Q, Σ, γ, q_{0}, q_{F}) be a Turing machine such that Q is a finite set of control states, Σ is a finite tape alphabet containing special symbols c, $ ∈ Σ (c is the left mark of the tape and $ it the right mark; let Σ_{1} =^{def} Σ ∖{c, $}), q_{0} ∈ Q is the initial state, q_{F} is the final state and

γ : Σ×Q×Σ ↦ (Q×Σ×Σ ∪ Σ×Σ×Q ∪ {halt})

is a total function such that

– γ(aqb) ∈ (Q×{a}×Σ_{1} ∪ {a}×Σ_{1}×Q) for all a, b ∈ Σ_{1} and q ∈ Q (the head moves either to the left or to the right)

– γ(cqa) ∈ {c}×Σ_{1}×Q for all a ∈ Σ and q ∈ Q (the head is not allowed to move on the left mark)

– γ(aq$) ∈ (Q×{a}×{$} ∪ {a}×Σ_{1}×Q) for all a ∈ Σ and q ∈ Q (the right mark cannot be changed but the head can move to the right)

– γ(aq_{F} b) = halt for all a, b ∈ Σ (when the final state q_{F} is reached, the computation stops).

A configuration of the machine M is an element from the set {c}×Σ_{1}^{∗}×Q×Σ_{1}^{∗}×{$}. A computational step between configurations c_{1} and c_{2} (written c_{1} ⟶ c_{2}) is defined in the usual way, i.e.,

– c_{1} ⟶ c_{2} if c_{1} ≡ w_{1}aqbw_{2} and c_{2} ≡ w_{1}γ(aqb)w_{2} where w_{1}, w_{2} ∈ Σ^{∗}, a, b ∈ Σ and q ∈ Q such that b ≠ $, or (b = $ ∧ γ(aqb) ∈ Q×{a}×{$}) (the head does not write on the right mark), or

– c_{1} ⟶ c_{2} if c_{1} ≡ w_{1}aq$ and c_{2} ≡ w_{1}γ(aq$)$ where w_{1} ∈ Σ^{∗}, a ∈ Σ and q ∈ Q such that γ(aq$) ∈ {a}×Σ_{1} ×Q (the head is at the end mark and moves to the right).

It is a well known fact that the problem whether the machine halts from the initial configuration cq_{0}$ (i.e. reaches a configuration containing the state q_{F} in a finite number of computational steps) is undecidable.

Let M = (Q, Σ, γ, q_{0}, q_{F}) be a Turing machine and let S =^{def} Q ∪ Σ ∪ {z} and S′ =^{def} {s′ | s ∈ S} such that z is a fresh symbol and S ∩S′ = ∅. We define a pingpong protocol Δ that will simulate the computation of the machine M. The set of plain-text messages is a singleton set T =^{def} {t}, the set of keys is K =^{def} S ∪ S′, and the set of process constants consists of Const =^{def} {B_{S}, B_{S′}, P, R} ∪ {P_{a′}, R_{a} | a ∈ S} ∪ {V_{a′b′c′}, V_{a′b′c′$′} | a, b, c ∈ S}.

First, we define the equations for process constants B_{S} and B_{S′} (buffers over S and S′).

B_{S} =^{def} ∑_{s∈S}\{x\}_{s}.\overline{\{x\}_{s}}.B_{S} B_{S′} =^{def} ∑_{s′∈S′}\{x\}_{s′}.\overline{\{x\}_{s′}}.B_{S′}

The intuition is that the buffers B_{S} and B′_{S} can store their content as a sequence of encryption keys over S resp. S′. In our case the buffers will store configurations of the machine M.

The process constant P transfers the content of the buffer B_{S} to the buffer B_{S′} and as soon as a control state is present, the computational step is performed. This is formally defined by

P =^{def} ∑_{a,b,c∈S, b∉Q}\{\{\{x\}_{c}\}_{b}\}_{a}.\overline{\{\{x\}_{c}\}_{b}}.P_{a′} +

∑_{a,c∈Σ, q∈Q, γ(aqc)=efg, ¬ω}\{\{\{x\}_{c}\}_{q}\}_{a}.\overline{x}.V_{e′f′g′} +

∑_{a,c∈Σ, q∈Q, γ(aqc)=efg, ω}\{\{\{x\}_{c}\}_{q}\}_{a}.\overline{x}.V_{e′f′g′$′}

where ω is the condition saying that the head is at the end of the tape and it moves to the right, i.e., ω ≡ c = $ ∧ g ∈ Q.

The process constant P_{a′} for all a′ ∈ S′ simply adds the symbol a′ to the buffer B_{S′} and then it continues as P.

P_{a′} =^{def} ∑_{s′∈S′}\{x\}_{s′}.\overline{\{\{x\}_{s′}\}_{a′}}.P

The process constants V_{a′b′c′} and V_{a′b′c′$′} (for a′, b′, c′ ∈ S′) add the corresponding sequence of keys to the buffer B_{S′} and then continue as R.

V_{a′b′c′} =^{def} ∑_{s′∈S′}\{x\}_{s′}.\overline{\{\{\{\{x\}_{s′}\}_{a′}\}_{b′}\}_{c′}}.R

V_{a′b′c′$′} =^{def} ∑_{s′∈S′}\{x\}_{s′}.\overline{\{\{\{\{\{x\}_{s′}\}_{a′}\}_{b′}\}_{c′}\}_{$′}}.R

We finish the definition of the process constants by introducing R (standing for ‘reverse’), which transfers the content of the buffer B_{S′} back to B_{S}.

R =^{def} ∑_{a′∈S′}\{x\}_{a′}.\overline{x}.R_{a}

Similarly as P_{a′}, R_{a} for all a ∈ S ∖ {c} adds the symbol a to the buffer B_{S} and continues as R, except for the situation when the beginning of the tape was reached (in this case R_{c} continues as P).

R_{a} =^{def} ∑_{s∈S}\{x\}_{s}.\overline{\{\{x\}_{s}\}_{a}}.R R_{c} =^{def} ∑_{s∈S}\{x\}_{s}.\overline{\{\{x\}_{s}\}_{c}}.P

Let m =^{def} {t}_{z} and m′ =^{def} {t}_{z′} (recall that t ∈ T is the only plain-text message). The following configuration of width 3 can simulate the computation of the machine M from the initial configuration cq_{0}$.

\overline{\{\{\{m\}_{$}\}_{q_{0}}\}_{c}}.B_{S} || \overline{m′}.B_{S′} || P

In order to see how the simulation works we use the notations [w]_{m} and [w]_{m′} to denote the messages m and m′ encrypted with the sequence of keys w, i.e., [ϵ]_{m} =^{def} m, [ϵ]_{m′} =^{def} m′, [aw]_{m} =^{def} {[w]_{m}}_{a} and [aw]_{m′} =^{def} {[w]_{m′}}_{a} where ϵ is the empty sequence, a ∈ K and w ∈ K^{∗}.

Now every configuration c of the machine M corresponds to the configuration f(c) =^{def} (\overline{[c]_{m}}.B_{S} || \overline{[ϵ]_{m′}}.B_{S′} || P) of the protocol Δ. Note that the initial configuration of Δ defined above is exactly f(cq_{0}$).

The following considerations will describe the simulation of the Turing machine M by the protocol Δ. A single step of the machine M will be simulated by a finite number of transitions in the protocol.

Let c_{1} = w_{1}aqcw_{2} and c_{2} = w_{1}efgw_{2} be configurations of M such that w_{1}, w_{2} ∈ Σ^{∗}, a, c ∈ Σ, q ∈ Q, γ(aqc) = efg, and ¬ω. This means that c_{1} ⟶ c_{2}. We will show that f(c_{1}) ⟶^{∗} f(c_{2}) such that the computation of the protocol from f(c_{1}) is deterministic, i.e., for any C ∈ Conf such that f(c_{1}) ⟶^{∗} C it is the case that C ⟶ C′ and C ⟶ C′′ implies C′ ≡ C′′. For w_{1} in the form a_{1} ⋯ a_{n} let w′_{1,R} =^{def} a′_{n} ⋯ a′_{1} be the reversed word w_{1} such that every letter is primed. The computation from f(c_{1}) looks as follows.

f(c_{1}) = \overline{[w_{1}aqcw_{2}]_{m}}.B_{S} || \overline{[ϵ]_{m′}}.B_{S′} || P ⟶^{∗} \overline{[aqcw_{2}]_{m}}.B_{S} || \overline{[w′_{1,R}]_{m′}}.B_{S′} || P ⟶

B_{S} || \overline{[w′_{1,R}]_{m′}}.B_{S′} || \overline{[w_{2}]_{m}}.V_{e′f′g′} ⟶ \overline{[w_{2}]_{m}}.B_{S} || \overline{[w′_{1,R}]_{m′}}.B_{S′} || V_{e′f′g′} ⟶

\overline{[w_{2}]_{m}}.B_{S} || B_{S′} || \overline{[g′f′e′w′_{1,R}]_{m′}}.R ⟶ \overline{[w_{2}]_{m}}.B_{S} || \overline{[g′f′e′w′_{1,R}]_{m′}}.B_{S′} || R ⟶^{∗}

\overline{[w_{1}efgw_{2}]_{m}}.B_{S} || \overline{[ϵ]_{m′}}.B_{S′} || P = f(c_{2})

It is easy to observe that such a computation is unique (deterministic).

Let c_{1} = w_{1}aq$ and c_{2} = w_{1}efg$ be configurations of M as before, however, this time the condition ω holds. This case is analogous to the previous one. The only difference is that V_{e′f′g′} is replaced with V_{e′f′g′$′} and the end of the tape $ is added (the tape hence becomes longer by one cell). Assume now that f(c_{1}) represents a halting configuration. The computation of the protocol from f(c_{1}) starts as before, however, there is no summand in the definition of the process constant P for the situation that γ(aqc) = halt and hence the computation gets stuck in the configuration \overline{[aqcw_{2}]_{m}}.B_{S} || \overline{[w′_{1,R}]_{m′}}.B_{S′} || P.

The following theorems are applications of the presented simulation.

Theorem 1. Reachability is undecidable for ping-pong protocols of width 3.

Theorem 2. Bisimilarity is undecidable for ping-pong protocols of width 3 for any knowledge function which respects structural congruence and renaming of process constants.

4 Ping-Pong Protocols of Width 2

If the family of protocols we consider contains at most two participants (parallel components), we get a class similar to that of the traditional ping-pong protocols [10, 11]. In fact, our class is more general in the sense that we allow for recursive definitions in the protocol specification. In the situation of at most two parallel components in any reachable configuration we may without loss of generality assume that such configurations are always of the form P || \overline{w}.Q for some P ∈ Const, Q ∈ Const ∪ {0} and w ∈ M(T, K). If this is not the case, the computation of such a protocol is stuck — no communication can take place.

We shall now observe that the class of ping-pong protocols of width 2 is not Turing powerful since e.g. reachability becomes decidable. Hence we can still hope for automatic verification of some protocol properties.

Theorem 3. The reachability problem for ping-pong protocols of width 2 is decidable in polynomial time.

In contrast, the bisimilarity problem is again undecidable.

Theorem 4. The problem of bisimilarity checking between a pair of ping-pong protocol configurations of width 2 is undecidable (provided that we allow for general but still computable, respecting and finite-domain knowledge functions).

In most of the examples of knowledge functions we, however, do not use knowledge functions similar to the one described in the undecidability proof. In fact, it is quite satisfactory to consider knowledge functions which depend only on a constant number of the upper-most symbols in the output prefix. We shall prove that if this is the case then bisimilarity becomes decidable.

Let P || \overline{w}.Q be a general form of a protocol configuration of width 2. A knowledge function kn is local if there is a constant M ∈ ℕ^{0} and a function

f : (Const ∪ {0}) × (Const ∪ {0}) × ((K^{<M} × T) ∪ K^{M}) ↦ D

such that kn(P || \overline{w}.Q) = f(P, Q, w′) where w′ is ⟨w⟩ if |⟨w⟩| ≤ M, and w′ is the prefix of ⟨w⟩ of length M otherwise. In other words, a local knowledge function depends only on P, Q and at most M outer-most keys of w.

Remark 2. Observe that local knowledge functions have finite co-domains. Hence for every local knowledge function there is an equivalent local knowledge function with a finite domain D. In what follows we shall assume that D is finite.

Theorem 5. The problem of bisimilarity checking between a pair of ping-pong protocol configurations of width 2 is decidable for local knowledge functions.

5 Conclusion

We have studied a simple, channel-free process calculus capable of describing recursive ping-pong protocols. Surprisingly, the calculus turns out to be Turingpowerful when we allow three or more principals. This implies that all interesting verification problems will remain undecidable in any richer calculus which can express at least the ping-pong behaviour. This fact remains valid even if we allow active attacks on the protocol since the syntax of ping-pong protocols is capable of describing this situation. This is, however, nontrivial to see and it is a part of our current work.

In the case of two principals, the reachability problem is in PTIME. Depending on our notion of observability, other properties (including strong bisimilarity) may also become decidable.

Amadio et al. in [5] have proved that reachability is polynomially decidable for processes with replication. However, they have only shown the result for a class of processes that, unlike the class studied in the present paper, does not involve an explicit representation of nondeterministic choice. It remains to be seen whether security properties are decidable for a version of our process calculus with replication replacing recursion, and whether our calculus without explicit nondeterminism remains Turing powerful. We claim that at least the latter is indeed the case and in our future work we shall further investigate the problem (including the connection with the results from [9] where it is shown that secrecy is decidable for protocols with replication but without nondeterminism).

References

1. Martin Abadi and Andrew D. Gordon. A bisimulation method for cryptographic protocols. Nordic Journal of Computing, 5(4):267–303, 1998.

2. Martin Abadi and Andrew D. Gordon. A calculus for cryptographic protocols: The spi calculus. Information and Computation, 148(1):1–70, 1999.

3. R.M. Amadio and W. Charatonik. On name generation and set-based analysis in the Dolev-Yao model. In Proceedings of the 13th International Conference on Concurrency Theory (CONCUR’02), volume 2421 of LNCS, pages 499–514. Springer-Verlag, 2002.

4. R.M. Amadio and D. Lugiez. On the reachability problem in cryptographic protocols. In Proceedings of the 11th International Conference on Concurrency Theory (CONCUR’00), volume 1877 of LNCS, pages 380–394. Springer-Verlag, 2000.

5. Roberto M. Amadio, Denis Lugiez, and Vincent Vanackère. On the symbolic reduction of processes with cryptographic functions. Theoretical Computer Science, 290(1):695–740, October 2002.

6. Michele Boreale. Symbolic trace analysis of cryptographic protocols. In 28th Colloquium on Automata, Languages and Programming (ICALP), volume 2076 of LNCS, pages 667–681. Springer, July 2001.

7. A. Bouajjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata: Application to model-checking. In Proceedings of the 8th International Conference on Concurrency Theory (CONCUR’97), volume 1243 of LNCS, pages 135–150. Springer-Verlag, 1997.

8. J.R. Büchi. Regular canonical systems. Arch. Math. Logik u. Grundlagenforschung, 6:91–111, 1964.

9. H. Comon-Lundh and V. Cortier. New decidability results for fragments of firstorder logic and application to cryptographic protocols. In Proceedings of Rewriting Techniques and Applications (RTA’03), number 2706 in LNCS, pages 148–164. Springer-Verlag, 2003.

10. D. Dolev, S. Even, and R.M. Karp. On the security of ping-pong protocols. Information and Control, 55(1–3):57–68, 1982.

11. D. Dolev and A.C. Yao. On the security of public key protocols. Transactions on Information Theory, IT-29(2):198–208, 1983.

12. N. Durgin, P. Lincoln, J. Mitchell, and A. Scedrov. Undecidability of bounded security protocols. In N. Heintze and E. Clarke, editors, Proceedings of Workshop on Formal Methods and Security Protocols (FMSP’99), July 1999.

13. J. Esparza, D. Hansel, P. Rossmanith, and S. Schwoon. Efficient algorithms for model checking pushdown systems. In Proceedings of the 12th International Conference on Computer Aided Verification (CAV’00), volume 1855 of LNCS, pages 232–247. Springer-Verlag, 2000.

14. M. Fiore and M. Abadi. Computing symbolic models for verifying cryptographic protocols. In 14th IEEE Computer Security Foundations Workshop (CSFW ’01), pages 160–173, Washington - Brussels - Tokyo, June 2001. IEEE.

15. R. Focardi, R. Gorrieri, and F. Martinelli. Non interference for the analysis of cryptographic protocols. In Proceedings of the 27th International Colloquium on Automata, Languages and Programming (ICALP’00), volume 1853 of LNCS, pages 354–372. Springer-Verlag, 2000.

16. M. Rusinowitch and M. Turuani. Protocol insecurity with a finite number of sessions and composed keys is NP-complete. TCS: Theoretical Computer Science, 299, 2003.

17. G. Sénizergues. Decidability of bisimulation equivalence for equational graphs of finite out-degree. In Proceedings of the 39th Annual Symposium on Foundations of Computer Science(FOCS’98), pages 120–129. IEEE Computer Society, 1998.

18. C. Stirling. Local model checking games. In Proceedings of the 6th International Conference on Concurrency Theory (CONCUR’95), volume 962 of LNCS, pages 1–11. Springer-Verlag, 1995.

19. W. Thomas. On the Ehrenfeucht-Fraïssé game in theoretical computer science (extended abstract). In Proceedings of the 4th International Joint Conference CAAP/FASE, Theory and Practice of Software Development (TAPSOFT’93), volume 668 of LNCS, pages 559–568. Springer-Verlag, 1993.

A Appendix

Theorem 1. Reachability is undecidable for ping-pong protocols of width 3.

Proof. Let M be a Turing machine and let Δ be the ping-pong protocol constructed above. We modify Δ by adding the following summand to the definition of the process constant P

∑_{a,c∈Σ, q∈Q, γ(aqc)=halt}\{\{\{x\}_{c}\}_{q}\}_{a}.\overline{x}.D

where D is a new process constant with its definition

D =^{def} ∑_{a∈S∪S′}\{x\}_{a}.\overline{x}.D.

This means that M halts if and only if a protocol configuration containing D is reachable. The process constant D can remove the content of both of the buffers and hence the question whether the configuration \overline{m}.B_{S} || \overline{m′}.B_{S′} || D is reachable from the initial configuration f(cq_{0}$) is undecidable. ⊓ ⊔

Theorem 2. Bisimilarity is undecidable for ping-pong protocols of width 3 for any knowledge function which respects structural congruence and renaming of process constants.

Proof. Let M be a Turing machine and let Δ be the ping-pong protocol constructed above. Let Δ′ be a copy of Δ such that every process constant X ∈ Const in Δ′ is replaced with X′. Moreover, Δ also contains the following extra summand in the definition of the process constant P

∑_{a,c∈Σ, q∈Q, γ(aqc)=halt}\{\{\{x\}_{c}\}_{q}\}_{a}.\overline{\{\{\{x\}_{c}\}_{q}\}_{a}}

and Δ′ contains the following extra summand in the definition of the process constant P′ plus a definition of a fresh process constant Z′

∑_{a,c∈Σ, q∈Q, γ(aqc)=halt}\{\{\{x\}_{c}\}_{q}\}_{a}.\overline{\{\{\{x\}_{c}\}_{q}\}_{a}}.Z′

Z′ =^{def} ∑_{a,c∈Σ, q∈Q, γ(aqc)=halt}\{\{\{x\}_{c}\}_{q}\}_{a}.\overline{\{\{\{x\}_{c}\}_{q}\}_{a}}.Z′.

If the machine M diverges then the initial configurations (as described above) of Δ and Δ′ are bisimilar since both of them are capable of performing infinite computations (these computations are deterministic) and the knowledge function cannot distinguish between them (it respects renaming of process constants).

If the machine M halts then Δ′ can still perform an infinite sequence of transitions but Δ gets stuck after using the extra summand in P defined above. Hence their initial configurations cannot be bisimilar for any knowledge function.

⊓ ⊔

Theorem 3. The reachability problem for ping-pong protocols of width 2 is decidable in polynomial time.

Proof. We reduce reachability of ping-pong protocols of width 2 to reachability of pushdown automata (PDA), disregarding the input alphabet. In fact, we will use a slightly more general notion of PDA where several stack symbols can be removed in one computational step.

Let Δ be a given protocol specification and let P_{1} || \overline{w_{1}}.Q_{1} and P_{2} || \overline{w_{2}}.Q_{2} be two configurations of the protocol. We shall construct a PDA system together with two configurations p_{1}α_{1} and p_{2}α_{2} such that P_{1} || \overline{w_{1}}.Q_{1} ⟶^{∗} P_{2} || \overline{w_{2}}.Q_{2} if and only if p_{1}α_{1} ⟶^{∗} p_{2}α_{2}.

Let m ∈ M(T, K). By ⟨m⟩ ∈ (K ∪ T)^{∗} we understand the sequence of keys that occur in m followed by the corresponding plain-text message, i.e., ⟨t⟩ = t for t ∈ T and ⟨{m}_{k}⟩ = k⟨m⟩. Similarly, if m ∈ M({x}, K) then ⟨m⟩ ∈ K^{∗} denotes the sequence of keys that occur in m, i.e., ⟨x⟩ = ϵ and ⟨{m}_{k}⟩ = k⟨m⟩.

The set of control states of the PDA automaton is {(P, Q) | P, Q ∈ Const ∪ {0}} and the stack alphabet contains the encryption keys plus plain-text messages, i.e., it is the set K ∪ T. The set of (input) actions is a singleton set {a}. We have now a natural correspondence between configurations of the protocol and those of the PDA system. A protocol configuration P || \overline{w}.Q corresponds to a PDA configuration (P, Q)⟨w⟩ such that (P, Q) is the control state (its second component is always the one that has an output prefix) and ⟨w⟩ is the stack content. The PDA rewrite rules are defined as follows: (P, Q)⟨v_{i}⟩ ⟶^{a} (Q, P_{i})⟨w_{i}⟩ for every P ∈ Const and Q ∈ Const ∪ \{0\} such that P =^{def} ∑_{i∈I} v_{i}.\overline{w_{i}}.P_{i}.

It is now easy to see that P_{1} || \overline{w_{1}}.Q_{1} ⟶^{∗} P_{2} || \overline{w_{2}}.Q_{2} if and only if (P_{1}, Q_{1})⟨w_{1}⟩ ⟶^{∗} (P_{2}, Q_{2})⟨w_{2}⟩.

The reachability problem of extended PDA is by standard techniques reducible to reachability of ordinary PDA where at most one stack symbol is removed by performing a single transition (it is enough to replace every rule of the form px_{1}x_{2} … x_{m} ⟶ qα by the rules px_{1} ⟶ p_{1}, p_{1}x_{2} ⟶ p_{2}, …, p_{m−1}x_{m} ⟶ qα where p_{1}, …, p_{m−1} are new control states).

Since reachability of PDA is decidable [8], we can conclude that reachability of ping-pong protocols of width 2 is also decidable. Moreover, the reachability problem of ordinary PDA can be solved in polynomial time [7, 13], which implies that reachability of ping-pong protocols of width 2 is decidable also in PTIME.

⊓ ⊔

Definition 1. A Minsky machine R with two counters c_{1} and c_{2} is a finite sequence of instructions

R = (I_{1}, I_{2}, …, I_{n−1}, n : halt)

where n ≥ 1 and every I_{p}, 1 ≤ p ≤ n − 1 is an instruction of one from the following two types:

– increment: p : c_{i} := c_{i} + 1; goto q

– test and decrement: p : if c_{i} = 0 then goto q else c_{i} := c_{i} − 1; goto r where 1 ≤ i ≤ 2 and 1 ≤ q, r ≤ n.

Definition 2. A configuration of a Minsky machine R is a triple (p, v_{1}, v_{2}) where p is an instruction label (1 ≤ p ≤ n), and v_{1}, v_{2} ∈ ℕ^{0} are nonnegative integers representing the values of the counters c_{1} and c_{2}, respectively. The transition relation ⟶ between configurations is defined in the natural way.

Note that the computation of R is deterministic, i.e., if (p, v_{1}, v_{2}) ⟶ (p′, v′_{1}, v′_{2}) and (p, v_{1}, v_{2}) ⟶ (p′′, v′′_{1}, v′′_{2}) the p′ = p′′, v′_{1} = v′′_{1} and v′_{2} = v′′_{2}.

Definition 3. A Minsky machine R halts with the initial counter values set to zero if (1, 0, 0) ⟶^{∗} (n, v_{1}, v_{2}) for some v_{1}, v_{2} ∈ ℕ^{0}. If R does not halt we say that it diverges.

Proposition 1. The halting problem for Minsky machines in undecidable.

Let R be a given Minsky machine. We now construct a ping-pong protocol specification Δ and two configurations C_{1} and C_{2} of width 2 such that R diverges if and only if (C_{1}, T (Δ)) ∼ (C_{2}, T (Δ)).

Let the set of plain-text messages be T =^{def} {t}, let the set of encryption keys

be K =^{def} {1, …, n} ∪ {+_{i}, −_{i} | 1 ≤ i ≤ 2} ∪ {p_{=0}^{i}, p_{≥0}^{i}, p^{cheat} | 1 ≤ p < n, 1 ≤

i ≤ 2} and let Const =^{def} {B_{K}, P, Q}. The constant B_{K} stands for a buffer over a certain subset of K.

Let #_{k}(m) denote the number of occurrences of the key k ∈ K in the message m ∈ M(T, K). The intuition of the reduction is that a configuration (p, v_{1}, v_{2}) of the Minsky machine R corresponds to a pair of protocol configurations \overline{\{m\}_{p}}.B_{K} || P and \overline{\{m\}_{p}}.B_{K} || Q such that #_{+_{i}}(m) − #_{−_{i}}(m) = v_{i} for 1 ≤ i ≤ 2. The definitions of the process constants P and Q are almost symmetric except for the situation when a halting configuration of the machine R is reachable. In this case the computation from the configuration containing Q is stuck while the configuration containing P performs an infinite sequence of transition. The knowledge function is designed in such a way that if a correct computation of the machine R is simulated by the attacker in the bisimulation game (a single step in the computation of R will be simulated by two transitions in Δ), the defender can only mimic the same transitions in the other process. However, if the attacker “cheats” in the bisimulation game (e.g. decreases a value of a counter into negative integers), the defender threatens by entering a syntactically equal (and hence bisimilar) pair of protocol configurations.

Formally, the protocol Δ is given as follows.

B_{K} =^{def} ∑_{k∈\{1,...,n\}}\{x\}_{k}.\overline{\{x\}_{k}}.B_{K} +

∑_{All(p)} (\{x\}_{p_{=0}^{i}}.\overline{\{x\}_{p}}.B_{K} + \{x\}_{p_{≥0}^{i}}.\overline{\{x\}_{p}}.B_{K} +

\{x\}_{p^{cheat}}.\overline{\{x\}_{p}}.B_{K})

P =^{def} ∑_{Inc(p)}\{x\}_{p}.\overline{\{\{x\}_{+_{i}}\}_{q}}.P +

∑_{Dec(p)} (\{x\}_{p}.\overline{\{x\}_{q_{=0}^{i}}}.P + \{x\}_{p}.\overline{\{x\}_{q^{cheat}}}.P +

\{x\}_{p}.\overline{\{x\}_{q^{cheat}}}.Q) +

∑_{Dec(p)} (\{x\}_{p}.\overline{\{\{x\}_{−_{i}}\}_{r_{≥0}^{i}}}.P + \{x\}_{p}.\overline{\{\{x\}_{−_{i}}\}_{r^{cheat}}}.P +

\{x\}_{p}.\overline{\{\{x\}_{−_{i}}\}_{r^{cheat}}}.Q) + \{x\}_{n}.\overline{\{x\}_{n}}.P

Q =^{def} ∑_{Inc(p)}\{x\}_{p}.\overline{\{\{x\}_{+_{i}}\}_{q}}.Q +

∑_{Dec(p)} (\{x\}_{p}.\overline{\{x\}_{q_{=0}^{i}}}.Q + \{x\}_{p}.\overline{\{x\}_{q^{cheat}}}.Q +

\{x\}_{p}.\overline{\{x\}_{q^{cheat}}}.P ) +

∑_{Dec(p)} (\{x\}_{p}.\overline{\{\{x\}_{−_{i}}\}_{r_{≥0}^{i}}}.Q + \{x\}_{p}.\overline{\{\{x\}_{−_{i}}\}_{r^{cheat}}}.Q +

\{x\}_{p}.\overline{\{\{x\}_{−_{i}}\}_{r^{cheat}}}.P )

where Inc(p) =^{def} 1 ≤ p < n ∧ I_{p} = (p : c_{i} := c_{i} + 1; goto q), and Dec(p) =^{def} 1 ≤ p < n ∧ I_{p} = (p : if c_{i} = 0 then goto q else c_{i} := c_{i} − 1; goto r),

and All(p) =^{def} 1 ≤ p ≤ n ∧ 1 ≤ i ≤ 2.

We shall now argue that R diverges if and only if

\overline{\{t\}_{1}}.B_{K} || P ∼ \overline{\{t\}_{1}}.B_{K} || Q

in T (Δ) where the knowledge function

kn : Conf ↦ {OK_{=0} , OK_{≥0} , CHEAT , OTHER}

is defined as follows (let i ∈ {1, 2}, X, Y ∈ {B_{K}, P, Q}, and p ∈ {1, …, n − 1}).

kn(X || \overline{\{m\}_{p_{=0}^{i}}}.Y) =^{def} \{ \begin{matrix}OK_{=0} & if #_{+_{i}}(m) = #_{−_{i}}(m) \\ CHEAT & otherwise \end{matrix}

kn(X || \overline{\{m\}_{p_{≥0}^{i}}}.Y) =^{def} \{ \begin{matrix}OK_{≥0} & if #_{+_{i}}(m) ≥ #_{−_{i}}(m) \\ CHEAT & otherwise \end{matrix}

kn(X || \overline{\{m\}_{p^{cheat}}}.Y) =^{def} CHEAT

For all other configurations C let kn(C) =^{def} OTHER.

Remark 3. Note that kn is a computable and respecting knowledge function, and that its knowledge domain is finite.

Lemma 1. If R halts then the attacker has a winning strategy in the bisimulation game played from the pair of configurations \overline{\{t\}_{1}}.B_{K} || P and \overline{\{t\}_{1}}.B_{K} || Q.

Proof. Assume that (1, 0, 0) ⟶^{∗} (n, v_{1}, v_{2}) for some v_{1}, v_{2} ∈ ℕ^{0}. We will show that the attacker can force the defender to reach a pair of configurations

\overline{\{m\}_{n}}.B_{K} || P and \overline{\{m\}_{n}}.B_{K} || Q

for some m ∈ M(T, {+_{i}, −_{i} | 1 ≤ i ≤ 2}) such that #_{+_{i}}(m) − #_{−_{i}}(m) = v_{i} for 1 ≤ i ≤ 2. From this pair of configurations the attacker wins because

\overline{\{m\}_{n}}.B_{K} || P ⟶ B_{K} || \overline{\{m\}_{n}}.P

whereas \overline{\{m\}_{n}}.B_{K} || Q −̸→.

In order to show that the attacker can force the defender to faithfully simulate the computation of the Minsky machine, we assume that the current configuration of R is (p, v_{1}, v_{2}) where 1 ≤ p < n and that the bisimulation game starts from the pair

\overline{\{m\}_{p}}.B_{K} || P and \overline{\{m\}_{p}}.B_{K} || Q

such that #_{+_{i}}(m)−#_{−_{i}}(m) = v_{i} for 1 ≤ i ≤ 2. We will show that if (p, v_{1}, v_{2}) ⟶ (p′, v′_{1}, v′_{2}) then after two rounds of the bisimulation game the attacker can force the defender to reach a pair of configurations \overline{\{m′\}_{p′}}.B_{K} || P and \overline{\{m′\}_{p′}}.B_{K} || Q such that #_{+_{i}}(m′) − #_{−_{i}}(m′) = v′_{i} for 1 ≤ i ≤ 2. There are three situations to be discussed.

(1) If the instruction I_{p} is of the form

p : c_{i} := c_{i} + 1; goto q

then the attacker makes two moves

\overline{\{m\}_{p}}.B_{K} || P ⟶ B_{K} || \overline{\{\{m\}_{+_{i}}\}_{q}}.P ⟶ \overline{\{\{m\}_{+_{i}}\}_{q}}.B_{K} || P

and the defender can only answer by

\overline{\{m\}_{p}}.B_{K} || Q ⟶ B_{K} || \overline{\{\{m\}_{+_{i}}\}_{q}}.Q ⟶ \overline{\{\{m\}_{+_{i}}\}_{q}}.B_{K} || Q.

(2) If the instruction I_{p} is of the form

          p : if c_{i} = 0 then goto q else c_{i} := c_{i} − 1; goto r

and v_{i} = 0 then the attacker plays

\overline{\{m\}_{p}}.B_{K} || P ⟶ B_{K} || \overline{\{m\}_{q_{=0}^{i}}}.P ⟶ \overline{\{m\}_{q}}.B_{K} || P.

This time the defender has six choices how to respond to the first move of the attacker. However, notice that

kn(B_{K} || \overline{\{m\}_{q_{=0}^{i}}}.P) = OK_{=0}

because v_{i} = 0 and hence the defender can only answer by

\overline{\{m\}_{p}}.B_{K} || Q ⟶ B_{K} || \overline{\{m\}_{q_{=0}^{i}}}.Q ⟶ \overline{\{m\}_{q}}.B_{K} || Q.

In all other possible moves the defender loses after the first move because the knowledge function returns different values.

(3) If the instruction I_{p} is of the form

          p : if c_{i} = 0 then goto q else c_{i} := c_{i} − 1; goto r

and v_{i} > 0 then the attacker plays

\overline{\{m\}_{p}}.B_{K} || P ⟶ B_{K} || \overline{\{\{m\}_{−_{i}}\}_{r_{≥0}^{i}}}.P ⟶ \overline{\{\{m\}_{−_{i}}\}_{r}}.B_{K} || P.

Again, because

kn(B_{K} || \overline{\{\{m\}_{−_{i}}\}_{r_{≥0}^{i}}}.P) = OK_{≥0}

the defender can only answer by

\overline{\{m\}_{p}}.B_{K} || Q ⟶ B_{K} || \overline{\{\{m\}_{−_{i}}\}_{r_{≥0}^{i}}}.Q ⟶ \overline{\{\{m\}_{−_{i}}\}_{r}}.B_{K} || Q.
⊓ ⊔

Lemma 2. If R diverges then the defender has a winning strategy in the bisimulation game played from the pair \overline{\{t\}_{1}}.B_{K} || P and \overline{\{t\}_{1}}.B_{K} || Q.

Proof. We will show that the defender in the bisimulation game from \overline{\{t\}_{1}}.B_{K} || P and \overline{\{t\}_{1}}.B_{K} || Q can force the attacker to faithfully simulate the computation of the Minsky machine. Since the computation of R diverges, the bisimulation game is infinite and the defender wins.

Consider a configuration (p, v_{1}, v_{2}) where 1 ≤ p < n of the machine R that was reached during the computation from (1, 0, 0). Let the corresponding pair of protocol configurations be

\overline{\{m\}_{p}}.B_{K} || P and \overline{\{m\}_{p}}.B_{K} || Q

such that #_{+_{i}}(m) − #_{−_{i}}(m) = v_{i} for 1 ≤ i ≤ 2.

We will show that if (p, v_{1}, v_{2}) ⟶ (p′, v′_{1}, v′_{2}) then after two rounds of the bisimulation game the defender can force the attacker to reach a pair of configurations \overline{\{m′\}_{p′}}.B_{K} || P and \overline{\{m′\}_{p′}}.B_{K} || Q such that #_{+_{i}}(m′) − #_{−_{i}}(m′) = v′_{i} for 1 ≤ i ≤ 2, or the defender can win by reaching a pair of syntactically equal (and hence bisimilar) configurations. There are three situations to be discussed.

(1) If the instruction I_{p} is of the form

p : c_{i} := c_{i} + 1; goto q

then there is only one possible continuation of the bisimulation game such that after two rounds the players reach the pair

\overline{\{\{m\}_{+_{i}}\}_{q}}.B_{K} || P and \overline{\{\{m\}_{+_{i}}\}_{q}}.B_{K} || Q.

(2) If the instruction I_{p} is of the form

       p : if c_{i} = 0 then goto q else c_{i} := c_{i} − 1; goto r

and v_{i} = 0, the attacker is forced to make either the move \overline{\{m\}_{p}}.B_{K} || P ⟶ B_{K} || \overline{\{m\}_{q_{=0}^{i}}}.P or \overline{\{m\}_{p}}.B_{K} || Q ⟶ B_{K} || \overline{\{m\}_{q_{=0}^{i}}}.Q and the game faithfully simulates the computation of R as before. In all other attacker’s moves the defender wins:

– if the attacker takes any of the four transitions (either from P or Q) introducing the key of the form p^{cheat} as the upper most encryption, the defender simply mimics the corresponding move in the other configuration except for the fact that he may switch P for Q or vice versa in order to achieve a pair of syntactically equal configurations (the knowledge function will return CHEAT in these situations);

– if the attacker takes a transition that should decrement a value of the counter c_{i} but the counter is already empty, i.e.,

\overline{\{m\}_{p}}.B_{K} || P ⟶ B_{K} || \overline{\{\{m\}_{−_{i}}\}_{r_{≥0}^{i}}}.P or
\overline{\{m\}_{p}}.B_{K} || Q ⟶ B_{K} || \overline{\{\{m\}_{−_{i}}\}_{r_{≥0}^{i}}}.Q,

the defender answers by the transitions

\overline{\{m\}_{p}}.B_{K} || Q ⟶ B_{K} || \overline{\{\{m\}_{−_{i}}\}_{r^{cheat}}}.P resp.
\overline{\{m\}_{p}}.B_{K} || P ⟶ B_{K} || \overline{\{\{m\}_{−_{i}}\}_{r^{cheat}}}.Q.

Since the attacker “cheated” the knowledge function allows this response (it returns the value CHEAT for these configurations). After the second round (there is only one possible continuation of the game which transfers the encrypted messages to the buffer), the protocol configurations become syntactically equal and hence the attacker loses.

(3) If the instruction I_{p} is of the form

       p : if c_{i} = 0 then goto q else c_{i} := c_{i} − 1; goto r

and v_{i} > 0, the situation is similar to the previous case. ⊓ ⊔ Theorem 4. The problem of bisimilarity checking between a pair of ping-pong protocol configurations of width 2 is undecidable (provided that we allow for general but still computable, respecting and finite-domain knowledge functions).

Proof. From Lemma 1 and Lemma 2. ⊓ ⊔

Theorem 5. The problem of bisimilarity checking between a pair of ping-pong protocol configurations of width 2 is decidable for local knowledge functions.

Proof. We shall reduce our problem to strong bisimilarity checking of PDA. The result then follows from the fact that strong bisimilarity of PDA is decidable [17].

In the reduction we extend the construction provided in the proof of Theorem 3. We consider not only the PDA rules

(P, Q)⟨v_{i}⟩ ⟶^{a} (Q, P_{i})⟨w_{i}⟩

for every P ∈ Const and Q ∈ Const ∪ \{0\} such that P =^{def} ∑_{i∈I} v_{i}.\overline{w_{i}}.P_{i} but also the rules

(P, Q)⟨w′⟩ ⟶^{f(P,Q,w′)} (P, Q)⟨w′⟩

for all elements (P, Q, w′) in the co-domain of the function f. Hence the reduction steps in the ping-pong protocol correspond to the a-labelled transitions in the PDA system, and the condition that the knowledge function agrees on bisimilar states is tested in the PDA by executing loops labelled by the elements from D. It is now easy to see that protocol configurations P_{1} || \overline{w_{1}}.Q_{1} and P_{2} || \overline{w_{2}}.Q_{2} are bisimilar if and only if the PDA configurations (P_{1}, Q_{1})⟨w_{1}⟩ and (P_{2}, Q_{2})⟨w_{2}⟩ are strongly bisimilar. ⊓ ⊔

Remark 4. By standard techniques for pushdown automata one can extend the previous theorem to allow a slightly more general definition of local knowledge functions. In particular, the functions kn can depend also on a constant number of inner-most keys of the encrypted message in addition to the M outer-most keys.

Recent BRICS Report Series Publications

RS-03-47 Hans Hüttel and Jiří Srba. Recursive Ping-Pong Protocols. December 2003. 21 pp. To appear in the proceedings of 2004 IFIP WG 1.7, ACM SIGPLAN and GI FoMSESS Workshop on Issues in the Theory of Security (WITS’04).

RS-03-46 Philipp Gerhardy. The Role of Quantifier Alternations in Cut Elimination. December 2003. 10 pp. Extends paper appearing in Baaz and Makowsky, editors, European Association for Computer Science Logic: 17th International Workshop, CSL ’03 Proceedings, LNCS 2803, 2003, pages 212-225.

RS-03-45 Peter Bro Miltersen, Jaikumar Radhakrishnan, and Ingo Wegener. On converting CNF to DNF. December 2003. 11 pp. A preliminary version appeared in Rovan and Vojtás, editors, Mathematical Foundations of Computer Science: 28th International Symposium, MFCS ’03 Proceedings, LNCS 2747, 2003, pages 612–621.

RS-03-44 Anna Gál and Peter Bro Miltersen. The Cell Probe Complexity of Succinct Data Structures. December 2003. 17 pp. An early version of this paper appeared in Baeten, Lenstra, Parrow and Woeginger, editors, 30th International Colloquium on Automata, Languages, and Programming, ICALP ’03 Proceedings, LNCS 2719, 2003, pages 332–344.

RS-03-43 Mikkel Nygaard and Glynn Winskel. Domain Theory for Concurrency. December 2003. 45 pp. To appear in a Theoretical Computer Science special issue on Domain Theory.

RS-03-42 Mikkel Nygaard and Glynn Winskel. Full Abstraction for HO-PLA. December 2003. 25 pp. Appears in Amadio and Lugiez, editors, Concurrency Theory: 14th International Conference, CONCUR ’03 Proceedings, LNCS 2761, 2003, pages 383–398.

RS-03-41 Malgorzata Biernacka, Dariusz Biernacki, and Olivier Danvy. An Operational Foundation for Delimited Continuations. December 2003. 21 pp.

RS-03-40 Andrzej Filinski and Henning Korsholm Rohde. A Denotational Account of Untyped Normalization by Evaluation. December 2003. 29 pp.