|
[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 ]
|
