AnoA-Analyzing Anonymous Communication Protocols.pdf

AnoA:AFrameworkForAnalyzing

AnonymousCommunicationProtocols

Unied Denitions and Analyses of Anonymity Properties

Michael Backes 1;2

Aniket Kate 3

Praveen Manoharan 1

Sebastian Meiser 1

Esfandiar Mohammadi 1

1 Saarland University, 2 MPI-SWS, 3 MMCI, Saarland University

{backes,manoharan,meiser,mohammadi}@cs.uni-saarland.de

aniket@mmci.uni-saarland.de

February 6, 2014

Abstract

Protecting individuals' privacy in online communications has become a challenge of paramount

importance. To this end, anonymous communication (AC) protocols such as the widely used

Tor network have been designed to provide anonymity to their participating users. While AC

protocols have been the subject of several security and anonymity analyses in the last years, there

still does not exist a framework for analyzing complex systems such as Tor and their dierent

anonymity properties in a unied manner.

In this work we presentAnoA: a generic framework for dening, analyzing, and quantifying

anonymity properties for AC protocols.AnoArelies on a novel relaxation of the notion of

(computational) dierential privacy, and thereby enables a unied quantitative analysis of well-

established anonymity properties, such as sender anonymity, sender unlinkability, and relationship

anonymity. While an anonymity analysis inAnoAcan be conducted in a purely information

theoretical manner, we show that the protocol's anonymity properties established inAnoA

carry over to secure cryptographic instantiations of the protocol. We exemplify the applicability

ofAnoAfor analyzing real-life systems by conducting a thorough analysis of the anonymity

properties provided by the Tor network against passive adversarys. Our analysis signicantly

improves on known anonymity results from the literature.

Note on this version Compared to the CSF version [BKM + 13], this version enhances theAnoAframework

by making the anonymity denitions as well as the corresponding privacy gamesadaptive. It also introduces the

concept ofadversaryclassesfor restricting the capabilities of adversaries to model realistic attack scenarios.

Contents

Introduction

5.3.3

Examples for adversary

classes . . . . . . . . . . . .

1.1

Contributions . . . . . . . . . . . .

Leveraging UC realizability

Notation

6.1

The UC framework . . . . . . . . .

TheAnoAFramework

6.2

Preservation of -IND-CDP. . .

3.1

Protocol model . . . . . . . . . . .

Analyzing Tor Anonymity

3.2

Generalized computational dier-

ential privacy . . . . . . . . . . . .

7.1

Tor | the OR network

. . . . . .

7.2

Anonymity analysis . . . . . . . . .

3.3

Anonymity properties

. . . . . . .

7.3

Anonymity quantication

. . . . .

3.3.1

Sender anonymity

. . . . .

7.3.1

Distinguishing events . . . .

3.3.2

The value of " . . . . . . .

7.4

System-level attacks and adaptations 27

7.4.1

3.3.3

Sender unlinkability

. . . .

Trac analysis attacks . . .

3.3.4

Relationship anonymity

. .

7.4.2

Entry guards

. . . . . . . .

Studying

our

Anonymity

Deni-

7.5

Link corruption . . . . . . . . . . .

tions

Related Work

4.1

Sender anonymity

. . . . . . . . .

4.2

Unlinkability

. . . . . . . . . . . .

Conclusion and Future Directions

4.3

Relationship anonymity

. . . . . .

4.4

Relations between anonymity no-

tions . . . . . . . . . . . . . . . . .

A Framework

A.1

Expressivity . . . . . . . . . . . . .

A.2

Relations among the various notions 41

AdaptiveAnoA 15

5.1

A.3

Leveraging UC

. . . . . . . . . . .

Dening adaptive adversaries

. . .

A.4

Composability theorem

. . . . . .

5.1.1

Adaptive anonymity notions 17

5.2

Adversary classes . . . . . . . . . .

B Abstracting Tor in UC

5.3

Sequentially

composable

adver-

B.1

System and adversary model

. . .

sary classes

. . . . . . . . . . . . .

B.2

Ideal functionality

. . . . . . . . .

5.3.1

Requirements for compos-

ability . . . . . . . . . . . .

C Tor

5.3.2

Sequential composability

theorem for adversary classes 21

C.1

Formal Analysis . . . . . . . . . . .

C.2

Link Corruption

. . . . . . . . . .

Introduction

Protecting individuals' privacy in online communications has become a challenge of paramount

importance. A wide variety of privacy enhancing technologies, comprising many dierent approaches,

have been proposed to solve this problem. Privacy enhancing technologies, such as anonymous

