wiki:WikiStart

EasyCrypt: Computer-Aided Cryptographic Proofs

Overview

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.

More…

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.

X.png imdea.png inria.png 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.

Downloads

https://travis-ci.org/EasyCrypt/easycrypt.svg

The current release of EasyCrypt (version 1.0) is still under development. Please join the EasyCrypt club mailing list to be informed of evolutions.

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.

EasyCrypt 0.2

You can also download EasyCrypt version 0.2 and its documentation. However, we are no longer actively supporting this version, and recommend switching to version 1.0.

Past Events

Contact

Support for installing and using EasyCrypt can be obtained through the EasyCrypt club mailing list.

To file bug reports and suggest enhancements to our tools, please use our tracker. You can log into the tracker using any GitHub account.

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.

People

Students

  • Cécile Baritel-Ruet (Inria Sophia-Antipolis Méditerranée)

Former members

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,

Acknowledgments

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.

Last modified 6 weeks ago Last modified on 13 Mar 2017, 10:47:26