Security of Cryptographic ALgorithms with Probabilities is a four-year ANR-sponsored project in the context of the call for project Sécurité et Sûreté Informatique.
Our day-to-day lives increasingly depend upon information and our ability to manipulate it securely. That is, in a way that prevents malicious elements to subvert the available information for their own benefits. This requires solutions based on cryptographic systems (primitives and protocols).
However, no matter how carefully crafted cryptographic systems are, experience has shown that effective attacks can remain hidden for years. This may be caused by poor design or often unclear and poorly defined security properties and assumptions.
Therefore, provable security, where new systems are published with a rigorous definition of their security goals and a mathematical proof that they meet their goals, is being increasingly advocated. While the adoption of provable security significantly increases, the complexity and diversity of designed systems tend to increase too. Hence, it is largely agreed on that the point has been reached where it is no longer viable to construct or verify cryptographic proofs by hand (Bellare& Rogaway 2004, Shoup 2004, Halevi 2005) and that there is a need for computer-aided verification methods for cryptographic systems. The goal of this project is to achieve a major step towards building automated tools for the verification of cryptographic systems. In order, to reconcile generality, imposed by the high diversity of cryptographic systems, and automation, we shall build our tools upon Coq.
The success of our project will depend on mastering the following key challenges.
We need to develop a probabilistic programming language that allows to describe the cryptographic systems to be verified. It has to be more complex than a simple probabilistic language since it must allow the description of games that specify the interaction between adversaries and the systems. Therefore, it should allows us to specify an adversary as a black-box that has access to some oracles; it needs to express concurrent systems where the adversary may affect scheduling; and it should be possible to characterize resource-bounded computations.
Most properties of random programs rely on good properties of pseudo-random generators. These properties are generally presented in a very abstract way and are generally implicitly admitted in proofs of probabilistic algorithms. We shall define formally the relevant properties for a probabilistic program. We will focus on watermarking algorithms for studying this area.
Verification of cryptosystems needs the development of a specific verification theory that has to include the following proof activities:
By the end of the project we expect to have a Coq-based tool for proving correctness of cryptosystems. We will demonstrate its usefulness by considering three major areas: key-exchange protocols, computationally sound type systems for non-interference and data integrity, and watermarking. In contrast to existing Dolev-Yao based verification tools, we will be able to treat group protocols and have complexity-theoretic proofs. More importantly, the tool will be open in the sense that it should be reasonably easy to consider new primitives. This does not seem easily achievable for symbolic tools.