communication (AC) protocols, seek to protect users' privacy by anonymizing their communication

over the Internet. Employing AC protocols has become increasingly popular over the last decade.

This popularity is exemplied by the success of the Tor network [Tor03].

There has been a substantial amount of previous work [STRL00, DSCP02, SD02, Shm04,

MVdV04, HO05, SW06, D06, FJS07a, FJS07b, GTD + 08, APSVR11, FJS12] on analyzing the

anonymity provided by various AC protocols such as dining cryptographers network (DC-net) [Cha88],

Crowds [RR98], mix network (Mixnet) [Cha81], and onion routing (e.g., Tor) [RSG98]. However,

most of the previous works only consider a single anonymity property for a particular AC protocol

under a specic adversary scenario. Previous frameworks such as [HS04] only guarantee anonymity

for a symbolic abstraction of the AC, not for its cryptographic realization. Moreover, while some

existing works like [FJS12] consider an adversary with access to a priori probabilities for the behavior

of users, there is still no work that is capable of dealing with an adversary that has arbitrary auxiliary

information about user behavior.

Prior to this work, there is no framework that is both expressive enough to unify and compare

relevant anonymity notions (such as sender anonymity, sender unlinkability, and relationship

anonymity), and that is also well suited for analyzing complex cryptographic protocols.

1.1

Contributions

In this work, we make four contributions to the eld of anonymity analysis.

As a rst contribution, we present the novel anonymity analysis frameworkAnoA. InAnoA

we dene and analyze anonymity properties of AC protocols. Our anonymity denition is based

on a novel generalization of dierential privacy, a notion for privacy preserving computation that

has been introduced by Dwork et al. [Dwo06, DMNS06]. The strength of dierential privacy

resides in a strong adversary that has maximal control over two adjacent settings that it has

to distinguish. However, applying dierential privacy to AC protocols seems impossible. While

dierential privacy does not allow for leakage of (potentially private) data, AC protocols inherently

leak to the recipient the data that a sender sends to this recipient. We overcome this contradiction

by generalizing the adjacency of settings between which an adversary has to distinguish. We

introduce an explicit adjacency function that characterizes whether two settings are considered

adjacent or not. In contrast to previous work on anonymity properties, this generalization of

dierential privacy, which we name -IND-CDP, is based on IND-CDP [MPRV09] and allows

the formulation of anonymity properties in which the adversary can choose the messages|which

results in a strong adversary|as long as the adjacent challenge inputs carry the same messages.

Moreover,AnoAis compatible with simulation-based composability frameworks, such as UC [Can01],

IITM [KT13], or RSIM [BPW07]. In particular, for all protocols that are securely abstracted by

an ideal functionality [Wik04, CL05, DG09, KG10, BGKM12], our denitions allow an analysis of

these protocols in a purely information theoretical manner.

As a second contribution, we formalize the well-established notions of sender anonymity, (sender)

unlinkability, and relationship anonymity in our framework, by introducing appropriate adjacency

functions. We discuss why our anonymity denitions accurately capture these notions, and show for

sender anonymity and (sender) unlinkability that our denition is equivalent to the denitions from

the literature. For relationship anonymity, we argue that previous formalizations captured recipient

anonymity rather than relationship anonymity, and we discuss the accuracy of our formalization.

Moreover, we show relations between our formalizations of sender anonymity, (sender) unlinkability,

and relationship anonymity: sender anonymity implies both (sender) unlinkability and relationship

anonymity, but is not implied by either of them.

As a third contribution, we extend our denitions by strengthening the adversary and improving

the exibility of our framework. We strengthen the adversary by introducing an adaptive challenger

and adaptive anonymity notions for our privacy games. In many real-world scenarios an adversary

has less control over individual protocol participants. We improve the exibility ofAnoAby

introducing so-called adversary classes that allow such a ne-grained specication of the inuence

that the adversary has on a scenario. Even though, in general, adversary classes are not sequentially

composable for adaptive adversaries, we identify a property that suces for proving sequential

composability.

Finally, as a fourth contribution, we apply our framework to the most successful AC protocol|

Tor. We leverage previous results that securely abstract Tor as an ideal functionality (in the UC

framework) [BGKM12]. Then, we illustrate that proving sender anonymity, sender unlinkability,

and relationship anonymity against passive adversaries boils down to a combinatoric analysis, purely

based on the number of corrupted nodes in the network. We further leverage our framework and

analyze the eect of a known countermeasure for Tor's high sensitivity to compromised nodes: the

entry guards mechanism. We discuss that, depending on the scenario, using entry guards can have

positive or negative eect.

