BRICS

Basic Research in Computer Science

Recursion vs. Replication in Simple Cryptographic Protocols

Hans Hüttel Jiří Srba BRICS Report Series RS-04-23 ISSN 0909-0878 October 2004 BRICS RS-04-23 Hüttel & Srba: Recursion vs. Replication in Simple Cryptographic Protocols Copyright \begin{matrix}c \\ ◯ \end{matrix} 2004, 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/04/23/

Recursion vs. Replication in Simple Cryptographic Protocols

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

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

Abstract. We use some recent techniques from process algebra to draw several conclusions about the well studied class of ping-pong protocols introduced by Dolev and Yao. In particular we show that all nontrivial properties, including reachability and equivalence checking wrt. the whole van Glabbeek’s spectrum, become undecidable for a very simple recursive extension of the protocol. The result holds even if no nondeterministic choice operator is allowed. We also show that the extended calculus is capable of an implicit description of the active intruder, including full analysis and synthesis of messages in the sense of Amadio, Lugiez and Vanackère. We conclude by showing that reachability analysis for a replicative variant of the protocol becomes decidable.

1 Introduction

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 notions of observational equivalence (like maytesting). Alternatively, security questions have been studied using reachability analysis [3, 5, 11].

We provide a basic study of expressiveness and feasibility of cryptographic protocols. We are interested in two verification approaches: reachability analysis and equivalence (preorder) checking. In reachability analysis the question is whether a certain (bad or good) configuration of the protocol is reachable from a given initial one. In equivalence checking the question is whether a protocol implementation is equivalent (e.g. bisimilar) to a given specification (optimal behaviour). These verification strategies can be used even in the presence of an active intruder (in the Dolev-Yao style), i.e., an agent with capabilities to listen to any communication, to perform analysis and synthesis of communicated messages according to the actual knowledge of compromised keys, and to actively

⋆ hans@cs.auc.dk ⋆⋆ srba@cs.auc.dk, the author is supported in part by the GACR, grant No.

201/03/1161.

⋆ ⋆ ⋆

Basic Research in Computer Science,

Centre of the Danish National Research Foundation.

participate in the protocol behaviour by transmitting new messages. This can be naturally implemented not only into the reachability analysis (see e.g. [4]) but also into the equivalence checking approach. As described in [12], these questions for equivalence (preorder) checking approach can be formulated as follows: “a protocol P guarantees a security property X if, whatever hostile environment E with a certain initial knowledge ϕ_{I}, then P is equivalent (in preorder) to (with) the specification α(P).” Formally this is given by saying that

protocol P satisfies property X iff ∀E ∈ E : P ∥ E ≈ α(P).  (1)

By an appropriate choice of the specification function α and a suitable equivalence (preorder) ≈, several security properties can be verified. Here is a small selection:

– Secrecy (confidential information should be available only to the partners of the communication). Here ≈ stands for trace preorder.

– (Message) authenticity (identification of other agents (messages) participating in communication ). Here ≈ stands for trace equivalence or preorder.

– Fairness (in a contract, no party can gain advantage by ending the protocol prematurely). Here ≈ stands for failure equivalence.

Various notions of bisimilarity are studied in this context as bisimilarity is usually the “most decidable behavioral equivalence” as confirmed e.g. by several positive decidability results in process algebra [6]. Hence the questions whether a certain class of cryptographic protocols has decidable reachability and equivalence (bisimilarity) checking are of particular importance for automated verification.

A number of security properties are decidable for finite protocols [3, 19]. In the case of an unbounded number of protocol configurations, the picture is more complex. Durgin et al. showed in [10] that security properties are undecidable in a restricted class of so-called bounded protocols (that still allows for infinitely many reachable configurations). In [2] 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 [4] that the reachability problem is in PTIME for a class of protocols with iteration.

In this paper we focus solely on ping-pong based behaviours of recursive and replicative protocols (perhaps the simplest behaviour of all studied calculi) in order to draw general conclusions about expressiveness and tractability of formal verification of cryptographic protocols. The class of ping-pong protocols was introduced in 1983 by Dolev and Yao [9]. The formalism deals with 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 [8]. The class of protocols studied in [4] contains iterative ping-pong protocols and, as a consequence, secrecy properties remain polynomially decidable even in this case.

In the present paper we continue our study of recursive and replicative extensions of ping-pong protocols. In [14] we showed that the recursive extension of the calculus is Turing powerful, however, the nondeterministic choice operator appeared to be essential in the construction. The question whether the calculus is Turing powerful even without any explicit way to define nondeterministic processes was left open. Here we present a radically new reduction from multi-stack automata and strengthen the undecidability results to hold even for protocols without nondeterministic choice. We prove, in particular, that both reachability and equivalence checking for all equivalences and preorders between trace equivalence/preorder and isomorphism of labelled transition systems (which includes all equivalences and preorders from van Glabbeek’s spectrum [20]) become undecidable. These results are of general importance because they prove the impossibility of automated verification for essentially all recursive cryptographic protocols capable of at least the ping-pong behaviour.

In the initial study from [14], the question of active attacks on the protocol was not dealt with. We shall demonstrate that a complete notion of the active intruder (including analysis and synthesis of messages in the sense of Amadio, Lugiez and Vanackère [4]) can be explicitly encoded into our formalism in order to analyze general properties like in the scheme (1).

Finally, we study a replicative variant of the calculus. Surprisingly, such a calculus becomes decidable, at least with regard to reachability analysis. We use a very recent result from process algebra (decidability of reachability for weak process rewrite systems by Křetínský, Řehák and Strejček [15]) in order to derive the result. We believe that this is one of the reasons which formally confirm the general trend that replication is a good choice for cryptographic formalisms and that is why recursion is only rarely studied.

2 Basic definitions

2.1 Labelled transition systems with label abstraction

In order to provide a uniform framework for our study of ping-pong protocols, we define their semantics by means of labelled transition systems. A labelled transition system (LTS) is a triple T = (S, Act, ⟶) where S is a set of states (or processes), Act is a set of labels (or actions), and ⟶⊆ S × Act × S is a transition relation, written α ⟶^{a} β, for (α, a, β) ∈⟶. As usual we extend the transition relation to the elements of Act^{∗}. We also write α ⟶^{∗} β, whenever α ⟶^{w} β for some w ∈ Act^{∗}.

The idea is that the states represent global configurations of a given protocol and the transitions describe the information flow. Labels on the transitions moreover represent the messages (both plain-text and cipher-text) which are being communicated during the state changes.

Remark 1. In [14] the semantics of ping-pong protocols is given in terms of transition systems with knowledge, i.e., unlabelled transition systems where each state it assigned its knowledge, represented as a subset of a certain set of all possible knowledge values. By standard techniques such a knowledge-based semantics can be translated to labelled transition systems and the studied verification properties (reachability, equivalence checking, etc.) are preserved. For example a state A with two knowledge values p_{1} and p_{2} can be transformed to a labelled transition system where the values p_{1} and p_{1} are represented as self-loops in state A which are visible under special actions p_{1} and p_{2}. A fresh action a is used to represent the change of the state (the unlabelled transitions in the original knowledge-based semantics).

The explicit possibility to observe the full content of messages is sometimes not very realistic; it means that an external observer of such a system can e.g. distinguish between two different messages encrypted by the same encryption key, without the actual knowledge of the key.

In order to restrict capabilities of the observer we introduce a so called label abstraction function ϕ : Act ↦ Act. Given a LTS T = (S, Act, ⟶_{T}) and a label abstraction function ϕ we define a new LTS T_{ϕ} =^{def} (S, Act, ⟶_{T_{ϕ}}) where

α ⟶^{ϕ(a)}_{T_{ϕ}} β iff α ⟶^{a}_{T} β for all α, β ∈ S and a ∈ Act. We call T_{ϕ} a labelled transition system with label abstraction.

Let us now focus on the messages (actions). Assume a given set of encryption keys K. The set of all messages over K is given by the following abstract syntax

m ::= k | k · m

where k ranges over K. Hence every element of the set K is a (plain-text) message and if m is a message then k · m is a (cipher-text) message (meaning that the message m is encrypted by the key k). Given a message k_{1} · k_{2} ⋯ k_{n} over K we usually^{1} write it only as a word k_{1}k_{2} ⋯ k_{n} from K^{∗}. Note that k_{n} is the plaintext part of the message and the outermost encryption key is always on the left (k_{1} in our case). In what follows we shall identify the set of messages and K^{∗}, and we denote the extra element of K^{∗} consisting of the empty sequence of keys by ϵ.

Example 1. Let us consider a labelled transition system T =^{def} (S, Act, ⟶) where S =^{def} {A, B, C}, Act =^{def} K^{∗} for a given set of keys K = {k_{1}, k_{2}, λ} and ⟶ is given by the following picture.

\xymatrix{A \ar[r]^{k_{1}k_{2}} & B \ar[r]^{k_{2}} & C}

The protocol computation starts in the state A and is very simple. First a plaintext k_{2} encrypted by the encryption key k_{1} is communicated to the process B, which decrypts the message and sends out the plain-text k_{2}. Let us now assume a label abstraction function ϕ defined by ϕ(k) = k if k ∈ K and ϕ(m) = λ

