Provable Anonymity
Flavio D. Garcia Ichiro Hasuo

Wolter Pieters

Peter van Rossum

Institute for Computing and Information Sciences, Radboud University Nijmegen
P.O. Box 9010, 6500 GL Nijmegen, The Netherlands
E-mail: {flaviog,ichiro,wolterp,petervr}@cs.ru.nl
URL: http://www.cs.ru.nl/{~flaviog, ~ichiro, ~wolterp, ~petervr}
ABSTRACTThis paper provides a formal framework for the analysis
of information hiding properties of anonymous communication protocols in terms of epistemic logic. The key ingredient is our notion of observational equivalence, which isbased on the cryptographic structure of messages and relations between otherwise random looking messages. Tworuns are considered observationally equivalent if a spy cannot discover any meaningful distinction between them. We
illustrate our approach by proving sender anonymity andunlinkability for two anonymizing protocols, Onion Routing and Crowds. Moreover, we consider a version of Onion
Routing in which we inject a subtle error and show how ourframework is capable of capturing this flaw.

Categories and Subject Descriptors
C.2.2 [Computer-Communication Networks]: Network
Protocols—Protocol verification; F.4 [Mathematical Logic
and Formal Languages]

General Terms
Security, Theory, Verification

Keywords
Anonymity, Unlinkability, Privacy, Epistemic Logic, Knowledge, Cryptography, Formal Methods, Crowds, Onion Routing

1.

INTRODUCTION

There is a growing concern about the amount of personal
information that is being gathered about people’s actions.
Websites habitually track people’s browsing behavior, banks
track people’s financial whereabouts, and current trends inapplications of RFID chips will make it possible to track people’s physical location. Furthermore, several European governments are considering to oblige Internet Service Providers
to keep traffic logs of all communication on the Internet.

Permission to make digital or hard copies of all or part of this work forpersonal or classroom use is granted without fee provided that copies are
not made or distributed for profit or commercial advantage and that copies
bear this notice and the full citation on the first page. To copy otherwise, torepublish, to post on servers or to redistribute to lists, requires prior specificpermission and/or a fee.
FMSE’05, November 11, 2005, Alexandria, Virginia, USA.
Copyright 2005 ACM 1-59593-231-3/05/0011 ...$5.00.

To protect users from undesired information leaks, there
are various protocols and tools that provide some form ofanonymity, e.g., for web browsing and e-mailing; for instance
Tor [6], Freenet [4], and Mixminion [5].
Anonymizing Protocols In 1981, Chaum [3] pioneered
the idea of what are currently called Chaum mixes. If A
wants to send a message m to B, she chooses a number of relays (cascading mixes, in Chaum’s terminology), say R1 , R2 ,and sends {|R2 , {|B, {|m|}B |}R2 |}R1 to R1 . Here {| . . . |}X denotes encryption with the public key of X. Relay R1 decrypts the first layer of encryption and forwards the message {|B, {|m|}B |}R2 to R2 , who peels off another layer andsends the remainder to B. Traffic analysis is complicatedas every relay queues messages until a certain number havebeen received and relays them in a batch. Also, dummy
network traffic can be generated if not enough messages areavailable. This technique forms the basis of Onion Routing[9] and its successor Tor [6], a currently running networkof relays providing anonymous communication for instancewith web servers.
Another idea to provide some kind of anonymity is given
by Crowds [16]. Here the message m is sent to a relay R1 ,which then probabilistically either forwards the message toanother relay R2 , or to its final destination. A key idea hereis that every member of the network can act as a relay.
Various notions of anonymous communication exist and various attacker models have to be considered. Chaum mixes
typically provide sender anonymity: the ultimate receiver Bof the message m does not know who originated the message. It also provides unlinkability: someone observing all
network traffic cannot tell that A and B are communicating.
Crowds does not provide unlinkability: a global eavesdropper will be able to see the message m passing throughthe whole network and will see the message m moving from
A to B over a number of relays. However, it does provide
sender anonymity even if some of the members of the network are corrupted.
Formal methods For security and authentication, a number of formal methods and automated tools have been developed to determine the correctness of security and authentication protocols (see, e.g., [14, 12, 10]). In contrast, theformalization of anonymity is still in its infancy. This paper
presents a formal framework in which various information
hiding properties can be expressed in a clear and precise
manner. It enables us to formulate competing notions ofanonymity in a uniform fashion and compare them.
Our contribution and related work Starting point of
our approach, also present in [11], is the idea that various

information hiding properties can best be expressed in thelanguage of epistemic logic. This makes it possible to reason
not only about the messages in a run, but also about theknowledge agents gain from these messages. For instance,
sender anonymity can typically be formulated as the receiver
not knowing who sent a certain message.
Central in the epistemic framework is our notion of observational equivalence of runs. An agent knows a fact of acertain run r if that fact is true in all possible worlds, i.e.,
in all runs that are observationally equivalent to r. In [11],the observational equivalence is basically assumed, whereas
we actually construct such a relation.
Our notion of observational equivalence takes care of thecryptographic operations that are defined on the set of messages. We should remark that other works present similar equivalence relations on the set of messages, e.g., [13,1]. Ours is unique in the sense that it not only deals withwhether or not messages are encrypted, but also takes careof relations between messages. Especially for dealing with
unlinkability this is essential. For example, if an agent A
sends a message {|m|}K and another agent B either sends
the message hash({|m|}K ) (for instance, to acknowledge receipt of A’s message), or the message {|m|}K (for instance,
forwarding it to someone else), then a global observer could
link A and B, even though all messages involved look likerandom bit strings to this global observer.
Note that this formal approach is possibilistic in nature: it
only considers whether or not it is possible that A and B are
communicating, but not the probability that they are. Thereis another body of literature studying probabilistic aspectsof anonymity, e.g., [18, 17]. These papers generally assume
the correctness of the anonymizing protocols in the formal
message sense and then compute measures of anonymity.
We will show that this epistemic framework allows us
to formally describe and verify various information hiding
properties that are considered in the literature.
Organization of the paper We start in Section 2 with thedefinition of the message algebra. Then Section 3 fixes the
network and intruder model and describes the fundamental
notion of observational equivalence of runs. Section 4 introduces the epistemic operators and show how these operators
can be used to express various information hiding properties, such as sender anonymity and unlinkability, can be expressed. Finally, to illustrate the power of our approach,we consider in Section 5 abstract versions of Crowds andOnion Routing and formally prove their anonymizing properties. We also consider a version of Onion Routing thathas a subtle error and show how our framework is capableof detecting this flaw.
Notations and terminology Throughout this paper asecret key is called a symmetric key. In an asymmetric encryption a key pair consists of a public key and a private
key.
We clearly distinguish the verbs to know and to possess:an agent knows a fact while it possesses a message. The
former acts as an epistemic operator which is applied to a
proposition on the run, while the latter concerns accessibility
to messages via cryptographic operations such as encryption
or decryption.
The set ‘X ∗ consists of all the finite lists over X, that∗nis, X =n∈N X . For a list r with length |r|, the ith element of r is denoted by ri . The head-closed sublist
hr0 , r1 , . . . , ri−1 i of r is denoted by r<i .

