CertiCrypt: Formal Proofs for Computational Cryptography

Provable security, whose origins can be traced back to the pioneering work of Goldwasser and Micali, advocates a mathematical approach based on complexity theory in which the goals and requirements of cryptosystems are specified precisely, and where the security proof is carried out rigorously and makes all underlying assumptions explicit. In a typical provable security setting, one reasons about effective adversaries, modelled as arbitrary probabilistic polynomial-time Turing machines, and about their probability of thwarting a security objective, e.g., secrecy. In a similar fashion, security assumptions about cryptographic primitives bound the probability of polynomial algorithms to solve difficult problems, e.g., computing discrete logarithms. The security proof is performed by reduction by showing that the existence of an effective adversary with a certain advantage in breaking security implies the existence of an effective algorithm contradicting the security assumptions.

The game-playing technique is a general method to structure and unify cryptographic proofs. Its central idea is to view the interaction between an adversary and the cryptosystem as a game, and to study game transformations that preserve security, thus allowing to transform an initial game-that explicitly encodes a security property-into a game where it is easy to bound the advantage of the adversary. Code-based techniques (CBT) is an instance of the game-playing technique that has been used successfully to verify state-of-the-art cryptographic schemes, see e.g. Bellare and Rogaway. Its distinguishing feature is to take a code-centric view of games, security hypotheses and computational assumptions, that are expressed using (probabilistic, imperative, polynomial-time) programs. Under this view, game transformations become program transformations, and can be justified rigorously by semantic means. Although CBT proofs are easier to verify and are more easily amenable to machine-checking, they go far beyond established theories of program equivalence and exhibit a rich and broad set of reasoning principles that draws from program verification, algebraic reasoning, and probability and complexity theory. Thus, despite the beneficial effect of their underlying framework, CBT proofs remain inherently difficult to verify. In an inspiring paper, Halevi argues that formal verification techniques are mandatory to improve trust in game-based proofs, going as far as describing an interface to a tool for computer-assisted code-based proofs. As a first step towards the completion of Halevi's programme, we develop CertiCrypt, a framework to construct machine-checked code-based proofs in the Coq proof assistant.

CertiCrypt achieves many important goals of Halevi's ideal tool. At the same time, it brings a formal semantics perspective on the design of the tool. The main characteristics of CertiCrypt are:

• Direct and faithful encoding of code-based techniques.

  In order to take advantage of the generality of the CBT approach and to be readily accessible to cryptographers, we have chosen a formalism that is commonly used by cryptographers to describe games. Concretely, the lowest layer of CertiCrypt is a deep embedding in Coq of an imperative programming language with random assignments, structured datatypes, and procedure calls. The language semantics takes non-standard features such as complexity of programs, variable usage and calling policies into account. These are of paramount importance in cryptographic proofs.

• Support for automated proofs.

  We have developed certified tactics for the most common transformations: 1) semantics preserving transformations, including compiler optimisations such as dead code elimination, code motion, constant propagation and common subexpression elimination; 2) transformations based on indistinguishability, i.e., a change that cannot be detected with a non-negligible probability; and 3) transformations based on failure events, where both games behave identically unless a certain failure occurs, and it is shown that this failure occurs with negligible probability. This corresponds to the so-called fundamental lemma of game-playing proofs.

• Complete and independently verifiable proofs.

  CertiCrypt benefits from being developed on top of the Coq proof assistant to go beyond Halevi's vision in two respects. First, it supports the construction of full proofs, whereas Halevi mostly focuses on their "mundane parts". Second, it permits independent verifiability of proofs by third parties, which is an important motivation behind game-based proofs. Regarding full proofs, CertiCrypt requires that all (complexity-theoretic, group-theoretic, probabilistic) side conditions to apply transformations are justified within Coq, and also enables ad hoc reasoning, /e.g./, to conclude the proof in case of a sequence of games that ends in a non-trivial game. Regarding verifiability, CertiCrypt inherits from Coq its ability to provide certificates, or proof objects, that are automatically verifiable with a small trusted core, namely the type-checker of Coq.