wiki:WikiStart

Version 13 (modified by Pierre-Yves Strub, 6 years ago) (diff)

--

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. EasyCrypt can also be used for reasoning about (vanilla, approximate, and computational) differential privacy.

EasyCrypt has been used to prove the security of emblematic cryptographic constructions, including the Cramer-Shoup cryptosystem, the OAEP padding scheme, the Full Domain Hash signature scheme, the Merkle-Damgård hash function design, and the CBC block cipher mode of operation.

Downloads

You can get EasyCrypt via our public git repository:

git clone http://ci.easycrypt.info/easycrypt.git

Installation instructions can be found here?.

Events

Contact

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

People

Former contributors

  • Guido Genzone (U. Nacional de Rosario, Argentina)
  • Daniel Hedin (Chalmers University of Technology, Sweden)
  • Sylvain Heraud (Prove & Run)
  • Anne Pacalet (SafeRiver)
  • Adrian Silveira (U. de la República, Uruguay)

Acknowledgments

The research is partially funded by ONR Grant N000141210914, Spanish project TIN2009-14599 DESAFIOS 10, and Madrid Regional project S2009TIC-1465 PROMETIDOS.

Publications

Journal Articles

BibRefList(Barthe:2013:TOPLAS,Barthe:2013:JCS,Barthe:2010)?

Peer-Reviewed Conference Papers

BibRefList(Barthe:2013:CCS,Almeida:2013:CCS,Barthe:2013:ICALP,Barthe:2013:CSF,Barthe:2012:CCS,Almeida:2012:CCS,Backes:2012:CSF,Barthe:2012:POST,Zanella:2012:POPL,Barthe:2011:ProvSec,Barthe:2011:CRYPTO,Barthe:2011:RSA,Barthe:2010:CSF,Barthe:2010:ITP,Barthe:2009:SP,Barthe:2009:POPL)?

Invited Papers

BibRefList(Barthe:2012:ITP,Barthe:2012:CPP,Barthe:2012:MPC,Barthe:2012:SAS,Barthe:2008:FAST)?

Theses

BibRefList(Zanella:2010:PhD)?