2.

THE MESSAGE ALGEBRAIn this section we present our model of the message algebra, and introduce the closure operator on a set of messages.
This is done in a standard way similar to [14, 12].
Definition 1. (Message algebra) The set of messages MSG
is the set given by the following BNF notation:
MSG 3 m ::= name(A) | nonce(n)|key(K) | enc(m, K)|hash(m) | hm, mi.
where A is taken from a set of agents, n from a set of nonces
and K from a set of keys. We also assume that there isa function (−)−1 from keys to keys with the property that(K −1 )−1 = K. If K −1 = K, then K is called a symmetrickey, otherwise one of K and K −1 is called a private key andthe other one a public key.
We abbreviate enc(m, K) to {|m|}K and omit angle brackets
inside encryptions. Typically, an agent A has an associatedpublic key and we denote encryption with the public key of
A simply by {|m|}A . Terms of the form name(A), nonce(n),key(K) are said to be primitive. To simplify notation, we
will simply write A instead of name(A), and similarly fornonces and keys.
There is a natural notion of subterm relation on the set of
messages, which we denote by ¹. This relation is unawareof cryptographic operations; e.g., m ¹ {|m|}K and m ¹
hash(m) always hold. Furthermore, a function π : MSG →MSG is said to be structure preserving if it maps names
to names, nonces to nonces, keys to keys, encrypted messages to encrypted messages, hashes to hashes, and satisfies
π(hm1 , m2 i) = hπ(m1 ), π(m2 )i for all messages m1 , m2 .
The closure U of a set U of messages consists of all the messages that can be extracted and constructed from those in
U using cryptographic operations such as decryption, encryption, tupling and decomposing tuples. For the formal
definition, see Appendix A. This closure operation is important here for two reasons. One reason, which is common informal modelling of security protocols, is that an agent may
send only the messages it can construct from what it has
seen (see Definition 5). The other one, which is novel, isthat the closure of the possessions of an agent restricts theset of runs that the agent considers to be observationallyequivalent to a given run (see Definition 8).

3.

RUNS AND OBSERVATIONAL EQUIVALENCE

3.1

Network model

To model anonymity properties, we have to be able totalk about the sender and receiver of a message. Therefore
we include explicit sender and receiver information in our
notion of event below. In a real world setting, an event
would correspond to an IP package, which has sender andreceiver information in the header and the actual message
in the body.
Definition 2. (Agents, events) We denote by AG a nonempty set of agents, which has a special element spy for the
intruder. An agent which is not spy is called a regular agent.
An event is a triple (A, B, m) of the sender A, the recipientB and the delivered message m. To make the intention clear
we denote the above event by (A → B : m). The set of all
events is denoted by Event.
Definition 3. (Runs) A run is a finite list of events, i.e.
an element of the set Run := Event∗ . A run describes all
the events that have occurred in a network. The function
msg : Run → P(MSG) extracts all the messages occurring ina run. That is,`
msg (A0 → B0 : m0 ),(A1 → B1 : m1 ),..
.
(An−1 → Bn−1 : mn−1 )3.2´= {m0 , m1 , . . . , mn−1 }.

Attacker model

It is standard to verify security properties such as authentication or secrecy under the Dolev-Yao intruder model [7].
In that model the network is completely under the control of
the intruder, hence no agent can be sure who sent the message it receives, or whether the intended recipient actually
receives the message send.
To model anonymity properties, it is customary to use aweaker attacker model. We assume that the intruder is passive, i.e., observes all network traffic, but does not actively
modify it. It is however possible that some regular agents arecorrupted; we will later model this in terms of the keys theintruder possesses. This setting enables us to express that a
run of a protocol satisfies a certain information hiding property as long as certain agents are not corrupted. Contrary
to the intruder, the regular agents are not necessarily awareof all the events in the run; we adopt the convention thatthey only see the events in which they are involved as senderor receiver.
Definition 4. (Visible part of runs) Let r be a run. For aregular agent A ∈ AG \ {spy} the A-visible part of r, denotedby r|A , is the sublist of r consisting of all the events thathave A in either sender or receiver field. The spy-visible partof r, denoted by r|spy , is identical to r.

3.3

Communication protocol

It is important to specify the set of runs of a protocol,
which is the set of possible worlds used in the definitionof knowledge. There, runs which are illegitimate with respect to a protocol are excluded because every agent knowsthat those runs cannot happen. In that sense, a protocol
is common knowledge. In this paper a protocol consists of
two components, namely the candidate runs and the initialpossessions.
The set of candidate runs is just a set of runs. Intuitively,
it consists of those runs which fulfill the requirements on
which messages may/must be sent by an agent. In the examples (see Section 5) we describe the set of candidate runs
by means of inference rules.
An initial possession function IPo : AG → P(MSG) assigns
to each agent the set of messages the agent possesses before
communication takes place. Typically an agent’s initial possessions consists of its private key and the public keys of allagents. We require that, for every agent A, IPo(A) consistsof only primitive messages.

We denote by PossIPo (r, A, i) the set of the messages thatan agent A possesses at stage i of the run r. It is the closure of the union of: 1) A’s initial possession `IPo(A); 2)´
the messages A has seen up to this point, msg (r<i ) |A ;3) the nonces and secret keys A has freshly generated atstage i. For a formal definition, see Appendix B. The set
PossIPo (r, A, i) consists of all messages the agent A can possibly construct after have seen the first i messages of therun.
Definition 5. A run r ∈ Run is said to be legitimate withrespect to an initial possession function IPo : AG → P(MSG)
if, for every i ∈ [0, |r|−1], mi ∈ PossIPo (r, A, i), where (Ai →Bi : mi ) = ri .
Definition 6. (Protocols and runs of protocol) A protocol
is a pair (cr, IPo) consisting of a set of candidate runs cr andan initial possession function IPo. A run r ∈ Run is said tobe a run of a protocol (cr, IPo) if r ∈ cr and is legitimate
with respect to the initial possession function IPo. The setof runs of a protocol (cr, IPo) is denoted by Runcr,IPo .
Note that in the literature (e.g., [8]) a protocol is often
given locally, by specifying what kind of messages an agent
can send in a certain situation. For our theory, the way of
specifying a protocol is unimportant; therefore we abstractfrom this specification by considering a given set of candidate runs.

