Home

EasyCrypt is a toolset for reasoning about relational properties of probabilistic computations with adversarial code. Its main application is the construction and verification of game-based cryptographic proofs. The development of EasyCrypt was initiated in 2009, and the initial prototype was used to prove the security of several constructions, including the Cramer-Shoup encryption scheme, the Merkle-Damgaard iterative hash function design, and of the ZAEP encryption scheme.

Starting from 2012, we have performed a complete reimplementation of the initial prototype, with the goal to overcome several of its limitations. The goals of the reimplementation were three-fold: first, consolidate the prototype into a robust platform that can be maintained and extended with reasonable effort; second, provide a versatile platform that supports automated proofs but also allows users to perform complex interactive proofs that interleave program verification and formalization of mathematics, which are intimately intertwined when formalizing cryptographic proofs; third, develop and implement the necessary foundations required to carry some standard cryptographic reasonings that were not supported by the initial prototype, such as hybrid arguments and simulation-based security proofs. To achieve its goals, EasyCrypt implements a probabilistic Hoare logic pHL for bounding the probability of post-conditions, and embeds pRHL and pHL into an ambient logic that can for instance be used to perform hybrid arguments. In addition, it implements a module system and a theory mechanism that support compositional proofs.

These developments have expanded significantly the scope of potential applications of EasyCrypt and enabled the formalization of examples that were previously out of reach of the initial prototype. For instance, we have formalized the security of two protocols based on garbled circuits: Yao's secure function evaluation protocol and Gennaro-Gentry-Parno verifiable computation protocol. Moreover, we have formalized a proof of security for authenticated key-exchange protocols, and derived proofs under weaker assumptions for the NAXOS and NETS protocols.