Verified Computational Differential Privacy with Applications to Smart Metering

被引：50

作者：

Barthe, Gilles ^{[1
]}

Danezis, George ^{[3
]}

Gregoire, Benjamin ^{[2
]}

Kunz, Cesar ^{[1
]}

Zanella-Beguelin, Santiago ^{[3
]}

机构：

[1] IMDEA Software Inst, Madrid, Spain

[2] INRIA, Sophia Antipolis, France

[3] Microsoft Res, Cambridge, England

来源：

2013 IEEE 26TH COMPUTER SECURITY FOUNDATIONS SYMPOSIUM (CSF) | 2013年

关键词：

D O I：

10.1109/CSF.2013.26

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

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.

引用

页码：287 / 301

页数：15

共 46 条

[11] Probabilistic relational reasoning for differential privacy [J].

Barthe, Gilles ;

Koepf, Boris ;

Olmedo, Federico ;

Zanella Beguelin, Santiago .

ACM SIGPLAN NOTICES, 2012, 47 (01) :97-109

[12] Formal Certification of Code-Based Cryptographic Proofs [J].

Barthe, Gilles ;

Gregoire, Benjamin ;

Beguelin, Santiago Zanella .

ACM SIGPLAN NOTICES, 2009, 44 (01) :90-101

[13]

Beimel A, 2008, LECT NOTES COMPUT SC, V5157, P451, DOI 10.1007/978-3-540-85174-5_25

[14]

Boneh D, 2005, LECT NOTES COMPUT SC, V3378, P325

[15]

Chan T.-H. H., 2012, International Conference on Financial Cryptography and Data Security, P200

[16]

Chaudhuri S., 2011, P 19 ACM SIGSOFT S 1, P102, DOI DOI 10.1145/2025113.2025131

[17] Hyperproperties [J].

Clarkson, Michael ;

Schneider, Fred .

JOURNAL OF COMPUTER SECURITY, 2010, 18 (06) :1157-1210

[18]

D'Antoni P. L., 2013, TYPE BASED SEN UNPUB

[19]

Danezis George, 2011, Information Hiding. 13th International Conference, IH 2011. Revised Selected Papers, P148, DOI 10.1007/978-3-642-24178-9_11

[20]

Deng Y, 2011, CMUCS11110 CMUCS11110

← 1 2 3 4 5 →