Probabilistic analysis of an anonymity system

Issue title: Special issue on CSFW15

Guest editors: S. Schneider

Article type: Research Article

Authors: Shmatikov, Vitaly^{; *}

Affiliations: SRI International, 333 Ravenswood Avenue, Menlo Park, CA 94025, USA. E-mail: [email protected]

Note: [*] Supported in part by DARPA contract N66001-00-C-8015 “Agile Management of Dynamic Collaboration”.

Abstract: We use the probabilistic model checker PRISM to analyze the Crowds system for anonymous Web browsing. This case study demonstrates how probabilistic model checking techniques can be used to formally analyze security properties of a peer-to-peer group communication system based on random message routing among members. The behavior of group members and the adversary is modeled as a discrete-time Markov chain, and the desired security properties are expressed as PCTL formulas. The PRISM model checker is used to perform automated analysis of the system and verify anonymity guarantees it provides. Our main result is a demonstration of how certain forms of probabilistic anonymity degrade when group size increases or random routing paths are rebuilt, assuming that the corrupt group members are able to identify and/or correlate multiple routing paths originating from the same sender.

DOI: 10.3233/JCS-2004-123-403

Journal: Journal of Computer Security, vol. 12, no. 3-4, pp. 355-377, 2004