As cryptographic proofs have become essentially unverifiable, cryptographers have argued in favor of computer-aided proofs. CertiCrypt 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 constructions, including encryption and digital signature schemes, zero-knowledge protocols, and hash functions. An extension of CertiCrypt supports reasoning about differential privacy.
CertiCrypt takes a language-based approach to cryptography: security goals and assumptions are expressed by means of probabilistic programs. 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 provides a rich set of verification techniques for probabilistic programs, including equational theories of observational equivalence, a probabilistic relational Hoare logic, certified program transformations, and techniques widely used in cryptographic proofs such as eager/lazy sampling and failure events.
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 programming language and a formalization of probabilistic polynomial-time programs. Verification methods are implemented in Coq, and proved correct w.r.t. program semantics.