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,ICFEM, 2009
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
Back to Top