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 engineer at Olvid
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 , JCS 2013
Gilles Barthe, Benjamin Gregoire, Sylvain Heraud, Federico Olmedo, Santiago Zanella Béguelin
In Journal of Computer Security , JCS 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
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]
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
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 Proceedings of the 23rd IEEE Computer Security Foundations Symposium, CSF 2010
Gilles Barthe, Benjamin Gregoire, Daniel 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 Barthe, Benjamin Gregoire, Sylvain Heraud, Anne Pacalet, Cesar Kunz
In Formal Methods and Software Engineering, 11th International Conference on Formal Engineering Methods,ICFEM, 2009
Gilles Barthe, Benjamin Gregoire, Sylvain Heraud, Anne Pacalet, Cesar 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 Barthe, Benjamin Gregoire, Sylvain Heraud, Santiago Zanella Béguelin
In Formal Aspects in Security and Trust, 5th International Workshop, FAST 2008
Gilles Barthe, Benjamin 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
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
Sylvain Heraud
In Master’s thesis, Université de Nice Sophia Antipolis, INRIA Sophia Antipolis, 2008