Paper 2014/087

AnoA: A Framework For Analyzing Anonymous Communication Protocols

Michael Backes, Aniket Kate, Praveen Manoharan, Sebastian Meiser, and Esfandiar Mohammadi

Abstract

Anonymous communication (AC) protocols such as the widely used Tor network have been designed to provide anonymity over the Internet 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 different anonymity properties in a unified manner. In this work we present AnoA: a generic framework for defining, analyzing, and quantifying anonymity properties for AC protocols. In addition to quantifying the (additive) advantage of an adversary in an indistinguishability-based definition, AnoA uses a multiplicative factor, inspired from differential privacy. AnoA enables a unified quantitative analysis of well-established anonymity properties, such as sender anonymity, sender unlinkability, and relationship anonymity. AnoA modularly specifies adversarial capabilities by a simple wrapper-construction, called adversary classes. We examine the structure of these adversary classes and identify conditions under which it suffices to establish anonymity guarantees for single messages in order to derive guarantees for arbitrarily many messages. We coin this condition single-challenge reducability. This then leads us to the definition of Plug'n'Play adversary classes (PAC), which are easy to use, expressive, and single-challenge reducable. Additionally, we show that our framework is compatible with the universal composability (UC) framework. Leveraging a recent security proof about Tor, we illustrate how to apply AnoA to a simplified version of Tor against passive adversaries.

Note: Compared to the previous version, we introduced a special kind of adversary class, called a Plug'n'Play adversary class (PAC). We show that every adversary class that can be expressed as a PAC already satisfies single-challenge reducability (in earlier versions called sequential composability). Additionally, we define some PACs for formalizing scenarios without website-fingerprinting.