Formal Analysis of Anonymity Based on Strand Space Model

Anonymous communication protocols can be used in ubiquitous environments to preserve the identity of users. To verify the correctness of the protocol, a formal framework for the analysis of anonymity property of anonymous communication protocols in terms of strand space model was proposed. The key ingredient is the notions of equivalent bundles and extremum pair, which are used to define anonymity. Then we illustrate our approach by proving sender anonymity and unlinkability for two well-known anonymous communication protocols, Crowds and Onion Routing and show how the framework is capable of verifying the correctness of protocols or capturing the flaws. The result shows that sender anonymity will fail in Crowds if there exist a global attacker and relation anonymity will fail in Onion Routing if the attacker knows the onion router's private key. Furthermore, to analyze the particular version of Onion Routing proposed in [1], it can also find the flaw in the protocol.