Articles in refereed journals and refereed book chapters

[1] Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Federico Olmedo, and Santiago Zanella Béguelin. Verified indifferentiable hashing into elliptic curves. Journal of Computer Security, 21(6):881-917, 2013. [ bib ]
[2] Benjamin Grégoire. Recent advances in the formal verification of cryptographic systems: Turing's legacy. ERCIM News, 2012(91), 2012. [ bib ]
[3] Jan Olaf Blech and Benjamin Grégoire. Certifying compilers using higher-order theorem provers as certificate checkers. Formal Methods in System Design, 38(1):33-61, 2011. [ bib ]
[4] Gilles Barthe, Benjamin Grégoire, and Colin Riba. A tutorial on type-based termination. Book chapter, LERNET 2008 Summer School, 2008. [ bib | .pdf ]
[5] Gilles Barthe, Benjamin Grégoire, and Tamara Rezk. Compilation of certificates. Formal Logical Methods for System Security and Correctness, IOS Press, 2008. [ bib | .pdf ]
[6] Gilles Barthe, Benjamin Grégoire, César Kunz, and Tamara Rezk. Certificate translation for optimizing compilers. Journal of Transactions on Programming Languages and Systems (TOPLAS), 2008. [ bib | .pdf ]

Articles in refereed conferences and workshops