3.4

Observational equivalence

If an agent receives an encrypted message for which itdoes not have the decryption key, this message looks justlike a random bit string. This section formalizes this idea bydefining the notion of observational equivalence. Intuitively,
two sequences of messages look the same to an agent if they
are the same for the messages the agent understands andif a message in one sequence looks like a random bit string
to the agent, then the corresponding message in the othersequence also looks like a random bit string. Matters areslightly more complicated: we have to take care of the casewhere a specific random looking bit string occurs more thanonce in a sequence of messages; we have to take care of thepossibility for someone to understand only a submessage of amessage; we also have to take care of the case where certain
messages look like random bit strings to the agent, but are
still somehow related. For example, if the agent does notpossess the symmetric key K, two messages m1 = {|m|}K and
m2 = hash({|m|}K ) both look like random bit strings. Still
the agent can derive a relationship between them, namely
m2 = hash(m1 ).
This motivates our definition of observational equivalence
below. The definition is typically applied with U being equal
to PossIPo (r, A, |r| − 1), the set of messages that an agent A
possesses after the run has finished.
Definition 7. (Reinterpretations of messages) Let π be a
structure preserving permutation on the set MSG of messages and let U ⊆ MSG be a set of messages. The map π issaid to be a semi-reinterpretation under U if it satisfies thefollowing conditions:
π(p) = p

for primitive terms pπ({|m|}K ) = {|π(m)|}K

if m, K are in U , orπ(hash(m)) = hash(π(m))

if {|m|}K , K −1 are in U
if m is in U .

The map π is called a reinterpretation under U if it is a semireinterpretation under U and if π −1 is a semi-reinterpretation
under π(U ) as well.
The above definition says that as far as an agent can observe(i.e., for all the messages in U ), the permutation π preserves structural and cryptographic relationships between
messages. We extend reinterpretations naturally to events(applying π to the message field of an event) and to runs
(applying π to the message field of every event in a run).

This is due to the fact that π must satisfy π({|B, {|m|}B |}M ) ={|B, π({|m|}B )|}M (and similarly for m0 ). Note how this nicely
captures the fact that, from the viewpoint of the spy, themessages {|B, {|m|}B |}M and {|B, {|m0 |}B |}M can indeed bedistinguished: at the end of the run the spy possesses themessages {|m|}B and {|m0 |}B and he can simply encrypt themessages hB, {|m|}B i and hB, {|m0 |}B i with the public key of
M . This does not hold for the version with the nonces, since
the spy never possesses these nonces.

Lemma 1. Let U be a set of messages.
1. The identity map on the set of messages is a reinterpretation under U .

4.

2. For every reinterpretation π under U , its inverse π −1
is a reinterpretation under π(U ).

In this section we introduce the epistemic (or modal) language as our specification language. The semantics of epistemic operators is defined in a standard way [8], taking
the set Runcr,IPo of runs of a protocol as the set of possible
worlds equipped with observational equivalence ∼=A . Notethat our language is semantics-based : a formula is identified as a {T, F}-valued function over a model, rather thana syntactically-defined entity.

