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