As cryptographic proofs have become essentially unverifiable, cryptographers have argued in favor of computer-aided proofs. CertiCrypt/EasyCrypt is a toolset that assists the construction and verification of cryptographic proofs; it supports common patterns of reasoning in cryptography, and has been used successfully to prove the security of many examples, including encryption schemes, signature schemes, zero-knowledge protocols and hash functions. Recently, CertiCrypt was extended to reason about differentially private computations.
CertiCrypt/EasyCrypt takes a language-based approach to cryptography: the security of a cryptographic scheme and the cryptographic assumptions upon which its security relies are expressed by means of probabilistic programs, called games; in a similar way, adversarial models are specified in terms of complexity classes, e.g. probabilistic polynomial-time programs. This code-centric view leads to statements that are amenable to formalization and tool-assisted verification. CertiCrypt instruments a rich set of verification techniques for probabilistic programs, including equational theories of observational equivalence, relational Hoare logic, data-flow analysis-based program transformations, and game-based techniques such as eager/lazy sampling and failure events.
The toolset has two main components:
- Certicrypt is a fully machine-checked framework built
on top of the Coq proof assistant. It is based on a deep embedding
of an extensible probabilistic imperative language and a formalization
of probabilistic polynomial-time programs. Verification methods are
implemented in Coq, and proved correct w.r.t. program semantics.
- Easycrypt is an automated tool for elaborating
security proofs of cryptographic systems from proof sketches.
The latter are compact, formal representations of the essence of a
proof as a sequence of games and hints. Proof sketches are checked
automatically using off-the-shelf SMT solvers and automated theorem
provers.