Project B3

Computationally Sound Reasoning
about Privacy Properties

Principal Investigators

Michael Backes

E9 1 3.01
66123 Saarbrücken

+49 681 302 3249
+49 681 302 57365
director(Replace this parenthesis with the @ sign)

PhD Students

Esfandiar Mohammadi

66123 Saarbrücken

+49 681 302 57372
+49 681 302 57365
mohammadi(Replace this parenthesis with the @ sign)

Project Summary

Proving security and privacy properties of protocols that rely on cryptographic operations constitutes a highly complex and error-prone task. As a consequence, the security of such protocols is usually analyzed by replacing cryptographic operations by symbolic abstractions that obey simple cancellation rules. However, carrying such analyses over to real-world implementations requires to show that these abstractions can be soundly implemented again using suitable cryptographic primitives, and existing research approaches fall short of achieving this goal for privacy-sensitive scenarios in many respects: (a) they pertain to restricted programming languages and adversarial capabilities; (b) they fall short in addressing strong secrecy properties as the central requirement in privacy-sensitive applications; and (c) they fail to compose with other results of this form. The objective of this project is to overcome these limitations, by developing novel methods to enable a computationally sound analysis of privacy properties in modern cryptographic protocols. This encompasses support for soundly analyzing symbolic abstractions of interactive cryptographic primitives that are at the core of many privacy-protection technologies, and the consideration of extended, privacy-critical adversarial capabilities that extract sensitive information by observing the timing behavior of cryptographic protocols. Building upon these results, we aim to enable symbolic, yet cryptographically sound reasoning about Oblivious RAM (one of the currently most important interactive privacy-protection technologies). We will furthermore aim to leverage our soundness results to additional programming languages, in particular to Android’s Dalvik Bytecode. Finally, we will derive composability guarantees for computational soundness for comprehensive privacy properties based on prior work on composable deduction soundness.

Role Within the Collaborative Research Center


Open Positions

In the context of this project we are looking for a qualified PhD student with a track record in topics relevant to the project. If you are interested please send a letter of intent together with your short CV to the PIs of the project.