@inproceedings{d851c4ca2ba24ea698fcecfede86bd05,
title = "Formal analysis of the information leakage of the DC-nets and crowds anonymity protocols",
abstract = "A crucial goal in computer security is to protect sensitive information from unwanted disclosure. However, some leakage is often unavoidable, be it by design of the system or by technological limitations. The field of Quantitative Information Flow (QIF) is concerned with the quantification, and limitation, of information leakage in systems. The QIF framework models systems as information-theoretic channels taking (secret) inputs and producing (observable) outputs, thereby increasing the adversary{\textquoteright}s knowledge about the secret value, as measured by some information metric. In this paper we use probabilistic model checking to obtain channels modeling two popular anonymity protocols, the Dining Cryptographers (a.k.a. DC-Nets) and Crowds, in two versions each. We then derive the systems{\textquoteright} capacities w.r.t. the g-leakage framework, which are robust upper bounds on information leakage that hold irrespectively of the probability distribution on secret values, or of the interests and goals of the adversary. To the best of our knowledge, this is the most general QIF analyses of such protocols.",
keywords = "Crowds, Dining cryptographers, Formal methods, g-leakage, Model checking, Quantitative information flow",
author = "Arthur Am{\'e}rico and Artur Vaz and Alvim, {M{\'a}rio S.} and Campos, {S{\'e}rgio V.A.} and Annabelle McIver",
year = "2017",
doi = "10.1007/978-3-319-70848-5_10",
language = "English",
isbn = "9783319708478",
series = "Lecture Notes in Computer Science",
publisher = "Springer, Springer Nature",
pages = "142--158",
editor = "Simone Cavalheiro and Jos{\'e} Fiadeiro",
booktitle = "Formal methods: foundations and applications",
address = "United States",
note = "20th Brazilian Symposium on Formal Methods, SBMF 2017 ; Conference date: 29-11-2017 Through 01-12-2017",
}