Probabilistic Model Checking of an Anonymity System. Shmatikov, V. Journal of Computer Security, 12(3-4):355\textendash377, 2004. ![Probabilistic Model Checking of an Anonymity System [link]](https://bibbase.org/img/filetypes/link.svg "link")
Paper abstract bibtex 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.
@article {crowds-model,
title = {Probabilistic Model Checking of an Anonymity System},
journal = {Journal of Computer Security},
volume = {12},
number = {3-4},
year = {2004},
pages = {355{\textendash}377},
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.},
keywords = {anonymity, P2P, routing},
url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.10.6570},
author = {Vitaly Shmatikov}
}
Downloads: 0
{"_id":"6pRWquHTNgu2RZLTZ","bibbaseid":"shmatikov-probabilisticmodelcheckingofananonymitysystem-2004","downloads":0,"creationDate":"2018-07-03T04:50:29.022Z","title":"Probabilistic Model Checking of an Anonymity System","author_short":["Shmatikov, V."],"year":2004,"bibtype":"article","biburl":"https://gnunet.org/bibliography/export/bibtex","bibdata":{"bibtype":"article","type":"article","title":"Probabilistic Model Checking of an Anonymity System","journal":"Journal of Computer Security","volume":"12","number":"3-4","year":"2004","pages":"355\\textendash377","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.","keywords":"anonymity, P2P, routing","url":"http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.10.6570","author":[{"firstnames":["Vitaly"],"propositions":[],"lastnames":["Shmatikov"],"suffixes":[]}],"bibtex":"@article {crowds-model,\n\ttitle = {Probabilistic Model Checking of an Anonymity System},\n\tjournal = {Journal of Computer Security},\n\tvolume = {12},\n\tnumber = {3-4},\n\tyear = {2004},\n\tpages = {355{\\textendash}377},\n\tabstract = {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.},\n\tkeywords = {anonymity, P2P, routing},\n\turl = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.10.6570},\n\tauthor = {Vitaly Shmatikov}\n}\n","author_short":["Shmatikov, V."],"key":"crowds-model","id":"crowds-model","bibbaseid":"shmatikov-probabilisticmodelcheckingofananonymitysystem-2004","role":"author","urls":{"Paper":"http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.10.6570"},"keyword":["anonymity","P2P","routing"],"downloads":0},"search_terms":["probabilistic","model","checking","anonymity","system","shmatikov"],"keywords":["anonymity","p2p","routing"],"authorIDs":[],"dataSources":["FWsPTwsmjtrBtRS3B"]}