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.
展开▼
