Version 29 (modified by Pierre-Yves Strub, 5 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.


See our dedicated page? for a list of related publications.


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 here?.

Note that the current release of EasyCrypt (version 1.0) is still under development. You can also download EasyCrypt version 0.2 (and its documentation) However, we are not actively supporting this version any longer, and recommend switching to version 1.0.

Past Events


You can contact the developers by sending an email to the EasyCrypt support mailing list. However, we encourage you to use the EasyCrypt club mailing list for general questions.

Related tools

  • CertiCrypt is a fully machine-checked framework for building and verifying game-based cryptographic proofs in the Coq proof assistant. The original version of EasyCrypt featured a mechanism for compiling EasyCrypt scripts into CertiCrypt proofs. This mechanism is currently disabled. For additional information, visit the CertiCrypt website. CertiCrypt was developed actively from 2006 until
    1. Its latest stable version can be obtained from us upon request.
  • ZKCrypt is a cryptographic compiler that outputs Java and C implementations of zero-knowledge protocols from high-level specifications, together with EasyCrypt proofs of their correctness.
  • ZooCrypt? is an automated tool for analyzing the security of padding-based public-key encryption schemes (i.e. schemes built from trapdoor permutations and hash functions). ZooCrypt includes an experimental mechanism to generate EasyCrypt proofs of security of analyzed schemes.