Probabilistic analysis of anonymity
- 25 June 2003
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
We present a formal analysis technique for probabilistic security properties of peer-to-peer communication system s 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 anony- mous 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.Keywords
This publication has 17 references indexed in Scilit:
- Probabilistic noninterference in a concurrent languagePublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Model checking for a probabilistic branching time logic with fairnessDistributed Computing, 1998
- Model checking of probabilistic and nondeterministic systemsPublished by Springer Nature ,1995
- A logic for reasoning about time and reliabilityFormal Aspects of Computing, 1994
- Toward a Mathematical Foundation for Information Flow SecurityJournal of Computer Security, 1992
- Automatic verification of probabilistic concurrent finite state programsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,1985
- Probabilistic temporal logics for finite and bounded modelsPublished by Association for Computing Machinery (ACM) ,1984
- On the security of public key protocolsIEEE Transactions on Information Theory, 1983
- Reasoning with time and chanceInformation and Control, 1982
- Untraceable electronic mail, return addresses, and digital pseudonymsCommunications of the ACM, 1981