Quantitative anonymity guarantees for Tor

Abstract

In this thesis, we present a methodology to compute sound anonymity guarantees for anonymous communication protocols, which we apply to the Tor protocol. To this end, we present AnoA, a formal framework for quantifying the anonymity of anonymous communication protocols against modularly describable adversaries. We show how the Tor protocol can be analyzed in an abstract way by utilizing an existing formalization of Tor in the universal composability (UC) framework and prove that this analysis is sound. Moreover, we derive efficiently computable, sound anonymity guarantees for Tor against eavesdropping adversaries that may control Tor servers or wiretap communications between parties. For known adversaries that perform perfect traffic correlations we show that our bounds are tight. Finally, we perform an extensive analysis of the Tor network against such adversaries in which we calculate the anonymity of Tor when using Tor's current path selection, thereby considering many real-world properties of the path selection algorithm, as well as when using one of several variants, against a variety of eavesdropping adversaries that can control Tor nodes (depending on various properties) or wiretap the communication between them.

In dieser Arbeit präsentieren wir eine neue Methode, um beweisbar sichere Anony-mitätsgarantien für Protokolle zur anonymen Kommunikation zu geben und veranschaulichen die Anwendung dieser Methode anhand des Tor Protokolls. Zu diesem Zweck präsentieren wir zunächst das AnoA Framework, welches dazu dient, die Anony-mität von Protokollen zur anonymen Kommunikation zu quantifizieren. Der Angreifer, der in AnoA betrachtet wird, ist modular konfigurierbar. Wir zeigen, wie das Tor Protokoll in einer abstrakten Weise analysiert werden kann und greifen hierbei auf eine existierende Formalisierung von Tor im Universal Composibility (UC) Framework zurück. Wir beweisen, dass unsere abstrakten Betrachtungen sichere Garantien ergeben. Darüber hinaus entwickeln wir effizient berechenbare und beweisbar sichere Formeln, mit denen sich die Sicherheit von Tor gegenüber von Angreifern, die entweder durch Besitz eigener Tor Server oder durch eine Überwachung der Kommunikation, auf eine passive Art versuchen, die Anonymität zu brechen. Letztlich führen wir eine umfassende Analyse des Tor Netzwerks durch und berechnen die Anonymität, die Tor gegen eine Vielzahl solcher Angreifer zur Verfügung stellt, basierend auf den technischen Eigenschaften von Tor's Pfadsuchalgorithmus (und einigen Alternativen).