Formal analysis of the information leakage of the DC-nets and crowds anonymity protocols

Arthur Américo*, Artur Vaz, Mário S. Alvim, Sérgio V.A. Campos, Annabelle McIver

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contributionpeer-review

3 Citations (Scopus)


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’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’ 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.

Original languageEnglish
Title of host publicationFormal methods: foundations and applications
Subtitle of host publication20th Brazilian Symposium, SBMF 2017, Recife, Brazil, November 29 – December 1, 2017. Proceedings
EditorsSimone Cavalheiro, José Fiadeiro
Place of PublicationCham
PublisherSpringer, Springer Nature
Number of pages17
ISBN (Electronic)9783319708485
ISBN (Print)9783319708478
Publication statusPublished - 2017
Event20th Brazilian Symposium on Formal Methods, SBMF 2017 - Recife, Brazil
Duration: 29 Nov 20171 Dec 2017

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference20th Brazilian Symposium on Formal Methods, SBMF 2017


  • Crowds
  • Dining cryptographers
  • Formal methods
  • g-leakage
  • Model checking
  • Quantitative information flow


Dive into the research topics of 'Formal analysis of the information leakage of the DC-nets and crowds anonymity protocols'. Together they form a unique fingerprint.

Cite this