3. For all reinterpretations π under U and π 0 under π(U ),their composition π 0 ◦ π is a reinterpretation under U .
Proof. Trivial. Note that 3 is already true for semireinterpretations.
Definition 8. (Observational equivalence of runs) Let r, r 0∈ Runcr,IPo be two runs of a protocol (cr, IPo) and let A ∈ AG
be an agent. Two runs r and r0 are said to be observationallyequivalent for an agent A, denoted by r ∼=A r0 , if there
exists a reinterpretation π under PossIPo (r, A, |r| − 1) suchthat π(r|A ) = r0 |A . Such a reinterpretation will be calleda reinterpretation for A.
Lemma 2. For each agent A ∈ AG, the binary relation∼=A on Runcr,IPo is an equivalence relation.
Proof.
This follows immediatelyfrom Lemma 1.´ Note`´that π PossIPo (r, A, |r| − 1) = PossIPo (π(r), A, |r| − 1) sinceIPo(A) consists solely of primitive messages and since a reinterpretation does not change the sender and receiver fieldsof events.
Example 1. Consider the following two runs in which A
and A0 are sending the messages m and m0 to B via a single
relay, or Chaum mix, M . Below n and n0 are fresh nonces.
r
r0(A → M : {|n, B, {|m|}B |}M ) (A → M : {|n0 , B, {|m0 |}B |}M )(A0 → M : {|n0 , B, {|m0 |}B |}M ) (A0 → M : {|n, B, {|m|}B |}M )(M → B : {|m|}B )(M → B : {|m|}B )(M → B : {|m0 |}B )(M → B : {|m0 |}B )Assume that the spy knows the identities of all agents,
all public keys and also the private key of B. Then theseruns are still observationally equivalent for the spy; we cantake a reinterpretation that exchanges {|n, B, {|m|}B |}M and{|n0 , B, {|m0 |}B |}M and leaves {|m|}B and {|m0 |}B fixed. It is
important to realize that a reinterpretation π for the spy
must satisfy π({|m|}B ) = {|π(m)|}B (since B’s private key
is compromised), but does not necessarily have to satisfy
π({|n, B, {|m|}B |}M ) = {|n, B, π({|m|}B )|}M (and similarly form0 ).
Without the nonces, however, the runs are not observationally equivalent.
r
r0(A → M : {|B, {|m|}B |}M ) (A → M : {|B, {|m0 |}B |}M )(A0 → M : {|B, {|m0 |}B |}M ) (A0 → M : {|B, {|m|}B |}M )(M → B : {|m|}B )(M → B : {|m|}B )(M → B : {|m0 |}B )(M → B : {|m0 |}B )FORMULAS AND EPISTEMIC OPERATORS

4.1

FormulasWith a formula we want to express not only a fact abouta run but also that an agent knows/does not know a certain
fact about a run.
Definition 9. (Formulas) A formula ϕ is a function whichtakes as its arguments a protocol (cr, IPo) and a run r ∈Runcr,IPo of that protocol, and returns either T or F. The
set of all the formulas is denoted by Form. We follow thetradition of logic to denote the fact ϕ(cr, IPo, r) = T, wherer ∈ Runcr,IPo , by cr, IPo, r |= ϕ. Often the protocol (cr, IPo)under consideration is clear from the context, in which case
we abbreviate cr, IPo, r |= ϕ to r |= ϕ. Logical connectives
on formulas such as ∧, ∨, → and ¬ are defined in an obvious
way. A formula ϕ is said to be valid if cr, IPo, r |= ϕ for all
cr, IPo and r.
We will use the following abbreviations Sends, Possesses, andOriginates repeatedly in the rest of the paper. They express
fundamental properties of runs.
Definition 10. The formula A Sends m to B means: atsome stage in the run, A sends a message to B which contains m as a subterm.
r |= A Sends m to B

def

⇐⇒
`
´
∃i ∈ [0, |r| − 1]. m ¹ m0 where (A → B : m0 ) = ri .

We will also use A Sends m to mean that A sends the message m to someone.
r |= A Sends m

def

⇐⇒

∃B. A Sends m to B.

The formula A Possesses m means: after the run has finished, A is capable of constructing the message m.
r |= A Possesses m

def

⇐⇒

m ∈ PossIPo (r, A, |r| − 1).

The formula A Originates m means that: A Sends m, but
A is not relaying. More precisely, m does not appear as a

subterm of a message which A has received before.
r |=A Originates m

def

⇐⇒
“
∃i ∈ [0, |r| − 1]. ∃B. m ¹ m0 where (A → B : m0 ) = ri`´”
∧ ∀j ∈ [0, i − 1]. m 6¹ m̂ where (A0 → A : m̂) = rj .

4.2

Epistemic operators

Using the observation equivalence relations over over the
set Runcr,IPo of possible worlds defined in Section 3.4, we can
now introduce epistemic operators in the standard way (seee.g., [8]).
Definition 11. (Epistemic operators) Let (cr, IPo) be a
protocol. For an agent A ∈ AG, the epistemic operator
2A : Form → Form is defined by:
cr, IPo, r |=2A ϕ`r |= 2spy ¬(2A (A Possesses m)) .

def

The formula 2A ϕ is read as “after the run is completed, theagent A knows that ϕ is true”. The formula 3A ϕ is short for¬2A ¬ϕ and read as “after the run is completed, the agent
A suspects that ϕ is true”.
Lemma 3 (2A is the S5-modality). For each agent
A ∈ AG, the operator 2A satisfies the following properties.
• (Necessitation) For each set of candidate` runs cr andeach initial possession function IPo, if ∀r ∈ Runcr,IPo .
´`´r |= ϕ , then ∀r ∈ Runcr,IPo . r |= 2A ϕ .
• The following formulas are all valid: (Distribution)
2A (ϕ → ψ) → (2A ϕ → 2A ψ); (T) 2A ϕ → ϕ; (4)2A ϕ → 2A 2A ϕ; (5) 3A ϕ → 2A 3A ϕ.
In short, the operator 2A is so-called an S5-modality.
Proof. Since the epistemic operator 2A is defined via anequivalence relation ∼=A on Runcr,IPo . See e.g., [2].

Expressing information hiding properties

There are a number of properties which are referred to as
information hiding properties (see e.g., [15]), and a desired
property might be different from one application to another.
As stated in the introduction, we aim at, rather than a decisive definition of “anonymity”, a framework in which we
can formulate and analyze various different properties in a
uniform and straightforward manner.
In this subsection we formulate some common examples
of information hiding properties in our epistemic language.
We use the standard notion of an anonymity set: it is acollection of agents among which a given agent is not identifiable. The larger this set is, the more anonymous an agent
is.
Sender anonymity Suppose that r is a run of a protocol
in which an agent B receives a message m. We say thatr provides sender anonymity with anonymity set AS if itsatisfies^r |=3B (X Originates m).
X∈AS

This means that, as far as B is concerned, every agent in
the anonymity set could have sent the message.

X∈AS´
where ϕ0 (X, Y ) = ∃n. X Sends n ∧ Y Possesses n . Intuitively, the left side of the conjunction means that theadversary is not certain that A sent something to B. The
right side means that every other user could have sent something to B. Similarly, unlinkability between a user A anda message m could be defined as |= ¬2spy (A Sends m) ∧V
X∈AS 3spy (X Sends m).
Plausible deniability In certain circumstances (e.g., relays), agents might be interested in showing that they did
not know that they had some sensitive information m. Thismight be modelled by the following epistemic formula:

⇐⇒

