Computationally Sound Reasoning about Privacy Properties (B03)

• Subject Area: Theoretical Computer Science
• Term: from 2016 to 2019
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 272573906

Cryptographic protocols are typically analyzed using symbolic abstractions. This requires to show that the abstractions can be soundly implemented with cryptographic primitives. Existing approaches fall short of this goal, for privacy-sensitive scenarios: they pertain to restricted programming languages and adversaries; do not address strong secrecy properties; and fail to compose with other results. We aim to overcome these limitations. We consider cryptographic primitives at the core of privacy-protection technologies, with strong adversaries that are capable of observing the timing behavior of cryptographic protocols. We will in particular develop composable computational soundness results for Oblivious RAM and for Dalvik Bytecode.

• DFG Programme: Collaborative Research Centres
• Subproject of: SFB 1223: Methods and Tools for Understanding and Controlling Privacy
• International Connection: France
• Applicant Institution: Universität des Saarlandes
• Project Heads: Professor Dr. Michael Backes; Dr. Véronique Cortier