EasyCrypt: Computer-Aided Cryptographic Proofs
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.
EasyCrypt has been initially developed by the IMDEA Software Institute and Inria. It is now developed at the IMDEA Software Institute, Inria and École Polytechnique.
You can get EasyCrypt via our public git repository (browse):
git clone https://github.com/EasyCrypt/easycrypt.git
Installation instructions can be found in the README file, and some tutorial material is available, as well as a reference manual (under development). Note that the current release of EasyCrypt is still being developed. We do not guarantee backwards compatibility.
- The IACR School on Computer-aided Cryptography took place at University of Maryland, College Park, USA on June 1- 4 2015 and provide an hands-on introduction to EasyCrypt.
- The Joint EasyCrypt/F*/CryptoVerif School, 24-28 November 2014 in Paris. (You can download the EasyCrypt material)
- First EasyCrypt summer school and workshop: July 2013, UPenn.
Support for installing and using EasyCrypt can be obtained through the EasyCrypt club mailing list.
Support requests that include clearly marked non-public information can be sent to support @ easycrypt.info. In any other case, use the EasyCrypt club mailing list: our answers to you may also help others.
- Gilles Barthe (IMDEA Software Institute)
- François Dupressoir (University of Surrey)
- Benjamin Grégoire (Inria Sophia-Antipolis Méditerranée)
- Alley Stoughton (Boston University)
- Pierre-Yves Strub (École Polytechnique)
- Cécile Baritel-Ruet (Inria Sophia-Antipolis Méditerranée)
Miguel Ambrona, Simón Cancela-Díaz, Juan Manuel Crespo, Lavinia Damian, Guillaume Davy, Thomas Espitau, Edvard Fagerholm, Guido Genzone, Giuseppe Guagliardo, Daniel Hedin, Sylvain Heraud, César Kunz, Martin Moreau, Federico Olmedo, Anne Pacalet, Guillermo Ramos, Benedikt Schmidt, Léo Stefanesco, Santiago Zanella-Béguelin,
Our research is partially supported by ONR project AutoCrypt and SynthCrypt with Stanford University, the University of Pennsylvania, and SRI. We have received useful feedback from members of the MIT Lincoln Laboratory and the Naval Research Laboratory.
The group is partially funded by FP7 Marie Curie Actions-COFUND 291803 (Amarout II), ONR Grant N000141210914, Spanish projects TIN2009-14599 DESAFIOS 10 and TIN2012-39391-C04-01 StrongSoft, and Madrid Regional projects S2009TIC-1465 PROMETIDOS and S2013/ICE-2731 N-GREENS Software-CM.