Overview Related tools People Publications

Overview

As cryptographic proofs have become essentially unverifiable, cryptographers have argued in favor of computer-aided proofs. CertiCrypt is a toolset that assists the construction and verification of cryptographic proofs; it supports common patterns of reasoning in cryptography, and has been used successfully to prove the security of many constructions, including encryption and digital signature schemes, zero-knowledge protocols, and hash functions. An extension of CertiCrypt supports reasoning about differential privacy.

CertiCrypt takes a language-based approach to cryptography: security goals and assumptions are expressed by means of probabilistic programs. In a similar way, adversarial models are specified in terms of complexity classes, e.g. probabilistic polynomial-time programs. This code-centric view leads to statements that are amenable to formalization and tool-assisted verification. CertiCrypt provides a rich set of verification techniques for probabilistic programs, including equational theories of observational equivalence, a probabilistic relational Hoare logic, certified program transformations, and techniques widely used in cryptographic proofs such as eager/lazy sampling and failure events.

Certicrypt is a fully machine-checked framework built on top of the Coq proof assistant. It is based on a deep embedding of an extensible probabilistic imperative programming language and a formalization of probabilistic polynomial-time programs. Verification methods are implemented in Coq, and proved correct w.r.t. program semantics.

People

The CertiCrypt project was joint between IMDEA Software Institute and INRIA Sophia-Antipolis Méditerranée.

Former contributors:

Publications

Journal Articles

  1. G. Barthe, B. Köpf, F. Olmedo, and S. Zanella-Béguelin. Probabilistic Relational Reasoning for Differential Privacy. In ACM Trans. Program. Lang. Syst., ACM, 2013. To appear.
    [ BibTeX | PDF ]
  2. G. Barthe, B. Grégoire, S. Heraud, F. Olmedo, and S. Zanella-Béguelin. Verified Indifferentiable Hashing into Elliptic Curves. In Journal of Computer Security., IOS Press, 2013. To appear.
    [ BibTeX | PDF ]
  3. G. Barthe, B. Grégoire, S. Zanella-Béguelin. Formal Certification of Code-Based Cryptographic Proofs. Under review.
    [ BibTeX | PDF ]

Peer-Reviewed Conference Papers

  1. G. Barthe and F. Olmedo. Beyond Differential Privacy: Composition Theorems and Relational Logic for f-divergences between Probabilistic Programs. In 40th International Colloquium on Automata, Languages and Programming, ICALP 2013. To appear.
    [ BibTeX | PDF ]
  2. 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 ]
  3. 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 ]
  4. 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 ]
  5. 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 ]
  6. 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 ]
  7. 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 ]
  8. 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 ]
  9. 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 ]
  10. 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, 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 ]

Acknowledgments

This work was partially funded by INRIA-Microsoft Research Joint Centre, French ANR project SCALP, European Project FP7-229599 AMAROUT, Spanish project TIN2009-14599 DESAFIOS 10, and Madrid Regional project S2009TIC-1465 PROMETIDOS.