Probabilistic Analysis of Anonymity by Vitaly Shmatikov Abstract: 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... http://citeseer.nj.nec.com/shmatikov02probabilistic.html "...for every complex problem, there is a solution that is simple, neat, and wrong." -- H.L. Mencken