*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:

- High-level reasoning about distributions defined by probabilistic programs.
- Semantic preserving program transformations.
- Cryptography-based program transformations.
- Asymptotic reasoning.

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.