Verified Computational Differential Privacy with Applications to Smart Metering

Gilles Barthe, George Danezis, Benjamin Grégoire, César Kunz, and Santiago Zanella-Béguelin

Abstract

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.

Details

Publication typeInproceedings
Published in26th IEEE Computer Security Foundations Symposium, CSF 2013
Pages287-301
PublisherIEEE Computer Society
> Publications > Verified Computational Differential Privacy with Applications to Smart Metering