Benjamin Grgoire
Publication record assembled from the DBLP archive of ranked conferences.
Papers indexed
57
Venues
22
Active years
2002–2025
Best venue rank
A*
Where they publish
Papers
57 indexed papers, newest first.
| Year | Venue | Title | Authors |
|---|---|---|---|
| 2025 | ASPLOS | Protecting Cryptographic Code Against Spectre-RSB: (and, in Fact, All Known Spectre Variants). | Santiago Arranz-Olmos, Gilles Barthe, Chitchanok Chuengsatiansup, Benjamin Grgoire, Vincent Laporte, Tiago Oliveira, Peter Schwabe, Yuval Yarom, Zhiyuan Zhang |
| 2025 | CCS | Jazzline: Composable CryptoLine Functional Correctness Proofs for Jasmin Programs. | Jos Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Lionel Blatter, Gustavo Xavier Delerue Marinho Alves, Joo Diogo Duarte, Benjamin Grgoire, Tiago Oliveira, Miguel Quaresma, Pierre-Yves Strub, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang |
| 2024 | CRYPTO | Formally Verifying Kyber - Episode V: Machine-Checked IND-CCA Security and Correctness of ML-KEM in EasyCrypt. | Jos Bacelar Almeida, Santiago Arranz-Olmos, Manuel Barbosa, Gilles Barthe, Franois Dupressoir, Benjamin Grgoire, Vincent Laporte, Jean-Christophe Lchenet, Cameron Low, Tiago Oliveira, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Pierre-Yves Strub |
| 2023 | CPP | Practical and Sound Equality Tests, Automatically: Deriving eqType Instances for Jasmin's Data Types with Coq-Elpi. | Benjamin Grgoire, Jean-Christophe Lchenet, Enrico Tassi |
| 2023 | CRYPTO | Fixing and Mechanizing the Security Proof of Fiat-Shamir with Aborts and Dilithium. | Manuel Barbosa, Gilles Barthe, Christian Doczkal, Jelle Don, Serge Fehr, Benjamin Grgoire, Yu-Hsuan Huang, Andreas Hlsing, Yi Lee, Xiaodi Wu |
| 2023 | CRYPTO | Machine-Checked Security for rmXMSS as in RFC 8391 and $\mathrm {SPHINCS^{+}} $. | Manuel Barbosa, Franois Dupressoir, Benjamin Grgoire, Andreas Hlsing, Matthias Meijers, Pierre-Yves Strub |
| 2023 | SP | Typing High-Speed Cryptography against Spectre v1. | Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grgoire, Vincent Laporte, Tiago Oliveira, Swarn Priya, Peter Schwabe, Lucas Tabary-Maujean |
| 2022 | CCS | Enforcing Fine-grained Constant-time Policies. | Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grgoire, Vincent Laporte, Swarn Priya |
| 2021 | CCS | EasyPQC: Verifying Post-Quantum Cryptography. | Manuel Barbosa, Gilles Barthe, Xiong Fan, Benjamin Grgoire, Shih-Han Hung, Jonathan Katz, Pierre-Yves Strub, Xiaodi Wu, Li Zhou |
| 2021 | CCS | Mechanized Proofs of Adversarial Complexity and Application to Universal Composability. | Manuel Barbosa, Gilles Barthe, Benjamin Grgoire, Adrien Koutsos, Pierre-Yves Strub |
| 2021 | CCS | Structured Leakage and Applications to Cryptographic Constant-Time and Cost. | Gilles Barthe, Benjamin Grgoire, Vincent Laporte, Swarn Priya |
| 2021 | SP | High-Assurance Cryptography in the Spectre Era. | Gilles Barthe, Sunjay Cauligi, Benjamin Grgoire, Adrien Koutsos, Kevin Liao, Tiago Oliveira, Swarn Priya, Tamara Rezk, Peter Schwabe |
| 2020 | SP | The Last Mile: High-Assurance and High-Speed Cryptographic Implementations. | Jos Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grgoire, Adrien Koutsos, Vincent Laporte, Tiago Oliveira, Pierre-Yves Strub |
| 2019 | CCS | Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3. | Jos Bacelar Almeida, Ccile Baritel-Ruet, Manuel Barbosa, Gilles Barthe, Franois Dupressoir, Benjamin Grgoire, Vincent Laporte, Tiago Oliveira, Alley Stoughton, Pierre-Yves Strub |
| 2019 | CCS | A Machine-Checked Proof of Security for AWS Key Management Service. | Jos Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Matthew Campagna, Ernie Cohen, Benjamin Grgoire, Vitor Pereira, Bernardo Portela, Pierre-Yves Strub, Serdar Tasiran |
| 2019 | ESORICS | maskVerif: Automated Verification of Higher-Order Masking in Presence of Physical Defaults. | Gilles Barthe, Sonia Belad, Gatan Cassiers, Pierre-Alain Fouque, Benjamin Grgoire, Franois-Xavier Standaert |
| 2019 | PLDI | FaCT: a DSL for timing-sensitive computation. | Sunjay Cauligi, Gary Soeller, Brian Johannesmeyer, Fraser Brown, Riad S. Wahby, John Renner, Benjamin Grgoire, Gilles Barthe, Ranjit Jhala, Deian Stefan |
| 2018 | CCS | Symbolic Proofs for Lattice-Based Cryptography. | Gilles Barthe, Xiong Fan, Joshua Gancher, Benjamin Grgoire, Charlie Jacomme, Elaine Shi |
| 2018 | ESOP | An Assertion-Based Program Logic for Probabilistic Programs. | Gilles Barthe, Thomas Espitau, Marco Gaboardi, Benjamin Grgoire, Justin Hsu, Pierre-Yves Strub |
| 2018 | EuroCrypt | Masking the GLP Lattice-Based Signature Scheme at Any Order. | Gilles Barthe, Sonia Belad, Thomas Espitau, Pierre-Alain Fouque, Benjamin Grgoire, Mlissa Rossi, Mehdi Tibouchi |
| 2017 | CCS | Jasmin: High-Assurance and High-Speed Cryptography. | Jos Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Arthur Blot, Benjamin Grgoire, Vincent Laporte, Tiago Oliveira, Hugo Pacheco, Benedikt Schmidt, Pierre-Yves Strub |
| 2017 | CCS | A Fast and Verified Software Stack for Secure Function Evaluation. | Jos Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Franois Dupressoir, Benjamin Grgoire, Vincent Laporte, Vitor Pereira |
| 2017 | EuroCrypt | Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model. | Gilles Barthe, Franois Dupressoir, Sebastian Faust, Benjamin Grgoire, Franois-Xavier Standaert, Pierre-Yves Strub |
| 2017 | LPAR | Proving uniformity and independence by self-composition and coupling. | Gilles Barthe, Thomas Espitau, Benjamin Grgoire, Justin Hsu, Pierre-Yves Strub |
| 2017 | POPL | Coupling proofs are probabilistic product programs. | Gilles Barthe, Benjamin Grgoire, Justin Hsu, Pierre-Yves Strub |
| 2016 | CCS | Strong Non-Interference and Type-Directed Higher-Order Masking. | Gilles Barthe, Sonia Belad, Franois Dupressoir, Pierre-Alain Fouque, Benjamin Grgoire, Pierre-Yves Strub, Rbecca Zucchini |
| 2016 | CCS | Advanced Probabilistic Couplings for Differential Privacy. | Gilles Barthe, Nomie Fong, Marco Gaboardi, Benjamin Grgoire, Justin Hsu, Pierre-Yves Strub |
| 2016 | ICALP | A Program Logic for Union Bounds. | Gilles Barthe, Marco Gaboardi, Benjamin Grgoire, Justin Hsu, Pierre-Yves Strub |
| 2016 | LICS | Proving Differential Privacy via Probabilistic Couplings. | Gilles Barthe, Marco Gaboardi, Benjamin Grgoire, Justin Hsu, Pierre-Yves Strub |
| 2015 | CCS | Automated Proofs of Pairing-Based Cryptography. | Gilles Barthe, Benjamin Grgoire, Benedikt Schmidt |
| 2015 | EuroCrypt | Verified Proofs of Higher-Order Masking. | Gilles Barthe, Sonia Belad, Franois Dupressoir, Pierre-Alain Fouque, Benjamin Grgoire, Pierre-Yves Strub |
| 2015 | LPAR | Relational Reasoning via Probabilistic Coupling. | Gilles Barthe, Thomas Espitau, Benjamin Grgoire, Justin Hsu, Lo Stefanesco, Pierre-Yves Strub |
| 2014 | CCS | Synthesis of Fault Attacks on Cryptographic Implementations. | Gilles Barthe, Franois Dupressoir, Pierre-Alain Fouque, Benjamin Grgoire, Jean-Christophe Zapalowicz |
| 2014 | CHES | Making RSA-PSS Provably Secure against Non-random Faults. | Gilles Barthe, Franois Dupressoir, Pierre-Alain Fouque, Benjamin Grgoire, Mehdi Tibouchi, Jean-Christophe Zapalowicz |
| 2014 | POPL | Probabilistic relational verification for cryptographic implementations. | Gilles Barthe, Cdric Fournet, Benjamin Grgoire, Pierre-Yves Strub, Nikhil Swamy, Santiago Zanella-Bguelin |
| 2013 | CCS | Fully automated analysis of padding-based encryption in the computational model. | Gilles Barthe, Juan Manuel Crespo, Benjamin Grgoire, Csar Kunz, Yassine Lakhnech, Benedikt Schmidt, Santiago Zanella-Bguelin |
| 2012 | CPP | Automation in Computer-Aided Cryptography: Proofs, Attacks and Designs. | Gilles Barthe, Benjamin Grgoire, Csar Kunz, Yassine Lakhnech, Santiago Zanella-Bguelin |
| 2012 | ITP | Computer-Aided Cryptographic Proofs. | Gilles Barthe, Juan Manuel Crespo, Benjamin Grgoire, Csar Kunz, Santiago Zanella-Bguelin |
| 2012 | MPC | Probabilistic Relational Hoare Logics for Computer-Aided Security Proofs. | Gilles Barthe, Benjamin Grgoire, Santiago Zanella-Bguelin |
| 2012 | SAS | Computer-Aided Cryptographic Proofs. | Gilles Barthe, Benjamin Grgoire, Santiago Zanella-Bguelin |
| 2011 | CPP | A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses. | Michal Armand, Germain Faure, Benjamin Grgoire, Chantal Keller, Laurent Thry, Benjamin Werner |
| 2011 | CPP | Full Reduction at Full Throttle. | Mathieu Boespflug, Maxime Dns, Benjamin Grgoire |
| 2011 | CRYPTO | Computer-Aided Security Proofs for the Working Cryptographer. | Gilles Barthe, Benjamin Grgoire, Sylvain Heraud, Santiago Zanella-Bguelin |
| 2010 | ITP | Extending Coq with Imperative Features and Its Application to SAT Verification. | Michal Armand, Benjamin Grgoire, Arnaud Spiwack, Laurent Thry |
| 2010 | ITP | Programming Language Techniques for Cryptographic Proofs. | Gilles Barthe, Benjamin Grgoire, Santiago Zanella-Bguelin |
| 2010 | LPAR | On Strong Normalization of the Calculus of Constructions with Type-Based Termination. | Benjamin Grgoire, Jorge Luis Sacchini |
| 2009 | ICFEM | Implementing a Direct Method for Certificate Translation. | Gilles Barthe, Benjamin Grgoire, Sylvain Heraud, Csar Kunz, Anne Pacalet |
| 2009 | POPL | Formal certification of code-based cryptographic proofs. | Gilles Barthe, Benjamin Grgoire, Santiago Zanella-Bguelin |
| 2009 | SP | Formally Certifying the Security of Digital Signature Schemes. | Santiago Zanella-Bguelin, Gilles Barthe, Benjamin Grgoire, Federico Olmedo |
| 2008 | CADE | Preservation of Proof Obligations from Java to the Java Virtual Machine. | Gilles Barthe, Benjamin Grgoire, Mariela Pavlova |
| 2008 | CSL | Type-Based Termination with Sized Products. | Gilles Barthe, Benjamin Grgoire, Colin Riba |
| 2006 | CADE | A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers. | Benjamin Grgoire, Laurent Thry |
| 2006 | FLOPS | A Computational Approach to Pocklington Certificates in Type Theory. | Benjamin Grgoire, Laurent Thry, Benjamin Werner |
| 2006 | LPAR | CIC[^( )]: Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions. | Gilles Barthe, Benjamin Grgoire, Fernando Pastawski |
| 2006 | SAS | Certificate Translation for Optimizing Compilers. | Gilles Barthe, Benjamin Grgoire, Csar Kunz, Tamara Rezk |
| 2005 | CSL | On the Role of Type Decorations in the Calculus of Inductive Constructions. | Bruno Barras, Benjamin Grgoire |
| 2002 | ICFP | A compiled implementation of strong reduction. | Benjamin Grgoire, Xavier Leroy |