Formal Certification of ElGamal Encryption. - Gilles Barthe; Benjamin Grégoire; Sylvain Heraud; Santiago Zanella-Béguelin (Formal Aspects in Security and Trust, 2008)

Implementing a Direct Method for Certificate Translation. - Gilles Barthe; Benjamin Grégoire; Sylvain Heraud; César Kunz; Anne Pacalet (ICFEM, 2009)

A Machine-Checked Formalization of Sigma-Protocols. - Gilles Barthe; Daniel Hedin; Santiago Zanella-Béguelin; Benjamin Grégoire; Sylvain Heraud (CSF, 2010)

Computer-Aided Security Proofs for the Working Cryptographer. - Gilles Barthe; Benjamin Grégoire; Sylvain Heraud; Santiago Zanella-Béguelin (CRYPTO, 2011)

A Formalization of Polytime Functions. - Sylvain Heraud; David Nowak (ITP, 2011)

Vérification semi-automatique de primitives cryptographiques. (Semi-automatic verification of cryptographic primitives). - Sylvain Heraud (2012)

Verified indifferentiable hashing into elliptic curves. - Gilles Barthe; Benjamin Grégoire; Sylvain Heraud; Federico Olmedo; Santiago Zanella-Béguelin (J. Comput. Secur., 2013)