Introduction
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.
Objectives
The success of our project will depend on mastering the following key challenges.
Probabilistic language and semantics for cryptographic proofs
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.
Formalization of random generators
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.
Proof theory
Verification of cryptosystems needs the development of a specific verification theory that has to include the following proof activities:
- High-level reasoning about distributions defined by probabilistic programs.
- Semantic preserving program transformations.
- Cryptography-based program transformations.
- Asymptotic reasoning.
Partners
- EVEREST-INRIA
- Plume-LIP
- ProVal-LRI
- CPR-Cédric
- VERIMAG/DCS