1 In our previous work on ping-pong protocols [14] we denoted a message m encrypted by a key k as {m}_{k}. We changed the notation in order to improve the clarity of the proofs. In particular, when messages like k_{1}k_{2} ⋯ k_{n} are used, the previous syntax described the keys in a reversed order, which was technically inconvenient.

otherwise. The labelled transition system T_{ϕ} with label abstraction function ϕ now looks as follows.

\xymatrix{A \ar[r]^{λ} & B \ar[r]^{k_{2}} & C}

This translates to the fact that the external observer is not allowed to see the content of encrypted messages (the action λ is used instead) and only plain-text messages can be recognized. ⊓ ⊔

The level of abstraction we may select depends on the particular studied property we are interested in and it directly corresponds to the specification function α from (1). Nevertheless, it seems reasonable to require at least the possibility to distinguish between plain-text and cipher-text messages. We say that a label abstraction function ϕ is reasonable iff ϕ(k) ≠ ϕ(k′w) for all k, k′ ∈ K and w ∈ K^{+}.

2.2 A calculus of recursive ping-pong protocols

We shall now define a calculus which captures exactly the class of ping-pong protocols by Dolev and Yao [9] extended (in a straightforward manner) with recursive definitions.

Let K be a set of encryption keys. A specification of a recursive ping-pong is a finite set of process definitions Δ such that for every process constant P (from a given set Const) the set Δ contains exactly one process definition of the form

P =^{def} ∑_{i_{1}∈I_{1}} v_{i_{1}} ▷ . \overline{w_{i_{1}}▷}.P_{i_{1}} + ∑_{i_{2}∈I_{2}} v_{i_{2}}.P_{i_{2}} + ∑_{i_{3}∈I_{3}} \overline{w_{i_{3}}}.P_{i_{3}}

where I_{1}, I_{2} and I_{3} are finite sets of indices such that I_{1} ∪ I_{2} ∪ I_{3} ≠ ∅, and v_{i_{1}}, v_{i_{2}}, w_{i_{1}} and w_{i_{3}} are messages (belong to K^{∗}) for all i_{1} ∈ I_{1}, i_{2} ∈ I_{2} and i_{3} ∈ I_{3}, and P_{i} ∈ Const ∪ {0} for all i ∈ I_{1} ∪ I_{2} ∪ I_{3} such that 0 is a special constant called the empty process. We moreover require that v_{i_{2}} and w_{i_{3}} for all i_{2} ∈ I_{2} and i_{3} ∈ I_{3} are different from the empty message ϵ. (Observe that any specification Δ contains only finitely many keys.)

Summands continuing in the empty process constant 0 will be written without the 0 symbol and process definitions will often be written in their unfolded form using the nondeterministic choice operator ‘+’. An example of a process

definition is e.g. P =^{def} k_{1}▷ . \overline{k_{2}▷}.P_{1} + k_{1}▷ . \overline{k_{3}▷} + k_{1}k_{2}.P_{1} + \overline{k_{1}k_{1}} + \overline{k_{1}k_{2}}.P_{2}.

The intuition is that each summand of the form v_{i_{1}} ▷ . \overline{w_{i_{1}}▷}.P_{i_{1}} can receive a message encrypted by a sequence v_{i_{1}} of outermost keys, decrypt the message using these keys, send it out encrypted by the sequence of keys w_{i_{1}}, and finally behave as the process constant P_{i_{1}}. The symbol ▷ stands for the rest of the message after decrypting it with the key sequence v_{i_{1}}. This describes a standard ping-pong behaviour of the process.

In addition to this we may have summands of the forms v_{i_{2}}.P_{i_{2}} and \overline{w_{i_{3}}}.P_{i_{3}}, meaning simply that a message is received and forgotten or unconditionally transmitted, respectively. This is a small addition to the calculus we presented in [14] in order to allow for discarding of old messages and generation of new messages. These two features were not available in the earlier version of the calculus but they appear to be technically convenient when modeling an explicit intruder and for strengthening the positive decidability results in Section 5. Nevertheless, the undecidability results presented in Section 3 are valid even without this extension since only the standard ping-pong behaviour is used in the constructions. A feature very similar to the forgetful input operation can be also found in [4].

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

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

where 0 is the empty configuration, P ∈ Const ∪ {0} ranges over process constants including the empty process, w ∈ K^{∗} ranges over the set of messages, and ‘∥’ is the operator of parallel composition.

We introduce a structural congruence relation ≡ which identifies configurations that represent the same state of the protocol. The relation ≡ is defined as the least congruence over configurations (≡⊆ Conf × Conf) such that (Conf, ∥, 0) is a commutative monoid and \overline{ϵ}.P ≡ P for all P ∈ Const. In what follows we shall identify configurations up to structural congruence.

Remark 2. We let \overline{ϵ}.P ≡ P because the empty message should never be communicated. This means that when a prefix like k ▷ . \overline{▷}.P receives a plain-text message k and tries to output \overline{ϵ}.P, it simply continues as the process P.

We shall now define the semantics of ping-pong protocols in terms of labelled transition systems. We define a set Conf_{S} ⊆ Conf consisting of all configurations that do not contain the operator of parallel composition and call these simple configurations. We also define two sets In(C, m), Out(C, m) ⊆ Conf_{S} for all C ∈ Conf_{S} and m ∈ K^{+}. The intuition is that In(C, m) (Out(C, m)) contains all configurations which can be reached from the simple configuration C after receiving (resp. outputting) the message m from (to) the environment. Formally, In(C, m) and Out(C, m) are the smallest sets which satisfy:

– Q ∈ In(P, m) whenever P ∈ Const and m.Q is a summand of P

– \overline{wα}.Q ∈ In(P, m) whenever P ∈ Const and v▷ . \overline{w▷}.Q is a summand of P such that m = vα

– P ∈ Out(\overline{m}.P, m) whenever P ∈ Const ∪ \{0\}

– Q ∈ Out(P, m) whenever P ∈ Const and \overline{m}.Q is a summand of P.

A given protocol specification Δ determines a labelled transition system T (Δ) =^{def} (S, Act, ⟶) where the states are configurations of the protocol modulo the structural congruence (S =^{def} Conf/ ≡), the set of labels (actions) is the set of messages that can be communicated between the agents of the protocol (Act =^{def} K^{+}), and the transition relation ⟶ is given by the following SOS rule (recall that ‘∥’ is commutative).

\frac{m ∈ K^{+} C_{1}, C_{2} ∈ Conf_{S} C′_{1} ∈ Out(C_{1}, m) C′_{2} ∈ In(C_{2}, m)}{C_{1} ∥ C_{2} ∥ C ⟶^{m} C′_{1} ∥ C′_{2} ∥ C}

This means that (in the context C) two simple configurations (agents) C_{1} and C_{2} can communicate a message m in such a way that C_{1} outputs m and becomes C′_{1} while C_{2} receives the message m and becomes C′_{2}.

Example 2. Let us consider a protocol specification Δ.

P =^{def} \overline{k}.P ∥ k▷ . \overline{kk▷}.P ∥ k.Q Q =^{def} k.P

A fragment of the labelled transition system reachable from the initial configuration P ∥ P looks as follows.

\xymatrix{P ∥ P \ar[r]^{k} \ar[d]_{k} & P ∥ \overline{kk}.P \ar[r]^{kk} & P ∥ \overline{kkk}.P \ar[r]^{kkk} & … \\ P ∥ Q \ar[u]_{k}}

⊓ ⊔

For further discussion and examples of recursive ping-pong protocols we refer the reader to [14].

2.3 Reachability and behavioural equivalences

One of the problems that is usually studied is that of reachability analysis: given two configurations C_{1}, C_{2} ∈ Conf we ask whether C_{2} is reachable from C_{1}, i.e., if C_{1} ⟶^{∗} C_{2}. In this case the set of labels is irrelevant.

As the semantics of our calculus is given in terms of labelled transition systems (together with an appropriate label abstraction function), we can also study the equivalence checking problems. Given some behavioural equivalence or preorder ↔ from van Glabbeek’s spectrum [20] (e.g. strong bisimilarity or trace, failure and simulation equivalences/preorders just to mention a few) and two configurations C_{1}, C_{2} ∈ Conf of a protocol specification Δ, the question is to decide whether C_{1} and C_{2} are ↔-equivalent (or ↔-preorder related) in T (Δ), i.e., whether C_{1} ↔ C_{2}.

3 Recursive ping-pong protocols without explicit choice

In this section we strengthen the undecidability result from [14] and show that the reachability and equivalence checking problems are undecidable for pingpong protocols without an explicit operator of nondeterminism and using classical ping-pong behaviour only, i.e., for protocols without any occurrence of the choice operator ‘+’ and where every defining equation is of the form P =^{def} v▷ . \overline{w▷}.P′ such that P′ ∈ Const.

Remark 3. Note that every process constant is allowed to have exactly one defining equation, however, no constraints are imposed on the communication behaviour of the parallel components.

We moreover show that the negative results apply to all behavioural equivalences and preorders between trace equivalence/preorder and isomorphism of LTS (which preserves labelling) with regard to all reasonable label abstraction functions as defined in Section 2.

