Sylvain Heraud

I was a PhD student in the Marelle team at INRIA Sophia-Antipolis. My advisor is Benjamin Gregoire. I worked on verification of cryptographic proofs in the Coq proof assistant with CertiCrypt and EasyCrypt. I was involved in SCALP Project. 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 BartheBenjamin Gregoire, Sylvain Heraud, Federico OlmedoSantiago Zanella Béguelin
In Journal of Computer Security , JCS 2013


Papers

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

Computer-Aided Security Proofs for the Working Cryptographer
Gilles BartheBenjamin 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 BartheBenjamin GregoireDaniel Hedin, Sylvain Heraud, Santiago Zanella Béguelin
In Proceedings of the 23rd IEEE Computer Security Foundations Symposium, CSF 2010

Implementing a Direct Method for Certificate Translation
Gilles BartheBenjamin Gregoire, Sylvain Heraud, Anne PacaletCesar Kunz
In Formal Methods and Software Engineering, 11th International Conference on Formal Engineering Methods,ICFEM2009

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


Thesis

Verification Semi-automatique de primitives cryptographiques
Sylvain Heraud
In PhD’s thesis, Université de Nice Sophia Antipolis, INRIA Sophia Antipolis, 2012

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

Using Format