Institut für Informatik

Technical Report No. 171 - Abstract

Burkhart Wolff, Oliver Berthold, Sebastian Clauss, Hannes Federrath, Stefan Koepsell, Andreas Pfitzmann
Towards a Formal Analysis of a Mix Network

We present a formal model of Mixes in an open network (following the concepts of D. Chaum) and apply well-known analysis techniques to a new type of security property, namely unlinkability. The network is composed of senders, receivers and Mix stations. The network and its components are formalized as CSP processes, and combined with a (passive) attacker. Based on the model-checker FDR, formal analyses of networks and their security properties are performed. The approach serves as a feasibility study for the analysis of anonymity and unobservability with a particular analysis technique. Moreover, it will result in the implementation of a particular analysis-testbed for the investigation of other security properties such as unobservabilityor more advanced protocols that might pave the way to secure Mix implementations with dynamically controlled dummy traffic.

Report No. 171 (PostScript)