A Formalization of Anonymity and Onion Routing
S. Mauw, J. Verschuren and E.P. de Vink

The use of formal methods to verify security protocols with
respect to secrecy and authentication has become standard practice.
In contrast, the formalization of other security goals, such as privacy,
has received less attention. Due to the increasing importance of privacy
in the current society, formal methods will also become indispensable
in this area. Therefore, we propose a formal definition of the notion
of anonymity in presence of an observing intruder. We validate this
definition by analyzing a well-known anonymity preserving protocol,
viz. onion routing.