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.