These results are achieved by showing that recursive ping-pong protocols can step-by-step simulate a Turing powerful computational device, in our case a computational model called multi-stack machines.

A multi-stack machine R with ℓ stacks (ℓ ≥ 1) is a triple R = (Q, Γ, ⟶) where Q is a finite set of control-states, Γ is a finite stack alphabet such that Q ∩ Γ = ∅, and ⟶⊆ Q × Γ × Q × Γ^{∗} is a finite set of transition rules, written pX ⟶ qα for (p, X, q, α) ∈⟶.

A configuration of a multi-stack machine R is an element from Q×(Γ^{∗})^{ℓ}. We assume a given initial configuration (q_{0}, w_{1}, …, w_{ℓ}) where q_{0} ∈ Q and w_{i} ∈ Γ^{∗} for all i, 1 ≤ i ≤ ℓ. If some of the stacks w_{i} are empty, we denote them by ϵ.

A computational step is defined such that whenever there is a transition rule pX ⟶ qα then a configuration which is in the control-state p and has X on top of the i’th stack (the tops of the stacks are on the left) can perform the following transition:

(p, w_{1}, …, Xw_{i}, …, w_{ℓ}) ⟶ (q, w_{1}, …, αw_{i}, …, w_{ℓ})

for all w_{1}, …, w_{ℓ} ∈ Γ^{∗} and for all i, 1 ≤ i ≤ ℓ.

It is a folklore result that multi-stack machines are Turing powerful. Hence (in particular) the following problem is easily seen to be undecidable: given an initial configuration (q_{0}, w_{1}, …, w_{ℓ}) of a multi-stack machine R, can we reach the configuration (h, ϵ, …, ϵ) for a distinguished halting control-state h ∈ Q such that all stacks are empty? Without loss of generality we can even assume that a configuration in the control-state h is reachable iff all stacks are empty.

Let R = (Q, Γ, ⟶) be a multi-stack machine. We define the following set of keys of a ping-pong specification Δ: K =^{def} Q ∪ Γ ∪ {k_{p} | p ∈ Q} ∪ {t, k_{∗}}. Here t is a special key such that every communicated message is an encryption of the plain-text key t. The reason for this is that it ensures that the protocol never communicates any plain-text message. The key k_{∗} is a special purpose locking key and it is explained later on in the construction.

We shall construct a ping-pong protocol specification Δ as follows.

– For every transition rule pX ⟶ qα we have a process constant P_{pX⟶qα} with the following defining equation.

P_{pX⟶qα} =^{def} pX ▷ . \overline{k_{q}α▷}.P_{pX⟶qα}

– For every state p ∈ Q we have two process constants T_{p} and T′_{p}.

T_{p} =^{def} k_{p}▷ . \overline{k_{∗}▷}.T′_{p}

T′_{p} =^{def} k_{∗}▷ . \overline{p▷}.T_{p} if p ∈ Q ∖ \{h\}, and T′_{h} =^{def} h▷ . \overline{h▷}.T′_{h}

Recall that h ∈ Q is the halting control-state.

– Finally, we define a process constant B (standing for a buffer over a fixed

key k_{∗}).

B =^{def} k_{∗}▷ . \overline{k_{∗}▷}.B

In this defining equation the key k_{∗} locks the content of the buffer such that it is accessible only by some T′_{p}.

Note that Δ does not contain any choice operator ‘+’ as required.

Let (q_{0}, w_{1}, …, w_{ℓ}) be an initial configuration of the multi-stack machine R. The corresponding initial configuration of the protocol Δ is defined as follows (the meta-symbol Π stands for a parallel composition of the appropriate components).

( ∏_{(r,A,s,β)∈⟶} P_{rA⟶sβ}) ∥ ( ∏_{p∈Q∖\{q_{0}\}}T_{p}) ∥ T′_{q_{0}} ∥ ( ∏_{j∈\{1,...,ℓ\}} \overline{k_{∗}w_{j}t}.B) (2)

The following invariants will be preserved during any computational sequence starting from this initial configuration:

– at most one T′_{p} for some p ∈ Q is present as a parallel component (the intuition is that this represents the fact that the machine R is in the controlstate p), and

– plain-text messages are never communicated.

Let (p, w_{1}, …, w_{i}, … w_{ℓ}) ⟶ (q, w_{1}, …, αw′_{i}, … w_{ℓ}) be a computational step of R using the rule pX ⟶ qα such that w_{i} = Xw′_{i}. This one step is simulated by a sequence of four transitions in the ping-pong protocol Δ (see Figure 3). In the first step one buffer is selected and unlocked (the current control-state p replaces the locking key k_{∗} in the outermost encryption). In particular the buffer \overline{k_{∗}w_{i}t}.B can be unlocked. No other kinds of transitions are possible in the first step. Opening of the selected buffer means that some of the process constants P_{rA⟶sβ} become able to accept this message. In particular the process constant P_{pX⟶qα} can receive the message and output \overline{k_{q}αw_{i}t} for further communication; the key k_{q} determines the control-state change. (At this stage also a communication between \overline{k_{∗}w_{i}t}.B and B is enabled but it does not change the current state and hence it cannot contribute to a computational progress.) In the next step only T_{q} can receive the message \overline{k_{q}αw_{i}t}, it remembers the new control-state q by becoming T′_{q} and offers the k_{∗}-locked message for a communication with B. This last communication (when B receives back the modified buffer) ends a simulation of one computational step of R.

The following property is easy to see: if after some number of steps starting in a protocol configuration corresponding to (p, w_{1}, …, w_{ℓ}) we reach a first protocol configuration where T′_{q} appears for some q ∈ Q then this corresponds to one correct computational step in R. On the other hand, the computation of Δ can

( ∏_{(r,A,s,β)∈⟶} P_{rA⟶sβ}) ∥ ( ∏_{r∈Q∖\{p\}} T_{r}) ∥ T′_{p} ∥ ( ∏_{j∈\{1,...,ℓ\}} \overline{k_{∗}w_{j}t}.B)

↓ k_{∗}w_{i}t

( ∏_{(r,A,s,β)∈⟶} P_{rA⟶sβ}) ∥ ( ∏_{r∈Q∖\{p\}} T_{r}) ∥ \overline{pw_{i}t}.T_{p} ∥

( ∏_{j∈\{1,...,ℓ\},j≠i} \overline{k_{∗}w_{j}t}.B) ∥ B

↓ pw_{i}t

( ∏_{(r,A,s,β)∈(⟶∖\{(p,X,q,α)\})} P_{rA⟶sβ}) ∥ \overline{k_{q}αw′_{i}t}.P_{pX⟶qα} ∥ ( ∏_{r∈Q} T_{r}) ∥

( ∏_{j∈\{1,...,ℓ\},j≠i} \overline{k_{∗}w_{j}t}.B) ∥ B

↓ k_{q}αw′_{i}t

( ∏_{(r,A,s,β)∈⟶} P_{rA⟶sβ}) ∥ ( ∏_{r∈Q∖\{q\}} T_{r}) ∥ \overline{k_{∗}αw′_{i}t}.T′_{q} ∥

( ∏_{j∈\{1,...,ℓ\},j≠i} \overline{k_{∗}w_{j}t}.B) ∥ B

↓ k_{∗}αw′_{i}t

( ∏_{(r,A,s,β)∈⟶} P_{rA⟶sβ}) ∥ ( ∏_{r∈Q∖{q}} T_{r}) ∥ T′_{q} ∥

( ∏_{j∈\{1,...,ℓ\},j≠i} \overline{k_{∗}w_{j}t}.B) ∥ \overline{k_{∗}αw′_{i}t}.B

Fig. 1. Simulation of (p, w_{1}, …, w_{i}, … w_{ℓ}) ⟶ (q, w_{1}, …, w′_{i}α, … w_{ℓ}) s.t. w_{i} = Xw′_{i}

get stuck after the first communication step (in case that the unlocked buffer does not enable an application of any rule rA ⟶ sβ) or an infinite sequence of communication steps of the form \overline{m}.B ∥ B ⟶^{m} \overline{m}.B ∥ B is also possible.

This is formally captured in the following lemma.

Lemma 1. In the given multi-stack machine R the configuration (q, w′_{1}, …, w′_{ℓ}) is reachable from (p, w_{1}, …, w_{ℓ}) if and only if

( ∏_{(r,A,s,β)∈⟶} P_{rA⟶sβ}) ∥ ( ∏_{p∈Q∖\{q\}} T_{p}) ∥ T′_{q} ∥ ( ∏_{j∈\{1,...,ℓ\}} \overline{k_{∗}w′_{j}t}.B)

is reachable (in Δ) from

( ∏_{(r,A,s,β)∈⟶} P_{rA⟶sβ}) ∥ ( ∏_{p∈Q∖\{p\}} T_{p}) ∥ T′_{p} ∥ ( ∏_{j∈\{1,...,ℓ\}} \overline{k_{∗}w_{j}t}.B).

The following theorems are now easily derived.

Theorem 1. The reachability problem for recursive ping-pong protocols without an explicit choice operator is undecidable.

Proof. Immediately from Lemma 1 and from the undecidability of reachability for multi-stack machines. ⊓ ⊔

