Research

I was a PhD student in the Marelle team at INRIA Sophia-Antipolis. My advisor was Benjamin Gregoire. I worked on verification of cryptographic proofs in the Coq proof assistant with CertiCrypt and EasyCrypt. My research interests include Verification of Cryptographic Systems, Language-based Security, Semantics of Programming Languages, Theorem Provers, Certificate Translation.

Now I’m research engineer at Prove & Run.

Journal Articles

Verifiable Indifferentiable Hashing into Elliptic Curves
Gilles Barthe, Benjamin Gregoire, Sylvain Heraud, Federico Olmedo, Santiago Zanella Béguelin
In Journal of Computer Security, FCS 2013

Papers

Verifiable Indifferentiable Hashing into Elliptic Curves
Gilles Barthe, Benjamin Gregoire, Sylvain Heraud, Federico Olmedo, Santiago Zanella Béguelin
In 1st Conference on Principles of Security and Trust, POST 2012

Computer-Aided Security Proofs for the Working Cryptographer
Gilles Barthe, Benjamin Gregoire, Sylvain Heraud, Santiago Zanella Béguelin
In 31st International Cryptology Conference, CRYPTO 2011
[Best Paper Award]

A Formalization of Polytime Functions
Sylvain Heraud, David Nowak
In 2nd International Conference on Interactive Theorem Proving, ITP 2011

A Machine-Checked Formalization of Sigma-Protocols
Gilles Barthe, Benjamin Gregoire, Daniel Hedin, Sylvain Heraud, Santiago Zanella Béguelin
In 23rd IEEE Computer Security Foundations Symposium, CSF 2010

Implementing a Direct Method for Certificate Translation
Gilles Barthe, Benjamin Gregoire, Sylvain Heraud, Anne Pacalet, Cesar Kunz
In 11th International Conference on Formal Engineering Methods, ICFEM 2009

Formal certification of ElGamal encryption: A gentle introduction to CertiCrypt
Gilles Barthe, Benjamin Gregoire, Sylvain Heraud, Santiago Zanella Béguelin
In Formal Aspects in Security and Trust, 5th International Workshop, FAST 2008

Thesis

Vérification Semi-automatique de primitives cryptographiques
Gilles Barthe
In PhD’s thesis, Université de Nice Sophia Antipolis, INRIA Sophia Antipolis, 2012

Transformation de preuve pour compilateur optimisant
Gilles Barthe
In Master’s thesis, Université de Nice Sophia Antipolis, INRIA Sophia Antipolis, 2008