Outline of the Paper. In Section 2 we introduce the notation used throughout the paper.

Section 3 presents our anonymity analysis frameworkAnoAand introduces the formalizations of

sender anonymity, unlinkability, and relationship anonymity notions in the framework. Section 4

compares our anonymity notions with those from the literature as well as with each other. In

Section 5 we extend the denitions with adaptively chosen inputs and with adversary classes. In

Section 6, we demonstrate compatibility ofAnoAwith a simulation-based composability framework

(in particular, the UC framework), and, in Section 7, we leverage our framework for proving of the

anonymity guarantees the Tor network. In Section 8, we discuss and compare related work with our

framework. Finally, we conclude and discuss some further interesting directions in Section 9.

Notation

Before we presentAnoA, we briey introduce some of the notation used throughout the paper. We

dierentiate between two dierent kinds of assignments: a := b denotes a being assigned the value b,

and a denotes that a value is drawn from the distribution and a is assigned the outcome. In

a similar fashion i R I denotes that i is drawn uniformly at random from the set I.

Probabilities are given over a probability space which is explicitly stated unless it is clear from

context. For example Pr[b = 1 : b R f0; 1g] denotes the probability of the event b = 1 in the

probability space where b is chosen uniformly at random from the set f0; 1g.

Our security notion is based on interacting Turing Machines (TM). We use an oracle-notation for

describing the interaction between an adversary and a challenger:

A B denotes the interaction of TM

A with TM B where A has oracle access to B. Whenever A activates B again, B will continue its

computation on the new input, using its previously stored state.

with

another input value, and B will continue its computation with the new input, using its previously

stored state. This interaction continues until A returns an output, which is considered the output

of A B .

can then again activate

In this paper we focus on computational security, i.e. all machines are computationally bounded.

More formally, we consider probabilistic, polynomial time (PPT) TMs, which we denote with PPT

whenever required.

TheAnoAFramework

In this section, we present theAnoAframework and our formulations of sender anonymity, sender

unlinkability, and relationship anonymity (Section 3.3). These formulations are based on a novel

generalization of dierential privacy that we describe in Section 3.2. Before we introduce this notion,

we rst describe the underlying protocol model. Using our protocol model, AC protocols are closely

related to mechanisms that process databases, a fact that enables us to apply a more exible form

of dierential privacy.

3.1

Protocol model

Anonymous communication (AC) protocols are distributed protocols that enable multiple users to

anonymously communicate with multiple recipients. Formally, an AC protocol is an interactive

Turing machine. 1

and an auxiliary

information spaceAux. Users' actions are modeled as an input to the protocol and represented

in the form of an ordered input table. Each row in the input table contains a user u 2 U that

performs some action, combined with a list of possible recipients r i

We associate a protocol with a user space

, a recipient space

2R together with some auxiliary

informationaux. The meaning ofauxdepends on the nature of the AC protocol. Based on the AC

protocol, auxiliary information can specify the content of a message that is sent to a recipient or

may contain a symbolic description of user behavior. We can think of the rows in the input table as

a list of successive input to the protocol.

Denition 1 (Input tables). An input table D of size t over a user space U, a recipient space

and an auxiliary information spaceAuxis an ordered table D = (d 1 ;d 2 ;:::;d t ) of tuples d j =

(u j ; (r j i ;aux j i ) i=1 ), where u j 2U;r j i

2R andaux j i

2Aux.

A typical adversary in an AC protocol can compromise a certain number of parties. We model

such an adversary capability as static corruption: before the protocol execution starts A may decide

which parties to compromise.

Our protocol model is generic enough to capture multi-party protocols in classical simulation-

based composability frameworks, such as the UC [Can01], the IITM [KT13] or the RSIM [BPW07]

framework. In particular, our protocol model comprises ideal functionalities, trusted machines that

are used in simulation-based composability frameworks to dene security. It is straightforward to

construct a wrapper for such an ideal functionality of an AC protocol that translates input tables to

the expected input of the functionality. We present such a wrapper for Tor in Section 7.

3.2

Generalized computational dierential privacy

For privacy preserving computations the notion of dierential privacy (DP) [Dwo06, DMNS06] is a

standard for quantifying privacy. Informally, dierential privacy of a mechanism guarantees that

the mechanism does not leak any information about a single user{even to an adversary that has

auxiliary information about the rest of the user base. It has also been generalized to protocols against

1 We stress that using standard methods, a distributed protocol with several parties can be represented by one

interactive Turing machine.

Plik z chomika:

Inne pliki z tego folderu:

Inne foldery tego chomika: