Version 64 (modified by Pierre-Yves Strub, 3 years ago) (diff)


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. Initial applications of EasyCrypt focus on encryption and signature schemes.

However, the initial prototype has been extended significantly to reason about the security of cryptographic systems, which achieve specific functionalities through intricate combinations of several primitives. These developments have expanded significantly the scope of potential applications of EasyCrypt, as reflected in our recent formalization of secure function evaluation and verifiable computation. Moreover, they have enabled the formalization of examples that were previously out of scope, for instance modular proofs of security for key-exchange protocols.

imdea.png inria.png EasyCrypt is being developed jointly by the Computer-Aided Cryptography Group? at the IMDEA Software Institute and by Inria.


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

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 (version 1.0) is still being actively 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


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 @ In any other case, use the EasyCrypt club mailing list: our answers to you may also help others.



  • Miguel Ambrona
  • Giuseppe Guagliardo

Former members

Cécile Baritel-Ruet, Simón Cancela-Díaz, Juan Manuel Crespo, Lavinia Damian, Guillaume Davy, Thomas Espitau, Edvard Fagerholm, Guido Genzone, Daniel Hedin, Sylvain Heraud, César Kunz, Martin Moreau, Federico Olmedo, Anne Pacalet, Guillermo Ramos, 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.