Verified Computational Differential Privacy with Applications to Smart Metering
Résumé
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.