Overview Events Downloads Contact Related tools People Publications

We are planning to release a complete reimplementation of EasyCrypt during Spring 2013. Please keep posted, or join the easycrypt-club mailing list to be informed of the new release. Preview tarballs (with limited functionalities) are available on our continuous integration server. Otherwise, download EasyCrypt version 0.2.

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.

Events

The first EasyCrypt summer school and workshop will take place at the University of Pennsylvania between the 16th and 19th of July 2013.

Downloads

Tar.gz archive
EasyCrypt-0.2
PDF document
EasyCrypt-0.2
User guide
Tar.gz archive
Preview release
(nightly builds)

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.

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)

Publications

Journal Articles

  1. G. Barthe, B. Grégoire, S. Zanella-Béguelin. Formal Certification of Code-Based Cryptographic Proofs. Submitted manuscript under review.
    [ BibTeX | PDF ]

Peer-Reviewed Conference Papers

  1. G. Barthe, G. Danezis, B. Grégoire, C. Kunz, and S. Zanella-Béguelin. Verified Computational Differential Privacy with Applications to Smart Metering. In 26th IEEE Computer Security Foundations Symposium, CSF 2013, IEEE Computer Society, 2013. To appear.
    [ BibTeX | PDF ]
  2. G. Barthe, D. Pointcheval, and S. Zanella-Béguelin. Verified Security of Redundancy-Free Encryption from Rabin and RSA. In 19th ACM Conference on Computer and Communications Security, CCS 2012, pages 724-735, ACM, 2012.
    [ BibTeX | PDF | Extended version | URL | Slides]
  3. J. Bacelar Almeida, M. Barbosa, E. Bangerter, G. Barthe, S. Krenn, and S. Zanella-Béguelin. Full Proof Cryptography: Verifiable Compilation of Efficient Zero-Knowledge Protocols. In 19th ACM Conference on Computer and Communications Security, CCS 2012, pages 488-500, ACM, 2012.
    [ BibTeX | PDF | URL ]
  4. M. Backes, G. Barthe, M. Berg, B. Grégoire, C. Kunz, M. Skoruppa, and S. Zanella-Béguelin. Verified security of Merkle-Damgård. In 25th IEEE Computer Security Foundations Symposium, CSF 2012, pages 354-368, IEEE Computer Society, 2012.
    [ BibTeX | PDF | URL | Slides ]
  5. G. Barthe, B. Grégoire, S. Heraud, F. Olmedo, S. Zanella-Béguelin. Verified Indifferentiable Hashing into Elliptic Curves. In 1st International Conference on Principles of Security and Trust, POST 2012, volume 7215 of Lecture Notes in Computer Science, pages 209-228, Springer, 2012.
    [ BibTeX | PDF | URL | Slides ]
  6. G. Barthe, B. Köpf, F. Olmedo, S. Zanella-Béguelin. Probabilistic Relational Reasoning for Differential Privacy. In 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, pages 97-110, ACM, 2012.
    [ BibTeX | PDF | URL | Slides ]
  7. G. Barthe, F. Olmedo, S. Zanella-Béguelin. Verifiable Security of Boneh-Franklin Identity-Based Encryption. In 5th International Conference on Provable Security - ProvSec 2011, volume 6980 of Lecture Notes in Computer Science, pages 68-83, Springer, 2011.
    [ BibTeX | PDF | URL | Slides ]
  8. G. Barthe, B. Grégoire, S. Heraud, S. Zanella-Béguelin. Computer-Aided Security Proofs for the Working Cryptographer. In Advances in Cryptology - CRYPTO 2011, volume 6841 of Lecture Notes in Computer Science, pages 71-90, Springer, 2011.
    Best Paper Award
    [ BibTeX | PDF | URL | Slides]
  9. G. Barthe, B. Grégoire, S. Zanella-Béguelin, Y. Lakhnech. Beyond Provable Security. Verifiable IND-CCA Security of OAEP. In Topics in Cryptology - CT-RSA 2011, volume 6558 of Lecture Notes in Computer Science, pages 180-196, Springer, 2011.
    [ BibTeX | PDF | URL | Slides ]
  10. G. Barthe, D. Hedin, S. Zanella-Béguelin, B. Grégoire, S. Heraud. A Machine-Checked Formalization of Sigma-Protocols. In 23rd IEEE Computer Security Foundations Symposium, CSF 2010, pages 246-260, IEEE Computer Society, 2010.
    [ BibTeX | PDF | URL | Slides ]
  11. G. Barthe, B. Grégoire, S. Zanella-Béguelin. Programming language techniques for cryptographic proofs. In 1st International Conference on Interactive Theorem Proving, ITP 2010, volume 5491 of Lecture Notes in Computer Science, pages 115-130, Springer, 2010.
    [ BibTeX | PDF | URL | Slides ]
  12. S. Zanella-Béguelin, G. Barthe, B. Grégoire, F. Olmedo. Formally certifying the security of digital signature schemes. In 30th IEEE Symposium on Security and Privacy, S&P 2009, pages 237-250, IEEE Computer Society, 2009.
    [ BibTeX | PDF | URL | Slides ]
  13. G. Barthe, B. Grégoire, S. Zanella-Béguelin. Formal certification of code-based cryptographic proofs. In 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, pages 90-101, ACM, 2009.
    [ BibTeX | PDF | URL | Slides ]

Invited Papers

  1. G. Barthe, J. M. Crespo, B. Grégoire, César Kunz, S. Zanella-Béguelin. Computer-Aided Cryptographic Proofs. In 3rd International Conference on Interactive Theorem Proving, ITP 2012, volume 7406 of Lecture Notes in Computer Science, pages 11-27, Springer, 2012.
    [ BibTeX | PDF | URL | Slides ]
  2. G. Barthe, B. Grégoire, C. Kunz, Y. Lakhnech, S. Zanella-Béguelin. Automation in Computer-Aided Cryptography: Proofs, Attacks and Designs In 2nd International Conference on Certified Programs and Proofs, CPP 2012, volume 7697 of Lecture Notes in Computer Science, pages 7-8, Springer, 2012.
    [ BibTeX | PDF | URL | Slides ]
  3. G. Barthe, B. Grégoire, S. Zanella-Béguelin. Probabilistic Relational Hoare Logics for Computer-Aided Security Proofs. In 11th International Conference on Mathematics of Program Construction, MPC 2012, volume 7342 of Lecture Notes in Computer Science, pages 1-6, Springer, 2012.
    [ BibTeX | PDF | URL | Slides ]
  4. G. Barthe, B. Grégoire, S. Zanella-Béguelin. Computer-Aided Cryptographic Proofs. In 19th International Symposium on Static Analysis, SAS 2012, volume 7460 of Lecture Notes in Computer Science, pages 1-2, Springer, 2012.
    [ BibTeX | PDF | URL | Slides ]
  5. G. Barthe, B. Grégoire, S. Heraud, S. Zanella-Béguelin. Formal certification of ElGamal encryption. A gentle introduction to CertiCrypt. In 5th International Workshop on Formal Aspects in Security and Trust, FAST 2008, volume 5491 of Lecture Notes in Computer Science, pages 1-19, Springer, 2009.
    [ BibTeX | PDF | URL ]

Theses

  1. S. Zanella-Béguelin. Formal Certification of Game-Based Cryptographic Proofs. École Nationale Supérieure des Mines de Paris, 2010.
    EAPLS Best PhD Dissertation Award
    [ BibTeX | PDF | URL | Slides ]