Verified Computational Differential Privacy with Applications to Smart Metering

Abstract : EasyCrypt is a tool-assisted framework for reason- ing about probabilistic computations in the presence of adver- sarial code, whose main application has been the verification of security properties of cryptographic constructions in the compu- tational 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.
Document type :
Conference papers
Liste complète des métadonnées

https://hal.inria.fr/hal-00935736
Contributor : Benjamin Gregoire <>
Submitted on : Friday, January 24, 2014 - 6:59:39 AM
Last modification on : Thursday, January 11, 2018 - 4:41:55 PM

Identifiers

Collections

Citation

Gilles Barthe, George Danezis, Benjamin Grégoire, César Kunz, Santiago Zanella-Béguelin. Verified Computational Differential Privacy with Applications to Smart Metering. 2013 IEEE 26th Computer Security Foundations Symposium, Jun 2013, New Orleans, United States. pp.287-301, ⟨10.1109/CSF.2013.26⟩. ⟨hal-00935736⟩

Share

Metrics

Record views

156