Computationally Sound Reasoning
about Privacy Properties
Proofs of security protocols are known to be error-prone and, due to multiple interleaved protocol runs that are typical for distributed systems, awkward for humans to construct. Vulnerabilities have indeed accompanied the early design of security protocols, from the timing attack by Bleichenbacher [B03-13] on the SSL 3.0 protocol, which two years earlier was shown secure by Wagner and Schneier [B03-28] in a weaker adversarial model, to a flaw in the Microsoft Passport service [B03-23], which allowed an attacker to reset passwords, to several Kerberos 5 flaws found during the verification of the protocol [B03-15].
Soon after the first protocols were developed, researchers began to work on automating security proofs. The predominantly used class of tools for this purpose are symbolic protocol verifiers, e.g., ProVerif [B03-12], AVISPA [B03-5], Scyther [B03-19], Deepsec [B03-17], Tamarin [B03-27], and APTE [B03-16]. Symbolic protocol verifiers abstract cryptographic operations as symbolic terms with corresponding cancellation rules, e.g., the encryption of a message m with the key k is represented as a term enc(k;m) with the simple cancellation rule dec(k;enc(k;m)) = m. The attacker in such a symbolic model is given by a non-deterministic algorithm that is restricted to applying the given set of rules. Establishing security in such models then boils down to showing that no algorithm that pertains to the given set of rules is capable of violating the security property under consideration, e.g., it cannot extract the message m. Grounding the security analysis on symbolic terms and a fixed set of rules reliefs proofs from cryptographic details such as reduction proofs, probabilistic behavior, and error probabilities. This was the key for automation, at least for moderate-sized protocols and for simple trace properties such as authentication.
However, to show the absence of attacks against actual cryptographic realizations, such a symbolic abstraction has to be sound, i.e., replacing the symbolic abstraction with a (provable secure) cryptographic instantiation should not give rise to attacks that were not covered on the symbolic level. We call symbolic models that are accurate in this sense computationally sound. In a similar spirit to symbolic protocol verifiers, tools have been proposed that allow for checking information-flow properties within a given language, e.g., Joana [B03-24] or Cassandra [B03-26]. These tools enable a detailed analysis already on the implementation level using the semantics of the programming language under consideration, while relying on a symbolic model for cryptographic operations in declassification or endorsement policies(typically encryption or signatures). Hence these works would benefit from computational soundness results as well. While these tools allow for declassification and endorsement policies, figuring out whether some piece of data can be declassified requires reasoning about the secrecy of, e.g., the key it was encrypted with, which comes back to the original question, information flow. Our main objective in this project was thus to develop novel methods and tools to enable a computationally sound analysis of privacy properties in modern cryptographic protocols. This encompasses providing support for reasoning about interactive cryptographic primitives that are at the core of many privacyprotection technologies; moreover, it aims to include extended, privacy-critical adversarial capabilities and to ensure the secure composition and integration of these results. Much of the work done focused on the CoSP framework [B03-6] for computational soundness proofs.
Prior to CoSP, computational soundness results were specific to a given, often ad hoc formalism. The reusability of such results was limited. e.g., computational soundness for public-key encryption did not automatically carry over to different formalisms and underlying programming languages. As a consequence, there were many computational soundness results for the same cryptographic primitives but within different formalisms. To remedy this situation, the CoSP framework decouples the embedding of the programming language from the computational soundness proofs, thereby entailing the reusability of computational soundness results to other programming languages. Hence, proving x cryptographic primitives sound for y programming languages / formal calculi only requires x+y proofs instead of x _ y without CoSP. Prior to this project, the applied p-calculus [B03-6] and RCF [B03-7] have been embedded into CoSP. We extend CoSP to encompass binary compiled languages and fragments of Dalvik Bytecode, the language used for the distribution of Android Apps.
Role Within the Collaborative Research Center