Differential Privacy by Typing in Security Protocols

By Fabienne Eigner, Matteo Maffei. 2013

35 citations recorded by the source corpus.

Differential privacy is a confidentiality property for database queries which allows for the release of statistical information about the content of a database without disclosing personal data. The variety of database queries and enforcement mechanisms has recently sparked the development of a number of mechanized proof techniques for differential privacy. Personal data, however, are often spread across multiple databases and queries have to be jointly computed by multiple, possibly malicious, parties. Many cryptographic protocols have been proposed to protect the data in transit on the network and to achieve differential privacy in a distributed, adversarial setting. Proving differential privacy for such protocols is hard and, unfortunately, out of the scope of the aforementioned mechanized proof techniques. In this work, we present the first framework for the mechanized verification of distributed differential privacy. We propose a symbolic definition of differential privacy for distributed databases, which takes into account Dolev-Yao intruders and can be used to reason about compromised parties. Furthermore, we develop a linear, distance-aware type system to statically and automatically enforce distributed differential privacy in cryptographic protocol implementations (expressed in the RCF calculus). We also provide an algorithmic variant of our type system, which we prove sound and complete. Finally, we tested our analysis technique on a recently proposed protocol for privacy-preserving web analytics: we discovered a new attack acknowledged by the authors, proposed a fix, and successfully type-checked the revised variant.

Subfields: Artificial Intelligence, Sociology and Political Science

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Sociology and Political Science

Citations in the corpus

Advanced Probabilistic Couplings for Differential Privacy (2016, neutral): “By now, there are tools that formally guarantee differential privacy via relational program logics [2, 6], linear type systems [25, 29, 42], interactive automata [50, 51], product programs [7], satisﬁability modulo theories [28], reﬁnement type systems [9], and more.”
Proving Differential Privacy in Hoare Logic (2014, methodology): “…memoriesm1 and m2 related byΦ, and every subsetA of output memories, Pr [c,m1 : A] ≤ exp(ǫ) Pr [c,m2 : A] + δ. HerePr [c,m : A] denotes the probability of the output memory landing inA according to distributionJcK m, whereJcK maps an initial memorym to a distributionJcK m of output memories.”
Differentially private data aggregation with optimal utility (2014, background): “We now formally deﬁne the notion of DDP for protocols, close in spirit to the one introduced in [23].”
Dynamic Differential Privacy for ADMM-Based Distributed Classification Learning (2017, background): “Eigner and Maffei developed the first framework for the automated verification of distributed differential privacy in [16]; they developed a system to enforce the distributed differential privacy in cryptographic protocol implementations.”