[[PageOutline(2-3)]] = !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. {{{#!Fold title="More..." tag=h3 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. }}} {{{#!div style="padding: 0; height: 50px;" [[Image(htdocs:X.png, nolink, 50px, align=right, margin-left=10)]] [[Image(htdocs:imdea.png, nolink, 100px, align=right, margin-left=10)]] [[Image(htdocs:inria.png, nolink, 100px, align=right, margin-left=10)]] !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 == [[Image(https://travis-ci.org/EasyCrypt/easycrypt.svg?branch=1.0, link=https://travis-ci.org/EasyCrypt/easycrypt)]] The current release of !EasyCrypt (version [[milestone:1.0]]) is still under development. Please join the [https://lists.gforge.inria.fr/mailman/listinfo/easycrypt-club EasyCrypt club mailing list] to be informed of evolutions. You can get !EasyCrypt via our public git repository ([https://www.easycrypt.info/trac/browser browse]): git clone !https://github.com/EasyCrypt/easycrypt.git Installation instructions can be found in the [source:README.md@1.0 README] file, and some tutorial material is [wiki:Tutorial available], as well as a [[https://www.easycrypt.info/documentation/refman.pdf|reference manual]] (under development). Note that the current release of !EasyCrypt is still being developed. We do not guarantee backwards compatibility. == Events == - [https://gdr-school.sciencesconf.org/ Cyber in Saclay -- Winter School in Cybersecurity], 8-12 Feb 2021. You can [[SchoolScalay21|download]] the !EasyCrypt material. == Past Events == - The [wiki:SchoolUMD2015 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 [[SchoolParis14|download]] the !EasyCrypt material) - [wiki:SchoolUPen2013 First EasyCrypt summer school and workshop]: July 2013, UPenn. == Contact == Support for installing and using !EasyCrypt can be obtained through the [https://lists.gforge.inria.fr/mailman/listinfo/easycrypt-club EasyCrypt club mailing list]. To file bug reports and suggest enhancements to our tools, please use our [https://www.easycrypt.info/trac/report tracker]. You can log into the tracker using any [[https://github.com|GitHub]] account. Support requests that include ''clearly marked'' non-public information can be sent to support @ easycrypt.info. '''In any other case''', use the [https://lists.gforge.inria.fr/mailman/listinfo/easycrypt-club EasyCrypt club mailing list]: our answers to you may also help others. == People == - [http://software.imdea.org/~gbarthe/ Gilles Barthe] (IMDEA Software Institute) - [http://fdupress.net François Dupressoir] (University of Bristol) - [http://www-sop.inria.fr/everest/Benjamin.Gregoire/ Benjamin Grégoire] (Inria Sophia-Antipolis Méditerranée) - [http://alleystoughton.us/ Alley Stoughton] (Boston University) - [http://strub.nu/ Pierre-Yves Strub] (École Polytechnique) === Students === - Cécile Baritel-Ruet (Inria Sophia-Antipolis Méditerranée) - Antoine Séré (École Polytechnique) === Former members === Miguel Ambrona, Simón Cancela-Díaz, [http://software.imdea.org/~jmcrespo/ Juan Manuel Crespo], Lavinia Damian, Guillaume Davy, Thomas Espitau, [http://www.math.upenn.edu/~edvardf/teaching.html Edvard Fagerholm], Guido Genzone, Giuseppe Guagliardo, Daniel Hedin, [http://www.sylvainheraud.fr/research/ Sylvain Heraud], [http://software.imdea.org/~ckunz/ César Kunz], Martin Moreau, [http://software.imdea.org/people/federico.olmedo/ Federico Olmedo], [http://anne.pacalet.fr/ Anne Pacalet], Guillermo Ramos, [http://www.beschmi.net Benedikt Schmidt], Clément Sartori, Léo Stefanesco, [http://research.microsoft.com/people/santiago/ Santiago Zanella-Béguelin],