`
´
0
∀r0 ∈ Runcr,IPo . r0 ∼=A r =⇒ cr, IPo, r |= ϕ .

4.3

Unlinkability We say that a run r provides unlinkability
for users A and B with anonymity set AS if^`´
r |= ¬2spy ϕ0 (A, B) ∧3spy ϕ0 (X, B) ,This formula is read as: the spy knows that A does not knowthat she possesses m.

5.

EXAMPLES

To illustrate the applicability of the theory, we analyze theanonymity of simplified versions of Crowds and Onion Routing. For Crowds, we focus on proving sender anonymity,
whereas for Onion Routing we are concerned with unlinkability.
Before starting, we need a convenient way of specifying thecandidate runs of the various protocols we will be considering. We describe them with the following inference stylerules:
e1 , . . . , ene1 , . . . , en
[c]
[c]
e
e
The first of these rules means that, under the side conditionc, if a run contains events e1 , . . . , en , then later the event e
may appear in the run. For the second it means that e must
appear later in the run.
For example, in a simple version of Chaum mixes, thefollowing rule would describe the action of a router:(X → M : {|Y, m|}M )(M → Y : m)

[X, Y, M pairwise distinct, M router]In normal language this means that if X sends the message{|Y, m|}M to M , then M must forward the message m to Y .
The side condition says that this only applies if X, Y and
M are three distinct agents and if M has been designatedas a router.
Note that this way of specifying runs of a protocol is no
integral part of the theory; it only serves as a convenient
way of presenting the protocols (or, more accurately, thecandidate runs) in the examples in the remainder of thissection.

5.1

CrowdsThe Crowds system [16] is a system for doing anonymous
web transactions based on the idea that anonymity can beprovided by hiding in a crowd. When someone wants tosend a request to a server, she randomly selects a user froma crowd of users and asks this user to forward the request forher to the server. This user then either forwards the request
to the server, or selects another random user from the crowd

to do the forwarding. (Note: this only describes the request
part; not the reply part). For simplicity reasons, we model
requests as nonces.
Schematically, we can model this as follows:(A → R : hS, ni)(A → R : hS, ni)

