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.
Type de document :
Communication dans un congrès
2013 IEEE 26th Computer Security Foundations Symposium, Jun 2013, New Orleans, United States. IEEE Computer Society, pp.287-301, 2013, Proceedings of the 26th IEEE Computer Security Foundations Symposium. 〈10.1109/CSF.2013.26〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00935736
Contributeur : Benjamin Gregoire <>
Soumis le : vendredi 24 janvier 2014 - 06:59:39
Dernière modification le : jeudi 11 janvier 2018 - 16:41:55

Identifiants

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. IEEE Computer Society, pp.287-301, 2013, Proceedings of the 26th IEEE Computer Security Foundations Symposium. 〈10.1109/CSF.2013.26〉. 〈hal-00935736〉

Partager

Métriques

Consultations de la notice

123