Theorem 2. The equivalence checking problem for recursive ping-pong protocols without an explicit choice operator is undecidable for any behavioral equivalence/preorder between trace equivalence/preorder and isomorphism (including all equivalences and preorders from van Glabbeek’s spectrum [20]) and for any reasonable label abstraction function.

Proof. Let R be a multi-stack machine and Δ the protocol specification constructed above with the initial configuration C as given by (2). We consider the question whether C ∥ \overline{h} is equivalent (or in preorder) with C.

In case that the halting control-state h is not reachable from the initial configuration of R, we know from Lemma 1 that T′_{h} will never appear as a parallel component in any reachable state from C. This implies that the plaintext message \overline{h} will never be communicated and hence C ∥ \overline{h} and C exhibit isomorphic behaviours under any label abstraction function.

On the other hand, if h is reachable from the initial configuration of R then because of Lemma 1 a configuration in Δ with the parallel component T′_{h} is reachable. Such a configuration is stuck in the process on the right, however, in the process on the left the plain-text message h can be communicated between T′_{h} and the extra parallel component \overline{h}. This means that C ∥ \overline{h} and C are not even related by the trace preorder (and hence they are also not trace equivalent) because after a finite sequence of communicated messages there is a successor of the configuration C ∥ \overline{h} which can communicate the plain-text h while (as argued before) C can only exchange cipher-text messages. As the label abstraction function ϕ is reasonable, necessarily for all messages m (cipher-texts) communicated in C it is the case that ϕ(m) ≠ ϕ(h).

To sum up, if the machine R cannot reach the halting configuration then C ∥ \overline{h} and C are isomorphic and if R halts than C ∥ \overline{h} and C are not in trace preorder. This implies that all equivalences and preorders between trace and isomorphism are undecidable for any reasonable label abstraction function. ⊓ ⊔

4 The active intruder

In the literature on applying process calculi to the study of cryptographic protocols, there have been several proposals for explicit modelling the active intruder (environment). Foccardi, Gorrieri and Martinelli in [12] express the environment within the process calculus, namely as a process running in parallel with the protocol. In [4] Amadio, Lugiez and Vanackère describe a tiny process calculus similar to ours, except that they use replication instead of recursion. Moreover, the environment is described in the semantics of the calculus. Transitions are of the form

(C, T) → (C′, T′)

where C and C′ are protocol configurations and T and T′ denote the sets of messages known to the environment (all communication occurs only by passing messages through these sets).

The environment is assumed to be hostile; it may compute new messages by means of the operations of analysis and synthesis and pass these on to the process. Let K be a set of encryption keys as before. The analysis of a set of messages T ⊆ K^{∗} is the least set A(T) satisfying

A(T) = T ∪ {w | kw ∈ A(T), k ∈ K ∩ A(T)}.  (3)

The synthesis of a set of messages T ⊆ K^{∗} is the least set S(T) satisfying

S(T) = A(T) ∪ {kw | w ∈ S(T), k ∈ K ∩ S(T)}.  (4)

The next lemmas follow immediately from Tarski’s fixed-point theorem.

Lemma 2. The analysis of a set of messages T ⊆ K^{∗} is the union of the family of sets A_{i}(S) defined by

A_{0}(T) = T
A_{i+1}(T) = A_{i}(T) ∪ {w | kw ∈ A_{i}(T), k ∈ K ∩ A_{i}(T)}

Lemma 3. The synthesis of a set of messages T ⊆ K^{∗} is the union of the family of sets S_{i}(T) defined by

S_{0}(T) = A(T)
S_{i+1}(T) = S_{i}(T) ∪ {kw | w ∈ S_{i}(T), k ∈ K ∩ S_{i}(T)}

The set of compromised keys K_{c} for a given set T ⊆ K^{∗} of messages is defined by K_{c} =^{def} K∩S(T), which is easily seen to be equal to K∩A(T). (The compromised keys are immediately available for the intruder because they are either in his initial knowledge or can be discovered by the analysis.)

Remark 4. Let T ⊆ K^{∗} be a given set of messages. The following observation is easy to verify: in order to compute the complete set K_{c} of compromised keys of size n, it is enough to find messages m_{1}, …, m_{n} ∈ T such that when we analyze them in a sequence, we discover exactly all compromised keys. Formally, we define

K_{c}^{0} =^{def} ∅ and K_{c}^{i} =^{def} K_{c}^{i−1} ∪ {k ∈ K | m_{i} = wk, w ∈ (K_{c}^{i−1})^{∗}}

for all i, 1 ≤ i ≤ n, and then K_{c} = K_{c}^{n}. ⊓ ⊔

Proposition 1. It holds that w ∈ S(T) if and only if w can be written as w = uw′ for some u ∈ K_{c}^{∗} and there exists u′ ∈ K_{c}^{∗} such that u′w′ ∈ T.

Proof. Notice that because of Lemma 2 w ∈ A(T) iff there is u ∈ K_{c}^{∗} such that uw ∈ T. The proposition then follows by an application of Lemma 3. ⊓ ⊔

We can now design an environment sensitive semantics for our calculus close in style to that of [4]. We define the reduction relation → by the following set of axioms (here x ∈ P means that x is a summand in the defining equation of the process constant P).

(P ∥ C, T) → (\overline{wα}.P′ ∥ C, T)  if (v▷ . \overline{w▷}.P′) ∈ P and vα ∈ S(T) (A1)
(P ∥ C, T) → (P′ ∥ C, T) if (v.P′) ∈ P and v ∈ S(T) (A2)
(\overline{w}.P ∥ C, T) → (P ∥ C, T ∪ \{w\})  (A3)
(P ∥ C, T) → (P′ ∥ C, T ∪ \{w\}) if (\overline{w}.P′) ∈ P  (A4)

We show that this semantics can be internalized in our calculus within our existing semantics.

4.1 Intruder implementation

Let Pr be an initial configuration of a given protocol Δ with its (finite) set of protocol keys K_{p}. Without loss of generality we may assume that Δ is inputguarded, meaning that it contains no input prefixes of the form ▷ (i.e., every input prefix is guarded by at least one encryption key; this is easily guaranteed by replacing every summand of the form ▷. \overline{w▷}.P_{i} with ∑_{k∈K_{p}} k ▷ . \overline{wk▷}.P_{i}, which can be easily seen to generate the same labelled transition system).

Given a protocol configuration Pr, we shall define the intruder as an extra parallel component in the configuration (and hence using the same syntax). The intruder will remember a set K_{c} ⊆ K_{p} of the compromised keys (as defined above) plus he will use an extra set of keys {ℓ_{P} , ℓ_{B}, ℓ_{T} } of so called locking keys and another key # called a separation key.

We implement the intruder as an abstract set of operations that can modify two main data structures, a pool and a buffer. Note that this is a conceptual abstraction: in fact the set of all data is represented as a single message containing the total sequence of keys of messages that have been encountered. For this the structure pool will store all available messages separated by the key #, and the buffer structure can be either empty or it can store a single message in order to enable its analysis and synthesis. Moreover (for technical reasons) all messages placed into the pool will be in the reversed order of encryption keys.

All communication between the intruder and the protocol Pr will pass through the buffer. The available operations are in Table 1. Note that all the corresponding process constants are parameterized by the set K_{c} of currently discovered compromised keys. The intuition is that listen can transfer any message offered by the protocol Pr and store it to the buffer. Similarly output can offer the content of the buffer for communication with the original protocol Pr. Deposit can transfer the message stored in buffer into the pool (the extra key # is used to separate the messages stored in the pool and the transfered message is stored into P in the reversed order). Retrieve can nondeterministically select a single message from the pool and copy it into the buffer. Analyze can provide an analysis of the current message in the buffer according to the set of compromised keys K_{c} (during this a new compromised key can be discovered and the set K_{c} is

Operation Direction  Process constant

Listen Protocol → Buffer L^{K_{c}} Output Buffer → Protocol O^{K_{c}} Deposit Buffer → Pool D^{K_{c}} Retrieve Pool → Buffer R^{K_{c}} Analyze Buffer → Buffer A^{K_{c}} Synthesize Buffer → Buffer S^{K_{c}}

Switch  no data operation  X^{K_{c}}

Table 1. Abstract operations of the intruder

updated accordingly). Synthesize can add an arbitrarily long sequence of compromised keys onto the message currently stored in the buffer. Finally, the switch process constant X^{K_{c}} allows for a nondeterministic selection of any one of the previously mentioned operations. In any configuration of the intruder, exactly one of the process constants from Table 1 is present as a parallel component.

All internal communication within the intruder uses one of the locking keys mentioned above as the outermost key in the communicated messages. Together with our assumption that the original protocol is input-guarded by the keys K_{p}, this guarantees that none of those messages are available for a communication with the protocol as they have to be unlocked first. Also observe that because the process constants from Table 1 are parameterized by K_{c} ⊆ K_{p}, we have exponentially many of them with respect to the size of the set K_{p}. This is for technical convenience only, and it is discussed in more detail in Conclusion.

Let us now define all the components of the intruder.

4.2 Buffer implementation

