Skip to Main content Skip to Navigation
New interface
Conference papers

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
Complete list of metadata
Contributor : Benjamin Gregoire Connect in order to contact the contributor
Submitted on : Friday, January 24, 2014 - 6:59:39 AM
Last modification on : Friday, November 18, 2022 - 9:26:42 AM

Links full text




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⟩



Record views