A QQQ((◦))A(◦) mm6 B
QQQ
m
(
mmm
M
Q
6
QQQ
nnn
QQ(
nnn((•))
(•)
0
0

B

A QQQ((◦))A(•) mm6 B
QQQ
m
(
mmm
M
Q
6
QQQ
nnn
QQ(
nnn((•))
(◦)
0
0

B

(R → S : n) or (R → R0 : hS, ni)This obviously provides sender anonymity, in the sense thatthe server cannot tell from who the request really originated.
In the formal framework this can be formulated as follows:
Theorem 1. Let r be a run of Crowds in which (A → S :n) occurs with A 6= S. Then^r |=3S (B Originates n),B∈AS

where the anonymity set AS is equal to AG \ {S}.
Proof. Let B ∈ AS and take r0 = (B → A : n), r, i.e.,
r augmented by a fictitious event (B → A : n). Then r0 is
also a valid run and obviously r0 |= B Originates n. Because
S 6= A, B, we have r0 |S = r|S and therefore r0 ∼=S r. Sor |= 3S (B Originates n).
Against a global eavesdropper, i.e., someone who can observe all network traffic, this does not provide anonymity.
This is, of course, also remarked in [16].
Theorem 2. Let r be a run of Crowds in which A freshly
sends n to S over a relay R. I.e., the run contains(A → R : hS, ni)
and the nonce n is fresh in A → R : hS, ni. Then r |=2spy (A Originates n).
Proof. Suppose that r |= ¬2spy (A Originates n). Then
there is a run r0 satisfying r ∼=spy r0 where the formula r0 |=¬(A Originates n) holds. Let π be the reinterpretation for
spy such that π(r) = r0 . Note that π(n) = n and π(S) = S.
Since A did not originate n in r0 , there must be an event
B → A : m with n as subterm appearing in m before theevent A → R : hS, ni. This message m must be of the formn or of the form hC, ni for some agent C, since the protocol
does not allow the sending of messages of any other formand since it must have n as subterm. However, this meansthat B → A : π −1 (m) occurs in r before A → R : hS, ni.
Note that π −1 (m) is of the form π −1 (n) = n or of the form
π −1 (hC, ni) = hC, ni for some agent C. This contradicts thefact that n appears freshly in the event A → R : hS, ni.

5.2

Similar run r0

Actual run r

Onion Routing

Chaum mixes were already mentioned in the introduction.
Users construct messages of the form {|R2 , {|B, {|m|}B |}R2 |}R1
(called onions, because of the layered encryptions) and use
relays (R1 , R2 ) that decrypt one layer (peel the onion) andforward the remainder. In this section we analyze the unlinkability of a very simple version.
An agent in the set AG belongs to one of the following
families: 1) Onion routers who try to disguise causal relations between incoming and outgoing messages by peelingonions (i.e., removing one layer of encryption) and forwarding them.
The router collects incoming messages until it has received
k messages. Then, the messages are permuted and sent in

Figure 1: Onion Routing
batch to their respective intended destinations. 2) Users
who try to communicate with one another unlinkably, withthe help of the onion router. 3) The intruder denoted byspy.
In the sequel we assume that there is only a single routerdenoted by M . and furthermore the initial possession function IPo is such that, for each agent X, IPo(X) consists ofthe private key of X and the public keys of all agents. For
now, no agent is corrupt, so also spy does not possess any
private keys other than his own.
Again we specify the candidate runs of the protocol in theform of inference rules. The first rule says that every user
X can initiate sending a message n to another user Y bybuilding an onion and submitting it to the router M . The
second says that users may also send random messages tothe router M , padding the network with dummy messages.
These messages will be ignored by the router; they only
serve to obscure the relation between incoming and outgoingmessages if not enough real traffic is available.
»–
X, Y, M pairwise distinct
n0 , n fresh(X → M : {|n0 , Y, {|n|}Y |}M )(X → M : {|n|}M )[n fresh]

The last one is(Xi → M : {|ni , Yi , mi |}M ),(Xj → M : {|nj |}M )(M → Yi : mi )3
Xi , X j , Y i , M
6 pairwise distinct 77654
i = 1...lj = l + 1...k
2

It means that when the router has received l onions andk − l padding messages, it “peels” the onions and forwards
the messages to the intended recipients. Note that l is a freevariable and can be instantiated by any value 1 ≤ l ≤ k,whereas k is a constant. Also note that this inference ruleposes no condition on the ordering of the messages. Now
we investigate under what condition onion routing ensuresunlinkability, that is, which V
runs r of onion routing makethe formula ¬2spy ϕ0 (A, B) ∧ X∈AS 3spy ϕ0 (X, B) true. Re`
member that we abbreviate the formula ∃n. X Sends n ∧´
Y Possesses n to ϕ0 (X, Y ).
Example 2. Consider a run r in which a user A is sendinga message to a user B via the router M . Intuitively, unlinkability of A and B is ensured by showing that there isanother run r0 that looks similar to r (i.e., is observationally equivalent to r), but in which another user A0 is actually communicating with B (and A is communicating withsomeone else, B 0 ). This situation is illustrated in Figure 1.
There ((◦)) represents a two-layered onion {|n0 , B, {|n|}B |}M .
When peeled the resulting one-layered onion is denoted by(◦). ((•)) is a two-layered onion with another nonce in its
core.
The following theorem gives a necessary condition for arun of Onion Routing to provide unlinkability. It says that
if a user A sends a message to B via the router M , thenevery user has to send a message to the router M to provide
unlinkability of A and B.
Theorem 3. Let r be a run of Onion Routing which contains the events
e1 = (A → M : {|n0 , B, {|n|}B |}M ) ,e2 = (M → B : {|n|}B )V
in this order. If r |= ¬2spy ϕ0 (A, B) ∧ X∈AS 3spy ϕ0 (X, B),then r contains before e2 , for every user X, an event of theform (X → M : {|m|}M ) for some message m.
Proof. Suppose we have a run r such that^r |= ¬2spy ϕ0 (A, B) ∧3spy ϕ0 (X, B).
X∈ASV

Then r |= X∈AS 3spy ϕ0 (X, B). Now take X ∈ AS. Thenr |= 3spy ϕ0 (X, B), which means that there is a run r0 withr0 ∼=spy r such that r0 |= ϕ0 (X, B). Hence r0 |= X Sends mfor some message m. Hence, r0 should contain an event e ofthe form (X → M : {|m0 |}M ), with m ¹ m0 , given the inference rule for X (users can only send encrypted messages toM ). Then, r must contain an event π −1 (e0 ), which finishes
the proof.
Now we give a sufficient condition for unlinkability. It saysthat if there are enough messages in the network, then A
and B cannot be linked.
Theorem 4. Let r be a run of Onion Routing which contain eventse = (A → M : {|n0 , B, {|n|}B |}M ) , e0 = (M → B : {|n|}B )in this order. Then, thereVexist an anonymity set AS suchthat r |= ¬2spy ϕ0 (A, B) ∧ X∈AS 3spy ϕ0 (X, B), with |AS| ≥k. Recall that k is the size of the router’s queue.
Proof. We first prove the left hand side of the conjunction. That is, we want to prove that r |= ¬2spy ϕ0 (A, B).
This means that there should be a run r0 with r0 ∼=spy rsuch that r0 |= ¬ϕ0 (A, B). Let e1 . . . eq be all the messages in r originated by A which have B as final destination, i.e., each ei has the form ei = (A → M : mi ) wheremi = {|n̂i , B, {|ni |}B |}M . To keep the notation easy, we only
consider the case where q = 1; the general case goes analogously.
By the inference rule of the router, r contains, k events
e0j = (Xj → M : {|mj |}M ), j = 1 . . . k, one of which ise1 . These are the messages that the router M received in
the same batch as e1 . Choose one of the events e0 j that isdifferent from e1 and define a reinterpretation π such thatπ(m0 j ) = m1 , π(m1 ) = m0 j , extending it in a natural way
to the rest of the domain. Now r0 = π(r) is a run of the protocol (because the router processes messages in batches).
Moreover, by the inference rule of the router, the final destinations of e0 j , j = 1 . . . k are pairwise distinct and therefore
B 6¹ π(mi ). This implies r0 6|= ϕ0 (A, B).
Now we are going to prove the right side of the conjunction. Given that e0 is in r, by the inference rule, there

must be k events ei = (Xi → M : mi ) with i = 1 . . . k
in r. Moreover, one of these events must be e, say ej . Take
AS = {Xi | i = 1 . . . k}. Note that V|AS| = k, since theXi are all distinct. To show that r |= X∈AS 3spy ϕ0 (X, B)
part it suffices to show that for a fixed Xi , there is a run
r0 = π(r) such that r0 |= ϕ0 (Xi , B). Now take π such that
π(mi ) = mj , π(mj ) = mi , and the obvious extension to therest of the domain. As before, r0 is a run of the protocol
and r0 |= ϕ0 (Xi , B).
Finally, let us consider the case where the private key of the−1router is compromised, i.e., IPo(spy) now contains KM. In
this case it is easy to see that unlinkability always fails.
Theorem 5. For any run r run of Onion Routing whichcontains the events
e1 = (A → M : {|n0 , B, {|n|}B |}M ) ,e2 = (M → B : {|n|}B )in this order, unlinkability fails. That is, r |= 2spy ϕ0 (A, B).
Proof. Let r0 be a run such that r0 ∼=spy r. Say π is a−1
reinterpretation for spy such that π(r) = r0 . Since KM∈
IPo(spy), we have π({|n0 , B, {|n|}B |}M ) = {|n0 , B, π({|n|}B )|}M .
Because r0 is a valid run of onion routing, π({|n|}B ) = {|n0 |}B
for some nonce n0 . Then r0 |= A Sends n0 ∧ B Possesses n0 ,and therefore r0 |= ϕ0 (A, B).

5.3

Onion Routing with subtle flaw

We now propose a version of Onion Routing that has asubtle error, and then show that unlinkability fails. As far
as we are aware, this is the first framework that detects thiskind of subtle flaws.
Imagine a modified version of Onion Routing where eachchannel in each path is assigned a nonce as an identifier(maybe for establishing a bi-directional communication).
These nonces are reused every time that a message is sent
through this channel.
The following he0 , e1 , . . . , e7 i is an example of a run:e0 = (A → M : hn11 , ((n))i) e4 = (A → M : hn11 , ((n00 ))i)e1 = (B → M : hn21 , ((n0 ))i) e5 = (B → M : hn31 , ((n000 ))i)e2 = (M → C : hn12 , (n)i)
e6 = (M → C : hn12 , (n00 )i)0e3 = (M → C : hn22 , (n )i) e7 = (M → E : hn32 , (n000 )i)
where ((−)) or (−) denotes an onion like in Section 5.2,
whose ultimate destination is clear from the way it is relayed. In e2 , M generates a nonce (an identifier) n12 andremembers the correspondence between n11 and n12 . WhenM relays another onion which comes with the same identifier n11 (in e4 ), it includes the corresponding nonce n12 (ine6 ). B uses a new identifier n31 in e5 because the destinationof the onion is different from e1 . From C’s point of view,
since the nonces n and n00 come with the same identifier n12 ,they are from the same originator. Nevertheless the actual
originator A is disguised to C.
Notice that both runs he0 , . . . , e3 i and he4 , . . . , e7 i ensure
unlinkability in themselves. However, when combined, inthe run he0 , . . . , e7 i the users A and C are linkable, but only
because the combination of identifiers n11 and n12 occurs
twice in the run.
In the following we put this flaw formally. The candidate runs for Flawed Onion Routing should be clear fromthe above example. A user can originate an onion with an
identifier, and the router M relays a peeled onion with asuitable identifier. The identifiers are either freshly generated or reused in the way illustrated in the above example.

In general, to attain unlinkability from A to B, there must
be another fixed user C who immediately imitates the behavior of A: if A sends an onion bound for B, before theonion is relayed, C must send an onion bound for fixed a
D. This condition is fairly unrealistic. The following theorem formally put this (unrealistic) necessary condition for
unlinkability, for the case where A sends two onions.
Theorem 6. Let r be a run of Flawed Onion Routing
which contains the events
e1

=

e2
e3

= (M → B : hnM , {|n|}B i),= (A → M : hnA , {|n00 , B, {|n0 |}B |}M i),(A → M : hnA , {|n0 , B, {|n|}B |}M i),e4=(M → B : hnM , {|n0 |}B i)in this order. If r |= ¬2spy ϕ0 (A, B) then, r contains before e2 and e4 , events (X → M : hnX , m1 i) and (X →M : hnX , m2 i) respectively, for some user X 6= A, messages
m1 , m2 .
Proof. Suppose we have a run r such thatr |= ¬2spy ϕ0 (A, B),
which means that there is a run r0 such that r0 ∼=spy r and
r0 |= ¬ϕ0 (A, B). Let π be a reinterpretation for spy suchthat π(r) = r0 . By Definition 7, r0 must contain events e02 =π(e2 ) = (M → B : hnM , π({|n|}B )i) and e04 = π(e4 ) = (M →B : hnM , π({|n0 |}B )i). Therefore, by the inference rule as tocorrespondence of identifiers, r0 must contain events e01 ande03 of the form e01 = (X → M : hnX , π({|n0 , B, {|n|}B |}M )i)and e03 = (X → M : hnX , π({|n00 , B, {|n0 |}B |}M )i), for somecommon sender X. Now r0 |= ¬ϕ0 (A, B) implies X 6= A,
which finishes the proof.

6.

CONCLUSIONS AND FUTURE WORK

We have presented a framework for verifying a variety
of information hiding properties, using modal logic. This
framework provides a well defined epistemic language where
various competing information hiding properties can be expressed and verified uniformly at semantical level. Our finegrained definition of message reinterpretation captures subtleties that would not be captured in other state of the art
frameworks.
Several extensions of our framework still remain. An obvious one is the consideration of a stronger adversarial model(e.g., active corrupt agents, Dolev-Yao), which should arise
straightforwardly. It would also be interesting to consider
applications to other fields like secure multiparty computation, and to other security properties besides information
hiding, such as secrecy. From a practical perspective, proofs
are slightly complicated, even with small examples. Therefore, having a tool which can perform this proofs in an automatic or semi-automatic fashion, would significantly improve the usability of the framework.

7.

REFERENCES[1] M. Abadi and P. Rogaway. Reconciling two views ofcryptography (the computational soundness of formal
encryption). Journal of Cryptology, 15(2):103–127,
2002.
[2] P. Blackburn, M. de Rijke, and Y. Venema. Modal
Logic. Number 53 in Cambridge Tracts in TheoreticalComputer Science. Cambridge University Press, 2001.

[3] D. L. Chaum. Untraceable electronic mail, return
addresses, and digital pseudonyms. Communicationsof the ACM, 24(2):84–88, 1981.
[4] I. Clarke, O. Sandberg, B. Wiley, and T. W. Hong.
Freenet: A distributed anonymous information storage
and retrieval system. In Proceedings of Designing
Privacy Enhancing Technologies: Workshop on Design
Issues in Anonymity and Unobservability, pages
46–66, July 2000.
[5] G. Danezis, R. Dingledine, and N. Mathewson.
Mixminion: Design of a type III anonymous remailer
protocol. In Proceedings of the 2003 IEEE Symposium
on Security and Privacy, pages 2–15, May 2003.
[6] R. Dingledine, N. Mathewson, and P. Syverson. Tor:
The second-generation onion router. In Proceedings ofthe 13th USENIX Security Symposium, pages 303–320,
Aug. 2004.
[7] D. Dolev and A. Yao. On the security of public key
protocols. IEEE Transactions on Information Theory,29(2):198–208, 1983.
[8] R. Fagin, J. Halpern, Y. Moses, and M. Vardi.
Reasoning About Knowledge. MIT Press, Cambridge,
MA, 1995.
[9] D. M. Goldschlag, M. G. Reed, and P. F. Syverson.
Hiding Routing Information. In R. Anderson, editor,
Proceedings of Information Hiding: First International
Workshop, volume 1174 of Lecture Notes in Computer
Science, pages 137–150. Springer-Verlag, May 1996.
[10] J. Guttman. Key compromise, strand spaces, and theauthentication tests. In Mathematical Foundations ofProgramming Semantics 17, volume 47 of Electronic
Notes in Theoretical Computer Science, pages 1–21.
Elsevier, Amsterdam, 2001.
[11] J. Halpern and K. O’Neill. Anonymity andinformation hiding in multiagent systems. In 16th
IEEE Computer Security Foundations Workshop(CSFW ’03), pages 75–88, 2003.
[12] B. Jacobs. Semantics and logic for security protocols.
Preprint, 2004.
[13] S. Mauw, J. Verschuren, and E. de Vink. A
formalization of anonymity and onion routing. In
Esorics 2004, volume 3193 of Lecture Notes in
Computer Science, pages 109–124, Sophia Antipolis,
2004.
[14] L. Paulson. The inductive approach to verifying
cryptographic protocols. Journal of Computer
Security, 6:85–128, 1998.
[15] A. Pfitzmann and M. Köhntopp. Anonymity,
unobservability, and pseudonymity: A consolidated
proposal for terminology. Draft, version 0.22, July
2000.
[16] M. Reiter and A. Rubin. Crowds: Anonymity for web
transactions. ACM Transactions on Information and
System Security, 1(1):66–92, 1998.
[17] A. Serjantov. On the Anonymity of Anonymity
Systems. PhD thesis, University of Cambridge, Mar.
2004.
[18] V. Shmatikov. Probabilistic model checking of ananonymity system. Journal of Computer Security,
12(3):355–377, 2004.

APPENDIX

For the intruder spy,A.

PossIPo (r, spy, 0) = IPo(spy) ,PossIPo (r, spy, i + 1) =8><{v ∈ FreshIPo (r, i) | v ¹ mi } ∪ PossIPo (r, spy, i)
if Ai = spy, (∗)>:{m } ∪ Poss (r, spy, i)otherwise.
i
IPo

CLOSUREFor the formal definition of the closure U of a set U of
messages, we use two functions analz, synth : P(MSG) →P(MSG) which are defined much like in [14]. The analyzing
function analz extends the input set by adding all the subterms obtained via decryption and decomposing tuples. For
example if K is a symmetric key, we have“˘¯”analz K, {|hA, hash(n)i|}K=
˘¯
K, {|hA, hash(n)i|}K , hA, hash(n)i, A, hash(n) .
Note that the nonce n is not included in the output. The
synthesizing function synth outputs the set of messages which
can be constructed by encryption and tupling using messages in the input set. For example if both m and the key
K are in U , then {|m|}K is in synth(U ).
Definition 12. (Analyze and synthesize) Let U be a setof messages. The analysis of U , notation analz(U ), is thesmallest set of messages satisfying
1. U ⊆ analz(U );2. if {|m|}K , K −1 ∈ analz(U ), then m ∈ analz(U );3. if hm1 , m2 i ∈ analz(U ), then m1 , m2 ∈ analz(U ).
Similarly, the synthesis of U , notation synth(U ), is the smallest set of messages satisfying
1. U ⊆ synth(U );2. if m, K ∈ synth(U ), then {|m|}K ∈ synth(U );3. if m ∈ synth(U ), then hash(m) ∈ synth(U );4. if m1 , m2 ∈ synth(U ), then hm1 , m2 i ∈ synth(U ).
Definition 13. (Closure) Let U be a set of messages. The
set synth(analz(U )) is called the closure of U and is denotedby U .
Theorem 7. The operator U 7→ U is indeed a closure
operator. That is, for any U, V ∈ MSG: U ⊆ U , U = U ,and U ⊆ V =⇒ U ⊆ V .

B.

POSSESSED MESSAGESDefinition 14. (Fresh nonces/keys) A nonce or key is said
to be fresh for an initial possession function IPo, a run r andi ∈ [0, |r| − 1], if it (and its inverse, in the case of a key) does
not occur in r<i nor in the initial possession IPo(A) of any
agent A. The set of fresh nonces and keys for IPo, r, i isdenoted by FreshIPo (r, i).
Definition 15. (Possessed messages) Let IPo : AG →P(MSG) be a initial possession function, r a run, A an agent
and i ∈ [0, |r|−1]. The set of possessed messages for IPo, r, A
at stage i, denoted by PossIPo (r, A, i), is defined inductively
on i. For every i, let ri be (Ai → Bi : mi ). For a regularagent A ∈ AG \ {spy},
PossIPo (r, A, 0) = IPo(A) ,PossIPo (r, A, i + 1) =8{v ∈ FreshIPo (r, i) | v ¹ mi } ∪ PossIPo (r, A, i)>>><
if Ai = A, (∗)>{mi } ∪ PossIPo (r, A, i)
if Bi = A,>>:
PossIPo (r, A, i)otherwise.

This definition says that if fresh nonces/keys occur as subterms in a sent message (i.e., if the sender freshly generates
nonces/keys), then these generated terms are added to thesender’s possessed messages. This complicated definition
can be understood with the following example. If an agent A
sends at stage i the public-key encryption {|n|}B of a freshly
generated nonce n, A is supposed to possess the nonce n(that A has generated herself) from then on. However, without the above clause (∗), when A does not possess the private
key, the nonce n would not be in PossIPo (r, A, i + 1).
When an agent sees a message (whether as the receiver oras an eavesdropper), the message is added to the ingredientsthe agent can use to construct messages. For example, if anagent receives at stage i an encryption of a nonce {|n|}K
which the agent cannot decrypt at that time, and later atstage j(> i) the agent receives the decryption key K −1 ,then from stage j + 1 on the agent can use the nonce n to
construct messages it sends.
The definition for spy differs from that for a regular agent
because spy is a global eavesdropper and hence sees every
message in the network.