[1] Gilles Barthe, Cédric Fournet, Benjamin Grégoire, Pierre-Yves Strub, Nikhil Swamy, and Santiago Zanella Béguelin. Probabilistic relational verification for cryptographic implementations. In Suresh Jagannathan and Peter Sewell, editors, POPL, pages 193-206. ACM, 2014. [ bib ]
[2] Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Yassine Lakhnech, Benedikt Schmidt, and Santiago Zanella Béguelin. Fully automated analysis of padding-based encryption in the computational model. In Ahmad-Reza Sadeghi, Virgil D. Gligor, and Moti Yung, editors, ACM Conference on Computer and Communications Security, pages 1247-1260. ACM, 2013. [ bib ]
[3] Gilles Barthe, George Danezis, Benjamin Grégoire, César Kunz, and Santiago Zanella Béguelin. Verified computational differential privacy with applications to smart metering. In CSF, pages 287-301. IEEE, 2013. [ bib ]
[4] Gilles Barthe, Benjamin Grégoire, César Kunz, Yassine Lakhnech, and Santiago Zanella Béguelin. Automation in computer-aided cryptography: Proofs, attacks and designs. In Chris Hawblitzel and Dale Miller, editors, CPP, volume 7679 of Lecture Notes in Computer Science, pages 7-8. Springer, 2012. [ bib ]
[5] Michael Backes, Gilles Barthe, Matthias Berg, Benjamin Grégoire, César Kunz, Malte Skoruppa, and Santiago Zanella Béguelin. Verified security of merkle-damgård. In Stephen Chong, editor, CSF, pages 354-368. IEEE, 2012. [ bib ]
[6] Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, and Santiago Zanella Béguelin. Computer-aided cryptographic proofs. In Lennart Beringer and Amy P. Felty, editors, ITP, volume 7406 of Lecture Notes in Computer Science, pages 11-27. Springer, 2012. [ bib ]
[7] Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Federico Olmedo, and Santiago Zanella Béguelin. Verified indifferentiable hashing into elliptic curves. In Pierpaolo Degano and Joshua D. Guttman, editors, POST, volume 7215 of Lecture Notes in Computer Science, pages 209-228. Springer, 2012. [ bib ]
[8] Gilles Barthe, Benjamin Grégoire, and Santiago Zanella Béguelin. Computer-aided cryptographic proofs. In Antoine Miné and David Schmidt, editors, SAS, volume 7460 of Lecture Notes in Computer Science, pages 1-2. Springer, 2012. [ bib ]
[9] Benjamin Grégoire, Loïc Pottier, and Laurent Théry. Proof certificates for algebra and their application to automatic geometry theorem proving. In Automated Deduction in Geometry - 7th International Workshop, ADG 2008, Shanghai, China, September 22-24, 2008. Revised Papers, volume 6301 of Lecture Notes in Computer Science, pages 42-59. Springer, 2011. [ bib ]
[10] Mathieu Boespflug, Maxime Dénès, and Benjamin Grégoire. Full reduction at full throttle. In First International Conference on Certified Programs and Proofs, Tawain, December 7-9, Lecture Notes in Computer Science. Springer, 2011. [ bib ]
[11] Michael Armand, Germain Faure, Benjamin Grégoire, Chantal Keller, Laurent Théry, and Benjamin Werner. A modular integration of sat/smt solvers to coq through proof witnesses. In First International Conference on Certified Programs and Proofs, Tawain, December 7-9, Lecture Notes in Computer Science. Springer, 2011. To Appear. [ bib ]
[12] Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, and Santiago Zanella Béguelin. Computer-aided security proofs for the working cryptographer. In Advances in Cryptology - CRYPTO 2011 - 31st Annual Cryptology Conference, Santa Barbara, CA, USA, August 14-18, 2011. Proceedings, volume 6841 of Lecture Notes in Computer Science, pages 71-90. Springer, 2011. Best Paper Award. [ bib ]
[13] Gilles Barthe, Benjamin Grégoire, Yassine Lakhnech, and Santiago Zanella Béguelin. Beyond provable security verifiable ind-cca security of oaep. In Topics in Cryptology - CT-RSA 2011 - The Cryptographers' Track at the RSA Conference 2011, San Francisco, CA, USA, February 14-18, 2011. Proceedings, volume 6558, pages 180-196. Springer, 2011. [ bib ]
[14] Benjamin Grégoire and Jorge Luis Sacchini. On strong normalization of the calculus of constructions with type-based termination. In Logic for Programming, Artificial Intelligence, and Reasoning - 17th International Conference, LPAR-17, Yogyakarta, Indonesia, October 10-15, 2010. Proceedings, pages 333-347. Springer, 2010. [ bib ]
[15] Michaël Armand, Benjamin Grégoire, Arnaud Spiwack, and Laurent Théry. Extending coq with imperative features and its application to sat verication. In Interactive Theorem Proving, international Conference, ITP 2010, Edinburgh, Scotland, July 11-14, 2010, Proceedings, Lecture Notes in Computer Science. Springer, 2010. [ bib ]
[16] Gilles Barthe, Benjamin Grégoire, and Santiago Zanella. Programming language techniques for cryptographic proofs. In Interactive Theorem Proving, international Conference, ITP 2010, Edinburgh, Scotland, July 11-14, 2010, Proceedings, Lecture Notes in Computer Science. Springer, 2010. [ bib ]
[17] Santiago Zanella Béguelin, Gilles Barthe, Sylvain Heraud, Benjamin Grégoire, and Daniel Hedin. A machine-checked formalization of sigma-protocols. In Computer Security Foundations Symposium, CSF 2010, Edinburgh, Scotland, July 17-19, 2010, Proceedings. IEEE, 2010. [ bib ]
[18] Jan Olaf Blech and Benjamin Grégoire. Using checker predicates in certifying code generation. In Proceedinfs of the Workshop Compiler Optimization meets Compiler Verification (COCV 2009). ENTCS, 2009. To appear. [ bib ]
[19] Gilles Barthe, Benjamin Grégoire, and Santiago Zanella. Formal certification of code-based cryptographic proofs. In 36th symposium Principles of Programming Languages. ACM Press, January 2009. [ bib | .pdf ]
[20] G. Barthe, B. Grégoire, F. Olmedo, and S. Zanella Béguelin. Formally certifying the security of digital signature schemes. In 30th IEEE Symposium on Security and Privacy, S&P 2009, 2009. [ bib ]
[21] Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Cesar Kunz, and Anne Pacalet. Implementing a direct method for certificate translation. In International Conference on Formal Engineering Methods, ICFEM 2009, Lectures Notes in Computer Science, 2009. To appear. [ bib ]
[22] Bruno Barras, Pierre Corbineau, Benjamin Grégoire, Hugo Herbelin, and Jorge Luis Sacchini. A new elimination rule for the Calculus of Inductive Constructions. In S. Berardi, F. Damiani, and U de'Liguoro, editors, Types for proofs and programs 2008, volume 5497 of Lecture Notes in Computer Science, pages 32-48. Springer, 2009. [ bib ]
[23] Jan Olaf Blech and Benjamin Grégoire. Certifying code generation with coq. In Proceedinfs of the Workshop Compiler Optimization meets Compiler Verification (COCV 2008). ENTCS, 2008. [ bib ]
[24] Gilles Barthe, Benjamin Grégoire, and Mariela Pavlova. Preservation of proof obligations from java to the java virtual machine. In Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings, Lecture Notes in Computer Science, pages 83-99. Springer, 2008. [ bib ]
[25] Gilles Barthe, Benjamin Grégoire, and Colin Riba. Type-based termination with sized products. In 17th EACSL Annual Conference on Computer Science Logic, 15th-19th September 2008, Bertinoro, Italy, Lecture Notes in Computer Science. Springer, 2008. [ bib ]
[26] Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, and Santiago Zanella Béguelin. Formal certification of elgamal encryption. In Formal Aspects in Security and Trust, pages 1-19, 2008. [ bib ]
[27] Gilles Barthe, Pierre Crégut, Benjamin Grégoire, Thomas Jensen, and David Pichardie. The mobius proof carrying code infrastructure. In Formal Methods for Components and Objects, 6th International Symposium, FMCO 2007, Amsterdam, The Netherlands, 2007, Revised Lectures, Lecture Notes in Computer Science. Springer, 2007. [ bib ]
[28] Benjamin Grégoire and Jorge Luis Sacchini. Combining a verification condition generator for a bytecode language with static analyses. In Trustworthy Global Computing, Third Symposium, TGC 2007, Sophia-Antipolis, France, November 5-6, 2007, Revised Selected Papers, volume 4912 of Lecture Notes in Computer Science, pages 23-40. Springer, 2007. [ bib ]
[29] Benjamin Grégoire, Laurent Théry, and Benjamin Werner. A computational approach to pocklington certificates in type theory. In Functional and Logic Programming, 8th International Symposium, FLOPS 2006, Fuji-Susono, Japan, April 24-26, 2006, Proceedings, volume 3945 of Lecture Notes in Computer Science, pages 97-113. Springer, 2006. [ bib ]
[30] Gilles Barthe, Lilian Burdy, Julien Charles, Benjamin Grégoire, Marieke Huisman, Jean-Louis Lanet, Mariela Pavlova, and Antoine Requet. Jack - a tool for validation of security and behaviour of java applications. In Formal Methods for Components and Objects, 5th International Symposium, FMCO 2006, Amsterdam, The Netherlands, November 7-10, 2006, Revised Lectures, volume 4709 of Lecture Notes in Computer Science, pages 152-174. Springer, 2006. [ bib ]
[31] Benjamin Grégoire and Laurent Théry. A purely functional library for modular arithmetic and its application to certifying large prime numbers. In Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, volume 4130 of Lecture Notes in Computer Science, pages 423-437. Springer, 2006. [ bib ]
[32] Gilles Barthe, Benjamin Grégoire, and Fernando Pastawski. Cic: Type-based termination of recursive definitions in the calculus of inductive constructions. In Logic for Programming, Artificial Intelligence, and Reasoning, 13th International Conference, LPAR 2006, Phnom Penh, Cambodia, November 13-17, 2006, Proceedings, volume 4246 of Lecture Notes in Computer Science, pages 257-271. Springer, 2006. [ bib ]
[33] Gilles Barthe, Benjamin Grégoire, César Kunz, and Tamara Rezk. Certificate translation for optimizing compilers. In Static Analysis, 13th International Symposium, SAS 2006, Seoul, Korea, August 29-31, 2006, Proceedings, volume 4134 of Lecture Notes in Computer Science, pages 301-317. Springer, 2006. [ bib ]
[34] Gilles Barthe, Lennart Beringer, Pierre Crégut, Benjamin Grégoire, Martin Hofmann, Peter Müller, Erik Poll, Germán Puebla, Ian Stark, and Eric Vétillard. Mobius: Mobility, ubiquity, security. In Trustworthy Global Computing, Second Symposium, TGC 2006, Lucca, Italy, November 7-9, 2006, Revised Selected Papers, volume 4661 of Lecture Notes in Computer Science, pages 10-29. Springer, 2006. [ bib ]
[35] Gilles Barthe, Benjamin Grégoire, and Fernando Pastawski. Practical inference for type-based termination in a polymorphic setting. In Typed Lambda Calculi and Applications, 7th International Conference, TLCA 2005, Nara, Japan, April 21-23, 2005, Proceedings, volume 3461 of Lecture Notes in Computer Science, pages 71-85. Springer, 2005. [ bib ]
[36] Benjamin Grégoire and Assia Mahboubi. Proving equalities in a commutative ring done right in coq. In Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, Oxford, UK, August 22-25, 2005, Proceedings, volume 3603 of Lecture Notes in Computer Science, pages 98-113. Springer, 2005. [ bib ]
[37] Bruno Barras and Benjamin Grégoire. On the role of type decorations in the calculus of inductive constructions. In Computer Science Logic, 19th International Workshop, CSL 2005, 14th Annual Conference of the EACSL, Oxford, UK, August 22-25, 2005, Proceedings, volume 3634 of Lecture Notes in Computer Science, pages 151-166. Springer, 2005. [ bib ]
[38] Yves Bertot, Benjamin Grégoire, and Xavier Leroy. A structured approach to proving compiler optimizations based on dataflow analysis. In Types for Proofs and Programs, International Workshop, TYPES 2004, Jouy-en-Josas, France, December 15-18, 2004, Revised Selected Papers, volume 3839 of Lecture Notes in Computer Science, pages 66-81. Springer, 2004. [ bib ]
[39] Benjamin Grégoire and Xavier Leroy. A compiled implementation of strong reduction. In International Conference on Functional Programming 2002, pages 235-246. ACM Press, 2002. [ bib ]

Dissertations

[1] B. Grégoire. Compilation des termes de preuves: un (nouveau) mariage entre Coq et Ocaml. Thése de doctorat, spécialité informatique, Université Paris 7, école Polytechnique, France, December 2003. [ bib | .ps.gz ]

>Editions

[1] Gilles Barthe, Benjamin Grégoire, Marieke Huisman, and Jean-Louis Lanet, editors. Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, Second International Workshop, CASSIS 2005, Nice, France, March 8-11, 2005, Revised Selected Papers, volume 3956 of Lecture Notes in Computer Science. Springer, 2006. [ bib ]