[[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.

=== !EasyCrypt 0.2 ===

You can also download
[[http://old.easycrypt.info/easycrypt-0.2.tgz|EasyCrypt version 0.2]]
and its
[[http://old.easycrypt.info/easycrypt-0.2.pdf|documentation]].
However, we are no longer actively supporting this version,
and recommend switching to version 1.0.

== 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 Surrey)
- [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)
- Clément Sartori (É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],
Léo Stefanesco,
[http://research.microsoft.com/people/santiago/ Santiago Zanella-Béguelin],