All operations of the intruder use their own private buffer. A buffer B_{ℓ} is a process which can temporarily store any message encrypted with the locking key ℓ.

B_{ℓ} =^{def} ℓ▷ . \overline{ℓ▷}.B_{ℓ}  (5)

The intruder uses three such buffers. We assign them the names P (pool), B (buffer) and B_{T} (temporary buffer) as follows.

P = B_{ℓ_{P}}  B = B_{ℓ_{B}}  B_{T} = B_{ℓ_{T}}

4.3 Initial configuration

The initial intruder with a given set of compromised keys K_{c} is described by the following configuration.

I_{init} = \overline{ℓ_{P} #}.P ∥ \overline{ℓ_{B}}.B ∥ \overline{ℓ_{T}} .B_{T} ∥ X^{K_{c}}  (6)

The prefix \overline{ℓ_{P} #} ensures that the empty message ϵ is available on the pool initially, and this will make it possible to output any compromised key k by using the synthesis operation on ϵ to obtain kϵ = k. The other two buffers are simply initialized to empty by transmitting only the corresponding locking key.

An intruder configuration is any configuration I such that I_{init}→^{∗}I. The behaviour of the intruder will be described in such a way that any intruder configuration will always be of the form

C_{P} ∥ C_{B} ∥ C_{B_{T}} ∥ C_{X}

where C_{P} is either P or \overline{ℓ_{P} w}.P for some w ∈ (K_{p} ∪ \{#\})^{∗}, C_{B} is either B or \overline{ℓ_{B}w}.B for some w ∈ K_{p}^{∗}, C_{B_{T}} is either B_{T} or \overline{ℓ_{T} w}.B_{T} for some w ∈ (K_{p}∪\{#\})^{∗}, and C_{X} is either Y or \overline{w}.Y where Y ∈ \{X^{K_{c}}, L^{K_{c}}, O^{K_{c}}, D^{K_{c}}, R^{K_{c}}, A^{K_{c}}, S^{K_{c}}\} and w ∈ K^{∗}.

As the original protocol is assumed to be input-guarded, in a configuration like Pr ∥ I (where Pr is a protocol configuration and I is an intruder configuration), we will make sure that only a process constant Y in the C_{X} part of I can manipulate the available buffers in parts C_{P}, C_{B} and C_{B_{T}}.

4.4 Switching between operations

The intruder is always capable of choosing nondeterministically between any of the six operations in Table 1. In this way, the intruder can manipulate messages by any means necessary. This is expressed by the central component of the intruder, the switch process constant X^{K_{c}}, which is parameterized by the set of currently compromised keys K_{c}.

X^{K_{c}} =^{def} ℓ_{B}.L^{K_{c}}  (7)
+ ℓ_{P} ▷ . \overline{ℓ_{P} ▷}.O^{K_{c}}  (8)
+ ℓ_{P} ▷ . \overline{ℓ_{P} ▷}.D^{K_{c}}  (9)
+ ℓ_{B}.R^{K_{c}}  (10)
+ ℓ_{P} ▷ . \overline{ℓ_{P} ▷}.A^{K_{c}}  (11)
+ ℓ_{P} ▷ . \overline{ℓ_{P} ▷}.S^{K_{c}}  (12)

As X^{K_{c}} is always in parallel with a pool of the form \overline{ℓ_{P} w}.P, the following

communication is possible \overline{ℓ_{P} w}.P ∥ X^{K_{c}} ⟶^{ℓ_{P} w} P ∥ \overline{ℓ_{P} w}.Y ⟶^{ℓ_{P} w} \overline{ℓ_{P} w}.P ∥ Y for

any Y ∈ {O^{K_{c}}, D^{K_{c}}, A^{K_{c}}, S^{K_{c}}}. This corresponds to giving a control to the appropriate process constant Y (the use of pool to make the switch is here only for technical reasons and the pool content is untouched). The process constants L^{K_{c}} and R^{K_{c}} use a different switching method which guarantees that the state change is possible only if the buffer B is empty (i.e., it outputs only the key ℓ_{B}).

4.5 Listen to the protocol

As the intruder runs in parallel with the protocol configuration Pr, it may collect any message transmitted by Pr. It then encrypts the message by the locking key ℓ_{B} and stores the message into the buffer B. The control is returned to X^{K_{c}} afterwards.

L^{K_{c}} =^{def} ∑_{k∈K_{p}} k▷ . \overline{ℓ_{B}k▷}.X^{K_{c}}  (13)

Formally, if m ∈ K_{p}^{∗} and Pr can transmit m and become Pr′, we can perform the following communication.

Pr ∥ B ∥ L^{K_{c}} ⟶^{m} Pr′ ∥ B ∥ \overline{ℓ_{B}m}.X^{K_{c}} ⟶^{ℓ_{B}m} Pr′ ∥ \overline{ℓ_{B}m}.B ∥ X^{K_{c}}

4.6 Output a message to the protocol

The intruder may output any message stored in the buffer B by removing its locking key ℓ_{B}, thereby making the message available to the protocol.

O^{K_{c}} =^{def} ℓ_{B} ▷ . \overline{▷}.O′^{K_{c}}  (14)
O′^{K_{c}} =^{def} \overline{l_{B}}.X^{K_{c}}  (15)

Hence if Pr can receive a message m ∈ K_{p}^{∗} and become Pr′ then we get the following communication.

Pr ∥ \overline{ℓ_{B}m}.B ∥ O^{K_{c}} ⟶^{ℓ_{B}m} Pr ∥ B ∥ \overline{m}.O′^{K_{c}} ⟶^{m}

Pr′ ∥ B ∥ O′^{K_{c}} ⟶^{ℓ_{B}} Pr′ ∥ \overline{ℓ_{B}}.B ∥ X^{K_{c}}

4.7 Analysis and synthesis

Assume that the buffer B contains some message of the form \overline{ℓ_{B}w}.B where w ∈ K_{p}^{∗}. Computing an element of the analysis amounts to step-by-step decryption with any of the compromised keys from K_{c}.

A^{K_{c}} =^{def} ∑_{k∈K_{c}} ℓ_{B}k▷ . \overline{ℓ_{B}▷}.A^{K_{c}} + ∑_{k∈K_{p}} ℓ_{B}k.A_{1}_{k}^{K_{c}} + ℓ_{P} ▷ . \overline{ℓ_{P} ▷}.X^{K_{c}}  (16)

A_{1}_{k}^{K_{c}} =^{def} \overline{ℓ_{B}}.X^{K_{c}∪\{k\}} for all k ∈ K_{p}  (17)

The second summand in equation (16) corresponds to the discovery of a plaintext key, which is promptly added to the set of compromised keys by equation (17), the buffer B is initialized to \overline{ℓ_{B}}.B and the control is given to X^{K_{c}∪\{k\}}. The third summand in (16) allows the intruder to end the analysis phase and return the control to the switch X^{K_{c}}.

Computing an element of the synthesis simply enables to add (step-by-step) as many compromised keys as the intruder wants to the message stored in the buffer B.

S^{K_{c}} =^{def} ∑_{k∈K_{c}} ℓ_{B} ▷ . \overline{ℓ_{B}k▷}.S^{K_{c}} + ℓ_{P} ▷ . \overline{ℓ_{P} ▷}.X^{K_{c}}  (18)

4.8 Deposit

This operation deposits a message from the buffer B into the pool P by moving it key by key.

D^{K_{c}} =^{def} ∑_{k∈K_{p}} ℓ_{B}k▷ . \overline{ℓ_{B}▷}.D_{k}^{K_{c}} + ℓ_{B}.D′_{#}^{K_{c}}  (19)

D_{k}^{K_{c}} =^{def} ℓ_{P} ▷ . \overline{ℓ_{P} k▷}.D^{K_{c}} for all k ∈ K_{p}  (20)
D′_{#}^{K_{c}} =^{def} \overline{ℓ_{B}}.D_{#}^{K_{c}}  (21)
D_{#}^{K_{c}} =^{def} ℓ_{P} ▷ . \overline{ℓ_{P} #▷}.X^{K_{c}}  (22)

The equations (19) and (20) perform the key transfer from B to P. One step of such a transfer looks as follows (here k ∈ K_{p} and w_{1} and w_{2} are arbitrary messages).

\overline{ℓ_{P} w_{1}}.P ∥ \overline{ℓ_{B}kw_{2}}.B ∥ D^{K_{c}} ⟶^{ℓ_{B}kw_{2}} \overline{ℓ_{P} w_{1}}.P ∥ B ∥ \overline{ℓ_{B}w_{2}}.D_{k}^{K_{c}} ⟶^{ℓ_{B}w_{2}}

\overline{ℓ_{P} w_{1}}.P ∥ \overline{ℓ_{B}w_{2}}.B ∥ D_{k}^{K_{c}} ⟶^{ℓ_{P} w_{1}} P ∥ \overline{ℓ_{B}w_{2}}.B ∥ \overline{ℓ_{P} kw_{1}}.D^{K_{c}} ⟶^{ℓ_{P} kw_{1}}

\overline{ℓ_{P} kw_{1}}.P ∥ \overline{ℓ_{B}w_{2}}.B ∥ D^{K_{c}}

Recall that as indicated before, the messages are stored in reverse order in P. When the bottom of the buffer B is reached, the second summand in equation (19) can be applied. First the key ℓ_{B} is returned to the buffer B by equation (21) and finally the control is given to the process constant X^{K_{c}} while adding the separation key # into the pool by equation (22).

4.9 Retrieve

To retrieve a message from the pool (the most complicated operation of the construction), the retrieval process scans through the message separation markers # until it nondeterministically decides to copy a message to the buffer (here it is also the only place where the temporary buffer is used).

R^{K_{c}} =^{def} \overline{ℓ_{B}}.R_{1}^{K_{c}}  (23)
R_{1}^{K_{c}} =^{def} ∑_{k∈K_{p}∪\{#\}} ℓ_{P} k▷ . \overline{ℓ_{P} ▷}.R_{k}^{K_{c}} + ℓ_{P} #▷ . \overline{ℓ_{P} ▷}.S_{#}^{K_{c}} + ℓ_{P} .T′_{2}^{K_{c}}  (24)

R_{k}^{K_{c}} =^{def} ℓ_{T} ▷ . \overline{ℓ_{T} k▷}.R_{1}^{K_{c}} for all k ∈ K_{p} ∪ \{#\}  (25)
S_{#}^{K_{c}} =^{def} ℓ_{T} ▷ . \overline{ℓ_{T} #▷}.T^{K_{c}}  (26)
T^{K_{c}} =^{def} ∑_{k∈K_{p}} ℓ_{P} k▷ . \overline{ℓ_{P} ▷}.T_{k}^{K_{c}} + ℓ_{P} #▷ . \overline{ℓ_{P} #▷}.T_{2}^{K_{c}} + ℓ_{P} .T′_{2}^{K_{c}}  (27)

T_{k}^{K_{c}} =^{def} ℓ_{T} ▷ . \overline{ℓ_{T} k▷}.T_{1}_{k}^{K_{c}} for all k ∈ K_{p}  (28)
T_{1}_{k}^{K_{c}} =^{def} ℓ_{B} ▷ . \overline{ℓ_{B}k▷}.T^{K_{c}} for all k ∈ K_{p}  (29)
T′_{2}^{K_{c}} =^{def} \overline{ℓ_{P}} .T_{2}^{K_{c}}  (30)
T_{2}^{K_{c}} =^{def} ∑_{k∈K_{p}∪\{#\}} ℓ_{T} k▷ . \overline{ℓ_{T} ▷}.T_{3}_{k}^{K_{c}} + ℓ_{T} .T_{4}^{K_{c}}  (31)

T_{3}_{k}^{K_{c}} =^{def} ℓ_{P} ▷ . \overline{ℓ_{P} k▷}.T_{2}^{K_{c}} for all k ∈ K_{p} ∪ \{#\}  (32)
T_{4}^{K_{c}} =^{def} \overline{ℓ_{T}} .X^{K_{c}}  (33)

First the buffer B is initialized with the key ℓ_{B} by equation (23). Then by equations (24) and (25) all keys from K_{p} can be moved one by one to the temporary buffer B_{T}. In case that the #-key is discovered during the process, the intruder can either continue as before by placing the key into the temporary buffer (using the first summand in (24)), or he can decide that # is the start of the selected message to be copied into the buffer B and use the second summand of (24).

In the latter case equation (26) places the # key into the temporary buffer B_{T} and evokes the process constant T^{K_{c}} which copies the next piece of the message from the pool both into the temporary buffer B_{T} and also into the buffer B. This is done using the equations (28) and (29) and the control returns to T^{K_{c}}. Whenever the first separation key # appears as the outermost key, the second summand in (27) applies and the intruder continues from T_{2}^{K_{c}} in equation (31). The same happens when the end of the pool is reached (third summand of equation (27)). In this case the key ℓ_{P} is first return into the pool by the process constant T′_{2}^{K_{c}} and then the process continues by equation (31) as before.

The remaining equations (31) – (33) simply return the content of the temporary buffer B_{T} back to the pool and give the control to X^{K_{c}} (making sure that the temporary buffer is reseted to \overline{ℓ_{T}} .B_{T}).

4.10 Correctness of the encoding

We now show that the intruder faithfully describes the environment sensitive semantics defined in the beginning of Section 4 by axioms (A1) – (A4).

To do this, we need to define the knowledge of the intruder. We take this to be the totality of the set of messages that he can output to the environment.

Let E =^{def} ∑_{k∈K_{p}} k▷ . \overline{k▷}.E be an observer (environment) which allows us to observe all messages encrypted by keys from K_{p}. Let ⟹ be an (unlabelled) reflexive and transitive closure of transition relations labelled by actions that are not available to the environment (internal communication of the intruder), i.e.,

⟹ =^{def} ( ⋃_{m∈(K∖K_{p})·K^{∗}} ⟶^{m} )^{∗}.

The set of known messages of an intruder configuration I is defined by

km(I) =^{def} {w ∈ K_{p}^{∗} | E ∥ I ⟹ ∘ ⟶^{w}}.

We say that I is a proper intruder configuration whenever I does not contain any parallel component of the form L^{K_{c}}, O^{K_{c}} or \overline{m}.O′^{K_{c}}. In other words it is not directly committed to communicate with the environment.

We now show an operational correspondence result which states that the intruder, as described above, accurately describes the behaviour of the environment sensitive semantics expressed by axioms (A1) – (A4). The following lemma shows that the intruder can synthesize all possible messages.

Lemma 4. For any proper intruder configuration I it holds that km(I) = S(km(I)).

Proof. The inclusion km(I) ⊆ S(km(I)) follows from the definition of synthesis. Let w ∈ S(km(I)). We will show that w ∈ km(I). Because of Remark 4 we know that the set of compromised keys K_{c} (where n = |K_{c}|) can be computed by analyzing of certain messages m_{1}, …, m_{n} ∈ km(I). As these messages belong to km(I) they can consequently be placed (in the given order) into the buffer B and analyzed. This will update the current set of compromised keys remembered by the intruder to the complete set K_{c}. Because of Proposition 1 we know that w can be constructed by first placing a selected message into the buffer and by removing all the compromised keys (by A^{K_{c}}) and then by adding the compromised keys in order to form w (by S^{K_{c}}). The message w can then be communicated to the environment E by O^{K_{c}} and hence w ∈ km(I). ⊓ ⊔

The first theorem states that the intruder can mimic the behaviour of the environment-sensitive semantics.

Theorem 3 (Completeness). Let C be a protocol configuration, let T ⊆ K^{∗}, and let I be a proper intruder configuration such that S(T) = km(I). If

(C, T) → (C′, T′)

then there exists w ∈ K_{p}^{∗} and a transition sequence

(C ∥ I) ⟹ ∘ ⟶^{w} (C′ ∥ I′)

such that S(T′) = km(I′) and I′ is a proper intruder configuration.

Proof. The intruder’s strategy is clear. He listens to every message communicated by the protocol and stores all such messages into the pool in order to be able to synthesize the appropriate messages and communicate them back to the protocol at some later stage.

First observe that there are four possible axioms (A1) – (A4) to perform (C, T) → (C′, T′). In case of the axioms (A1) and (A2) we know that the protocol configuration C receives a message w from S(T) and becomes C′, and that T′ = T. Because w ∈ S(T) = km(I) we know that the intruder I can perform

I ⟹ I′′ such that E ∥ I′′ ⟶^{w} E′ ∥ I′ and hence also (C ∥ I) ⟹ ∘ ⟶^{w} (C′ ∥ I′).

Moreover, km(I′) = km(I) as required because every message that appears in the buffer B can be also copied to the pool P for a use later on. It is also easy to see that I′ is proper.

In case of the axioms (A3) and (A4) the protocol configuration C emits a message w and becomes C′, and T′ = T ∪ {w}. In this case the intruder deposits the content of the buffer into the pool (in case that it was not empty) and then receives the message w from C. This means that (C ∥ I) ⟹ ∘ ⟶^{w} (C′ ∥ I′) and moreover km(I′) now contains the message w (obviously I′ is proper). This implies that S(T′) = S(T ∪ {w}) = km(I′) because of Lemma 4.

⊓ ⊔

Conversely, the intruder cannot gain any extra knowledge than the one he can construct by analysis and synthesis of the available messages.

Theorem 4 (Soundness). Let C be a protocol configuration, let T ⊆ K^{∗}, and let I be an intruder configuration such that km(I) ⊆ S(T). If for some w ∈ K_{p}^{∗}

(C ∥ I) ⟹ ∘ ⟶^{w} (C′ ∥ I′)

then there exists a transition

(C, T) → (C′, T′) or (C, T) → ∘ → (C′, T′)

such that km(I′) ⊆ S(T′).

Proof. There are two cases to distinguish. In the first case the intruder either listens to the message w sent by C, or he outputs w for a communication with the protocol C. This means that there is a corresponding transition also in (C, T) → (C′, T′) and it is easy to verify that km(I′) ⊆ S(T′). In the second case the intruder does not interfere with the communication in C (hence km(I′) = km(I)) and such a communication step is simulated by two steps (C, T) → ∘ → (C′, T′) (in the environment sensitive semantics all messages must pass through T). By the fact that S(T) ⊆ S(T′), we can immediately see that km(I′) ⊆ S(T′). ⊓ ⊔

5 Replicative ping-pong protocols

In this section we shall define a replicative variant of our calculus for ping-pong protocols. We will then show that this formalism is not Turing powerful because the reachability problem becomes decidable. This is to be put in contrast with several results where replicative calculi are known to be capable of simulating recursive ones (see e.g. [17] for the case of pi-calculus which implies also the same result for spi-calculus, and [13, 18] for other examples). On the other hand, a similar discrimination result as ours between recursion and replication was recently proved for CCS [7].

Let us now define replicative ping-pong protocols. Let K be the set of encryption keys as before. The set Conf of protocol configurations is given by the following abstract syntax

C ::= 0 | v▷ . \overline{w▷} | v | \overline{w} | !(v▷ . \overline{w▷}) | !(v) | !(\overline{w}) | C ∥ C

where 0 is the symbol for the empty configuration, v and w range over K^{∗}, and ! is the bang operator (replication). As before, we shall introduce structural congruence ≡, which is the smallest congruence over Conf such that

– (Conf, ∥, 0) is a commutative monoid

– ϵ ∥ C ≡ C ≡ \overline{ϵ} ∥ C

– !(ϵ) ≡ 0 ≡ !(\overline{ϵ})

– !(C) ≡ C ∥!(C).

A labelled transition system determined by a configuration (where states are configurations modulo ≡ and labels are non-empty messages as before) is defined by the following SOS rules (recall the replicative axiom !(C) ≡ C ∥!(C) and the fact that ‘∥’ is commutative).

\frac{m ∈ K^{+}}{\overline{m} ∥ m ∥ C ⟶^{m} C}  \frac{m ∈ K^{+} m = vα}{\overline{m} ∥ v▷ . \overline{w▷} ∥ C ⟶^{m} \overline{wα} ∥ C}

Example 3. An initial configuration C =^{def}!(\overline{k}) ∥ !(k▷ . \overline{kk▷}) generates a labelled transition system in Figure 2 with infinitely many reachable configurations (only a finite fragment is depicted). Observe that (unlike recursive protocols) the number of parallel components can grow arbitrarily (e.g. the left-most branch in the picture). The reason is that we allow prefixes of the form !(\overline{w}) which can unconditionally output new messages and that we have replicative agents accepting these messages.

In case that the number of output prefixes for all reachable configurations is bounded by some number n, the parallel components of the form !(v), !(\overline{w}) and !(v ▷ . \overline{w▷}) can be replaced by n parallel occurrences of fresh process constants

P_{!(v)}, P_{!(\overline{w})} and P_{!(v▷. \overline{w▷})} respectively such that P_{!(v)} =^{def} v.P_{!(v)}, P_{!(\overline{w})} =^{def} \overline{w}.P_{!(\overline{w})}

and P_{!(v▷. \overline{w▷})} =^{def} v ▷ . \overline{w▷}.P_{!(v▷. \overline{w▷})}, and hence it can be simulated by recursive protocols. ⊓ ⊔

\xymatrix{ &  &  & C \ar[d]^{k} \\  &  &  & \overline{kk} ∥ C \ar@{-->}[dl]_{k} \ar@{-->}[dr]^{kk} \\  &  & \overline{kk} ∥ \overline{kk} ∥ C \ar@{-->}[dl]_{k} \ar@{-->}[dr]^{kk} &  & \overline{kkk} ∥ C \ar@{-->}[dl]_{k} \ar@{-->}[dr]^{kkk} \\  & \overline{kk} ∥ \overline{kk} ∥ \overline{kk} ∥ C \ar@{-->}[dl]_{k} \ar@{-->}[dr]^{kk} &  & \overline{kk} ∥ \overline{kkk} ∥ C \ar@{-->}[dl]_{k} \ar[dd]^{kk} \ar@{-->}[dr]^{kkk} &  & \overline{kkkk} ∥ C \ar@{-->}[dl]_{k} \ar@{-->}[dr]^{kkkk} \\ \overline{kk} ∥ \overline{kk} ∥ \overline{kk} ∥ \overline{kk} ∥ C &  & \overline{kk} ∥ \overline{kk} ∥ \overline{kkk} ∥ C &  & \overline{kk} ∥ \overline{kkkk} ∥ C &  & \overline{kkkkk} ∥ C \\  &  &  & \overline{kkk} ∥ \overline{kkk} ∥ C}

Fig. 2. Initial fragment of a labelled transition system for C =^{def}!(\overline{k}) ∥ !(k▷ . \overline{kk▷})

We shall now show that the reachability problem for general replicative pingpong protocols is decidable. We reduce our problem to reachability of weak process rewrite systems (wPRS) which was very recently proven to be decidable [15].

Following the work of Mayr [16], let Const be a set of process constants. The set E of process expressions over Const is defined by

E ::= ϵ | X | E.E | E ∥ E

where ϵ is the symbol for empty expression, X ranges over Const, ‘.’ is the operator of sequential composition and ‘∥’ is the operator of parallel composition. We identify processes up to structural congruence, which is the least congruence such that ‘.’ is associative, ‘∥’ is associative and commutative and ϵ is a unit for ‘.’ and ‘∥’.

Let Q be a finite set of control-states and Act a set of actions. A stateextended process rewrite system (sePRS) is a finite set Δ of rewrite rules of the form pE ⟶^{a} qF where p, q ∈ Q, a ∈ Act, and E, F ∈ E such that E ≠ ϵ.

A given sePRS Δ generates a labelled transition system T (Δ) where states are process expressions over Const modulo the structural congruence, the set of actions is Act and the transition relation is given by the following SOS rules (recall that ‘∥’ is commutative).

\frac{(pE ⟶^{a} qF) ∈ Δ}{pE ⟶^{a} qF}  \frac{pE ⟶^{a} qE′}{p(E.F) ⟶^{a} q(E′.F)}  \frac{pE ⟶^{a} qE′}{p(E ∥ F) ⟶^{a} q(E′ ∥ F)}

A sePRS Δ is called a weak process rewrite system (wPRS) iff there is a partial ordering ≤ on Q such that all rewrite rules pE ⟶^{a} qF from Δ satisfy that q ≤ p.

Theorem 5 ([15]). The reachability problem for wPRS is decidable.

Let us now consider an arbitrary configuration C in the calculus of replicative ping-pong protocols. We shall construct a wPRS system Δ which preserves the reachability property.

The configuration C can be naturally written as C ≡ A ∥ B ∥ O where A contains all parallel components of the form !(v ▷ . \overline{w▷}), !(v) and !(\overline{w}); B contains all parallel components of the form v▷ . \overline{w▷} and v; and O contains all output prefixes of the form \overline{w}. Here we assume that the rules of the structural congruence ≡ are applied as long as possible in order to minimize the size of the configuration C (such assumptions are implicit also later on). Observe now that any configuration C′ ≡ A ∥ B′ ∥ O′ reachable from C contains exactly the same part A and every parallel component from B′ is also in B.

The intuition of the reduction is that A does not have to be remembered as all parallel components from A are always available, B will be stored in controlstates of the wPRS (note that there are only finitely many different components in B′ for all reachable configurations of the form A ∥ B′ ∥ O′) and the parallel components from O will be stored as a parallel composition of stacks in the wPRS system.

Let C ≡ A ∥ B ∥ O be the initial configuration. Formally, the wPRS rules Δ where Const =^{def} K ∪ {Z, X} (Z is a special symbol for the bottom of a stack, X is a process constant for creating more parallel components) and where Q =^{def} {p^{B′} | ∃B′′ s.t. B ≡ B′ ∥ B′′} are defined as follows.

1. p^{B′}X ⟶ p^{B′}(X ∥ w.Z) B′ ⊆ B and !(\overline{w}) ∈ A
2.  p^{B′}w.Z ⟶ p^{B′}  B′ ⊆ B and !(\overline{w}) ∈ A
3.  p^{B′}Z ⟶ p^{B′}  B′ ⊆ B
4.  p^{B′}v.Z ⟶ p^{B′}  B′ ⊆ B and !(v) ∈ A
5.  p^{B′}v ⟶ p^{B′}w  B′ ⊆ B and !(v▷ . \overline{w▷}) ∈ A
6.  p^{B′}v.Z ⟶ p^{B′′}  B′ ⊆ B and B′ ≡ B′′ ∥ v
7.  p^{B′}v ⟶ p^{B′′}w  B′ ⊆ B and B′ ≡ B′′ ∥ v▷ . \overline{w▷}

In the definitions above, whenever we have w ∈ K^{∗}, we use the word w also in the wPRS rules in the meaning that it represents a sequential composition of process constants contained in w, i.e., if w = a_{1}a_{2} ⋯ a_{n} then w in the wPRS rules stands for the sequential composition a_{1}.a_{2}. . . . .a_{n}. Moreover B′ ⊆ B means that there is some B′′ such that B ≡ B′ ∥ B′′ and x ∈ A means that the expression x is a parallel component in A. All actions are omitted as they are irrelevant for the reachability question.

Rules 1. – 3. correspond to the structural congruence ≡. As !(\overline{w}) ≡ \overline{w} ∥!(\overline{w}) rule 1. enables us to create a new parallel component \overline{w} whenever !(\overline{w}) ∈ A and by rule 2. such a component can always be deleted. Rule 3. corresponds to the fact that ϵ ∥ C ≡ C. (Recall that we assume that C does not contain any component of the form !(ϵ) or !(\overline{ϵ}).)

Rules 4. – 7. are computational rules: in rules 4. and 5. we allow the reception of messages by the components in A and the control-state does not change in this case; in rules 6. and 7. we do the same for components in B′ (the current remaining part of B) and whenever such a component is used, we remove it from B′ by changing the control-state to p^{B′′}.

Let us assume the initial configuration C ≡ A ∥ B ∥ O as above such that O ≡ \overline{w_{1}} ∥ \overline{w_{2}} ∥ ⋯ ∥ \overline{w_{n}}. The initial configuration of the wPRS system Δ is then

p^{B}(X ∥ w_{1}.Z ∥ w_{2}.Z ∥ ⋯ ∥ w_{n}.Z).

It is easy to see that every rewriting step in Δ corresponds either to a single computational step in the replicative ping-pong protocol or to an application of some congruence rule. On the other hand, any communication in the protocol can be directly simulated in Δ.

Hence we can make the following observation (assuming that O′ ≡ \overline{w′_{1}} ∥ \overline{w′_{2}} ∥ ⋯ ∥ \overline{w′_{n′}}).

Lemma 5. It holds that

A ∥ B ∥ O ⟶^{∗} A ∥ B′ ∥ O′

if and only if

p^{B}(X ∥ w_{1}.Z ∥ w_{2}.Z ∥ ⋯ ∥ w_{n}.Z) ⟶^{∗} p^{B′}(X ∥ w′_{1}.Z ∥ w′_{2}.Z ∥ ⋯ ∥ w′_{n′}.Z).

Theorem 6. The reachability problem for replicative ping-pong protocols is decidable.

Proof. By Lemma 5 we reduced the problem to the reachability question for wPRS (observe that p^{B′} ≥ p^{B′′} iff B′′ ⊆ B′ is the natural ordering on controlstates of the wPRS demonstrating that the control-state unit has a monotone behaviour). The decidability result then follows from Theorem 5. ⊓ ⊔

6 Conclusion

We have seen that ping-pong protocols extended with recursive definitions have full Turing power. This is the case even in the absence of nondeterministic choice operator ‘+’. A result like this implies that any reasonable property for all richer calculi cannot be automatically verified.

We also presented an explicit description of the active intruder in the syntax of recursive ping-pong protocols. The presented encoding gives an exponential blow-up in the size of the protocol. However, it is in fact not necessary and for a given protocol an active intruder of polynomial size can be constructed (it is enough to store the set of compromised keys in an extra buffer). We have decided to present the construction which is exponentially larger for clarity reasons. Nevertheless the polynomial modification of the analysis and synthesis part using the extra buffer can be easily implemented – it only becomes technically more tedious.

Finally, we showed that reachability analysis for a replicative variant of the protocol becomes feasible. Our proof uses very recent results from process algebra [15] and can be compared to the work of Amadio, Lugiez and Vanackère [4] which establishes the decidability of reachability for a similar replicative protocol capable of ping-pong behaviour. Their approach uses a notion of a pool of messages explicitly modelled in the semantics and reduces the question to a decidable problem of reachability for prefix rewriting. In our approach we allow spontaneous generation of new messages which is not possible in their calculus. Moreover, we can distinguish between replicated and once-only behaviours (unlike in [4] where all processes have to be replicated).

Last but not least we hope that our approach can be possibly extended to include other operations as the decidability result for replicative protocols uses only a limited power of wPRS (only a parallel composition of stacks). Hence there is a place for further extensions of the protocol syntax while preserving a decidable calculus (e.g. messages of the form \overline{k_{1}(k_{2} op k_{3})k_{4}} for some extra composition operation op on keys can be easily stored in wPRS as k_{1}.(k_{2} ∥ k_{3}).k_{4}). Such a study is left for future research.

Other open problems include decidability of bisimilarity for replicative pingpong protocols and the question to determine general conditions that guarantee equi-expressiveness of recursion and replication (see e.g. [17, 13, 18]).

References

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

2. 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.

3. 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.

4. R.M. Amadio, D. Lugiez, and V. Vanackère. On the symbolic reduction of processes with cryptographic functions. Theoretical Computer Science, 290(1):695–740, October 2002.

5. M. Boreale. Symbolic trace analysis of cryptographic protocols. In Proceedings of the 28th Colloquium on Automata, Languages and Programming (ICALP’01), volume 2076 of LNCS, pages 667–681. Springer, July 2001.

6. O. Burkart, D. Caucal, F. Moller, and B. Steffen. Verification on infinite structures. In J. Bergstra, A. Ponse, and S. Smolka, editors, Handbook of Process Algebra, chapter 9, pages 545–623. Elsevier Science, 2001.

7. N. Busi, M. Gabbrielli, and G. Zavattaro. Replication vs. recursive definitions in channel based calculi. In Proceedings of the 30th International Colloquium on Automata, Languages, and Programming (ICALP’03), volume 2719 of LNCS, pages 133–144. Springer-Verlag, 2003.

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

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

10. 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.

11. 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.

12. 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.

13. P. Giambiagi, G. Schneider, and F.D. Valencia. On the expressiveness of infinite behavior and name scoping in process calculi. In Proceedings of the 7nd International Conference on Foundations of Software Science and Computation Structures (FOSSACS’04), volume 2987 of LNCS, pages 226–240. Springer-Verlag, 2004.

14. H. Hüttel and J. Srba. Recursive ping-pong protocols. In Proceedings of the 4th International Workshop on Issues in the Theory of Security (WITS’04), pages 129–140, 2004.

15. M. Křetínský, V. Řehák, and J. Strejček. Extended process rewrite systems: Expressiveness and reachability. In Proceedings of the 15th International Conference on Concurrency Theory (CONCUR’04), volume 3170 of LNCS, pages 355–370. Springer-Verlag, 2004.

16. R. Mayr. Process rewrite systems. Information and Computation, 156(1):264–286, 2000.

17. R. Milner. The polyadic pi-calculus: a tutorial. In F. L. Bauer, W. Brauer, and H. Schwichtenberg, editors, Logic and Algebra of Specification, pages 203–246. Springer-Verlag, 1993.

18. M. Nielsen, C. Palamidessi, and F.D. Valencia. On the expressive power of temporal concurrent constraint programming languages. In Proceedings of the 4th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, pages 156–167. ACM Press, 2002.

19. 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.

20. R.J. van Glabbeek. The linear time - branching time spectrum I: The semantics of concrete, sequential processes. In J. Bergstra, A. Ponse, and S. Smolka, editors, Handbook of Process Algebra, chapter 1, pages 3–99. Elsevier Science, 2001.

Recent BRICS Report Series Publications

RS-04-23 Hans Hüttel and Jiří Srba. Recursion vs. Replication in Simple Cryptographic Protocols. October 2004. 26 pp. To appear in Vojtas, editor, 31st Conference on Current Trends in Theory and Practice of Informatics, SOFSEM ’05 Proceedings, LNCS, 2005.

RS-04-22 Gian Luca Cattani and Glynn Winskel. Profunctors, Open Maps and Bisimulation. October 2004. 64 pp. To appear in Mathematical Structures in Computer Science.

RS-04-21 Glynn Winskel and Francesco Zappa Nardelli. New-HOPLA— A Higher-Order Process Language with Name Generation. October 2004. 38 pp.

RS-04-20 Mads Sig Ager. From Natural Semantics to Abstract Machines. October 2004. 21 pp. Presented at the International Symposium on Logic-based Program Synthesis and Transformation, LOP-STR 2004, Verona, Italy, August 26–28, 2004.

RS-04-19 Bolette Ammitzbøll Madsen and Peter Rossmanith. Maximum Exact Satisfiability: NP-completeness Proofs and Exact Algorithms. October 2004. 20 pp.

RS-04-18 Bolette Ammitzbøll Madsen. An Algorithm for Exact Satisfiability Analysed with the Number of Clauses as Parameter. September 2004. 4 pp.

RS-04-17 Mayer Goldberg. Computing Logarithms Digit-by-Digit. September 2004. 6 pp.

RS-04-16 Karl Krukow and Andrew Twigg. Distributed Approximation of Fixed-Points in Trust Structures. September 2004. 25 pp.

RS-04-15 Jesús Fernando Almansa. Full Abstraction of the UC Framework in the Probabilistic Polynomial-time Calculus ppc. August 2004.

RS-04-14 Jesper Makholm Byskov. Maker-Maker and Maker-Breaker Games are PSPACE-Complete. August 2004. 5 pp.

RS-04-13 Jens Groth and Gorm Salomonsen. Strong Privacy Protection in Electronic Voting. July 2004. 12 pp. Preliminary abstract presented at Tjoa and Wagner, editors, 13th International Workshop on Database and Expert Systems Applications, DEXA ’02 Proceedings, 2002, page 436.