Verified Computational Differential Privacy with Applications to Smart Metering

By Gilles Barthe, George Danezis, Benjamin Gr'egoire, César Kunz, Santiago Zanella-B'eguelin. 2013

84 citations recorded by the source corpus.

EasyCrypt is a tool-assisted framework for reasoning about probabilistic computations in the presence of adversarial code, whose main application has been the verification of security properties of cryptographic constructions in the computational model. We report on a significantly enhanced version of EasyCrypt that accommodates a richer, user-extensible language of probabilistic expressions and, more fundamentally, supports reasoning about approximate forms of program equivalence. This enhanced framework allows us to express a broader range of security properties, that notably include approximate and computational differential privacy. We illustrate the use of the framework by verifying two protocols: a two-party protocol for computing the Hamming distance between bit-vectors, yielding two-sided privacy guarantees; and a novel, efficient, and privacy-friendly distributed protocol to aggregate smart meter readings into statistics and bills.

Subfields: Artificial Intelligence

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

Citations in the corpus

Detecting Violations of Differential Privacy (2018, background): “Suppose we start from a database candidate ([1, 1, 1, 1, 1], [2, 2, 2, 2, 2]).”
Advanced Probabilistic Couplings for Differential Privacy (2016, neutral): “[5] present a system for reasoning about computational differential privacy [39] a relaxation of differential privacy where the adversary are computationally-bound.”
Proving Differential Privacy in Hoare Logic (2014, methodology): “Finally,CertiPriv [11] and EasyCrypt [6] use an approximate relational Hoare logic for probabilistic programs to verify differential privacy.”
InnerCircle: A parallelizable decentralized privacy-preserving location proximity protocol (2015, background): “Similar proofs for semi-honest adversaries were constructed in [2].”
Differentially private data aggregation with optimal utility (2014, background): “Several specialized ad-hoc cryptographic protocols have been proposed recently to solve the problem of data aggregation in a distributed, privacypreserving manner, which has enabled the enforcement of DDP in some challenging scenarios, such as smart metering [13,24] and web analytics [7, 20,21].”
Smart meter aggregation via secret-sharing (2013, methodology): “linear([1] ∗ 100, readings) rsquares = [c.”
Proving differential privacy with shadow execution (2019, methodology): “D2: q[0]=1 q[1]=2 q[2]=2 q[3]=4”
Private and Dynamic Time-Series Data Aggregation with Trust Relaxation (2014, background): “[4] proposed a solution whereby each smart meter in the protocol establishes an ephemeral DH shared secret with all the aggregators.”
Probabilistic Relational Reasoning for Differential Privacy (2013, methodology): “In this way, one can capture adversaries that have only partial views on the system, as required for distributed differential privacy [Barthe et al. 2013; Beimel et al. 2008].”
PrivEx: Private Collection of Traffic Statistics for Anonymous Communication Networks (2014, result): “[3] which itself is an extension of previous works by Kursawe et al.”
The Effect of IoT New Features on Security and Privacy: New Threats, Existing Solutions, and Challenges Yet to Be Solved (2018, background): “, data collection [63], privacy data sharing with the cloud service [64]).”