Probabilistic Analysis of Anonymity

We present a formal analysis technique for probabilistic security properties of peer-to-peer communication systems based on random message routing among members. The behavior of group members and the adversary is modeled as a discrete-time Markov chain, and security properties are expressed as PCTL formulas. To illustrate feasibility of the approach, we model the Crowds system for anonymous Web browsing, and use a probabilistic model checker, PRISM, to perform automated analysis of the system and verify anonymity guarantees it provides. The main result of the Crowds analysis is a demonstration of how certain forms of anonymity degrade with the increase in group size and the number of random routing paths.

• Type: Conference
• Year: 2002
• Where: CSFW
• Authors: Vitaly Shmatikov
• Keywords: CSFW 2002, Discrete-time Markov Chain, Probabilistic Security Properties, Security Privacy, Security Properties