Benjamin Grégoire

145 papers A* 26A 13B 16C 1Misc 1Journal 62Unranked 24

Year	Rank	Type	Title / Venue / Authors
2025	J	`jnl`	A Quantitative Probabilistic Relational Hoare Logic. Proc. ACM Program. Lang. Martin Avanzini, Gilles Barthe, Davide Davoli, Benjamin Grégoire
2025	A*	`conf`	Jazzline: Composable CryptoLine Functional Correctness Proofs for Jasmin Programs. CCS José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Lionel Blatter, Gustavo Xavier Delerue Marinho Alves, João Diogo Duarte, Benjamin Grégoire, Tiago Oliveira, Miguel Quaresma, Pierre-Yves Strub, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang
2025	J	`jnl`	Let's DOIT: Using Intel's Extended HW/SW Contract for Secure Compilation of Crypto Code. IACR Cryptol. ePrint Arch. Santiago Arranz-Olmos, Gilles Barthe, Benjamin Grégoire, Jan Jancar, Vincent Laporte, Tiago Oliveira, Peter Schwabe
2025	J	`jnl`	Let's DOIT: Using Intel's Extended HW/SW Contract for Secure Compilation of Crypto Code. IACR Trans. Cryptogr. Hardw. Embed. Syst. Santiago Arranz-Olmos, Gilles Barthe, Benjamin Grégoire, Jan Jancar, Vincent Laporte, Tiago Oliveira, Peter Schwabe
2025	J	`jnl`	Preservation of Speculative Constant-Time by Compilation. Proc. ACM Program. Lang. Santiago Arranz-Olmos, Gilles Barthe, Lionel Blatter, Benjamin Grégoire, Vincent Laporte
2025	—	`conf`	Protecting Cryptographic Code Against Spectre-RSB: (and, in Fact, All Known Spectre Variants). ASPLOS (2) Santiago Arranz-Olmos, Gilles Barthe, Chitchanok Chuengsatiansup, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Peter Schwabe, Yuval Yarom, Zhiyuan Zhang
2025	J	`jnl`	The Jasmin Compiler Preserves Cryptographic Security. CoRR Santiago Arranz-Olmos, Gilles Barthe, Lionel Blatter, Benjamin Grégoire, Vincent Laporte, Paolo Torrini
2024	J	`jnl`	A quantitative probabilistic relational Hoare logic. CoRR Martin Avanzini, Gilles Barthe, Davide Davoli, Benjamin Grégoire
2024	A	`conf`	CV2EC: Getting the Best of Both Worlds. CSF Bruno Blanchet, Pierre Boutry, Christian Doczkal, Benjamin Grégoire, Pierre-Yves Strub
2024	—	`conf`	Formally Verifying Kyber - Episode V: Machine-Checked IND-CCA Security and Correctness of ML-KEM in EasyCrypt. CRYPTO (2) José Bacelar Almeida, Santiago Arranz-Olmos, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Cameron Low, Tiago Oliveira, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Pierre-Yves Strub
2024	J	`jnl`	Formally verifying Kyber Episode V: Machine-checked IND-CCA security and correctness of ML-KEM in EasyCrypt. IACR Cryptol. ePrint Arch. José Bacelar Almeida, Santiago Arranz-Olmos, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Cameron Low, Tiago Oliveira, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Pierre-Yves Strub
2024	J	`jnl`	High-assurance zeroization. IACR Trans. Cryptogr. Hardw. Embed. Syst. Santiago Arranz-Olmos, Gilles Barthe, Ruben Gonzalez, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Tiago Oliveira, Peter Schwabe
2024	J	`jnl`	Hopping Proofs of Expectation-Based Properties: Applications to Skiplists and Security Proofs. Proc. ACM Program. Lang. Martin Avanzini, Gilles Barthe, Benjamin Grégoire, Georg Moser, Gabriele Vanoni
2024	J	`jnl`	Masking the GLP Lattice-Based Signature Scheme at Any Order. J. Cryptol. Gilles Barthe, Sonia Belaïd, Thomas Espitau, Pierre-Alain Fouque, Benjamin Grégoire, Mélissa Rossi, Mehdi Tibouchi
2024	J	`jnl`	Preservation of Speculative Constant-time by Compilation. IACR Cryptol. ePrint Arch. Santiago Arranz-Olmos, Gilles Barthe, Lionel Blatter, Benjamin Grégoire, Vincent Laporte
2024	J	`jnl`	Protecting cryptographic code against Spectre-RSB. IACR Cryptol. ePrint Arch. Santiago Arranz-Olmos, Gilles Barthe, Chitchanok Chuengsatiansup, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Peter Schwabe, Yuval Yarom, Zhiyuan Zhang
2024	—	`book`	Provable Security of Cryptographic Primitives: from Algorithms to Assembly. Benjamin Grégoire
2023	—	`conf`	Fixing and Mechanizing the Security Proof of Fiat-Shamir with Aborts and Dilithium. CRYPTO (5) Manuel Barbosa, Gilles Barthe, Christian Doczkal, Jelle Don, Serge Fehr, Benjamin Grégoire, Yu-Hsuan Huang, Andreas Hülsing, Yi Lee, Xiaodi Wu
2023	J	`jnl`	Fixing and Mechanizing the Security Proof of Fiat-Shamir with Aborts and Dilithium. IACR Cryptol. ePrint Arch. Manuel Barbosa, Gilles Barthe, Christian Doczkal, Jelle Don, Serge Fehr, Benjamin Grégoire, Yu-Hsuan Huang, Andreas Hülsing, Yi Lee, Xiaodi Wu
2023	J	`jnl`	Formally verifying Kyber Episode IV: Implementation correctness. IACR Trans. Cryptogr. Hardw. Embed. Syst. José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Tiago Oliveira, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Antoine Séré, Pierre-Yves Strub
2023	J	`jnl`	Formally verifying Kyber Part I: Implementation Correctness. IACR Cryptol. ePrint Arch. José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Tiago Oliveira, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Antoine Séré, Pierre-Yves Strub
2023	J	`jnl`	High-assurance zeroization. IACR Cryptol. ePrint Arch. Santiago Arranz-Olmos, Gilles Barthe, Ruben Gonzalez, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Tiago Oliveira, Peter Schwabe
2023	J	`jnl`	Machine-Checked Security for $\mathrm{XMSS}$ as in RFC 8391 and $\mathrm{SPHINCS}^{+}$. IACR Cryptol. ePrint Arch. Manuel Barbosa, François Dupressoir, Benjamin Grégoire, Andreas Hülsing, Matthias Meijers, Pierre-Yves Strub
2023	—	`conf`	Machine-Checked Security for rmXMSS as in RFC 8391 and $\mathrm {SPHINCS^{+}} $. CRYPTO (5) Manuel Barbosa, François Dupressoir, Benjamin Grégoire, Andreas Hülsing, Matthias Meijers, Pierre-Yves Strub
2023	J	`jnl`	Mechanized Proofs of Adversarial Complexity and Application to Universal Composability. ACM Trans. Priv. Secur. Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Pierre-Yves Strub
2023	B	`conf`	Practical and Sound Equality Tests, Automatically: Deriving eqType Instances for Jasmin's Data Types with Coq-Elpi. CPP Benjamin Grégoire, Jean-Christophe Léchenet, Enrico Tassi
2023	A*	`conf`	Typing High-Speed Cryptography against Spectre v1. SP Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Swarn Priya, Peter Schwabe, Lucas Tabary-Maujean
2022	A*	`conf`	Enforcing Fine-grained Constant-time Policies. CCS Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Swarn Priya
2022	J	`jnl`	Enforcing fine-grained constant-time policies. IACR Cryptol. ePrint Arch. Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Swarn Priya
2022	J	`jnl`	Typing High-Speed Cryptography against Spectre v1. IACR Cryptol. ePrint Arch. Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Swarn Priya, Peter Schwabe, Lucas Tabary-Maujean
2021	A*	`conf`	EasyPQC: Verifying Post-Quantum Cryptography. CCS Manuel Barbosa, Gilles Barthe, Xiong Fan, Benjamin Grégoire, Shih-Han Hung, Jonathan Katz, Pierre-Yves Strub, Xiaodi Wu, Li Zhou
2021	J	`jnl`	EasyPQC: Verifying Post-Quantum Cryptography. IACR Cryptol. ePrint Arch. Manuel Barbosa, Gilles Barthe, Xiong Fan, Benjamin Grégoire, Shih-Han Hung, Jonathan Katz, Pierre-Yves Strub, Xiaodi Wu, Li Zhou
2021	J	`jnl`	Hardware Private Circuits: From Trivial Composition to Full Verification. IEEE Trans. Computers Gaëtan Cassiers, Benjamin Grégoire, Itamar Levi, François-Xavier Standaert
2021	A*	`conf`	High-Assurance Cryptography in the Spectre Era. SP Gilles Barthe, Sunjay Cauligi, Benjamin Grégoire, Adrien Koutsos, Kevin Liao, Tiago Oliveira, Swarn Priya, Tamara Rezk, Peter Schwabe
2021	J	`jnl`	Masking in Fine-Grained Leakage Models: Construction, Implementation and Verification. IACR Trans. Cryptogr. Hardw. Embed. Syst. Gilles Barthe, Marc Gourjon, Benjamin Grégoire, Maximilian Orlt, Clara Paglialonga, Lars Porth
2021	A*	`conf`	Mechanized Proofs of Adversarial Complexity and Application to Universal Composability. CCS Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Pierre-Yves Strub
2021	J	`jnl`	Mechanized Proofs of Adversarial Complexity and Application to Universal Composability. IACR Cryptol. ePrint Arch. Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Pierre-Yves Strub
2021	A*	`conf`	Structured Leakage and Applications to Cryptographic Constant-Time and Cost. CCS Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Swarn Priya
2021	J	`jnl`	Structured Leakage and Applications to Cryptographic Constant-Time and Cost. IACR Cryptol. ePrint Arch. Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Swarn Priya
2020	J	`jnl`	Formal verification of a constant-time preserving C compiler. Proc. ACM Program. Lang. Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, Alix Trieu
2020	J	`jnl`	Hardware Private Circuits: From Trivial Composition to Full Verification. IACR Cryptol. ePrint Arch. Gaëtan Cassiers, Benjamin Grégoire, Itamar Levi, François-Xavier Standaert
2020	J	`jnl`	High-Assurance Cryptography Software in the Spectre Era. IACR Cryptol. ePrint Arch. Gilles Barthe, Sunjay Cauligi, Benjamin Grégoire, Adrien Koutsos, Kevin Liao, Tiago Oliveira, Swarn Priya, Tamara Rezk, Peter Schwabe
2020	J	`jnl`	Improved parallel mask refreshing algorithms: generic solutions with parametrized non-interference and automated optimizations. J. Cryptogr. Eng. Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, François-Xavier Standaert, Pierre-Yves Strub
2020	J	`jnl`	Masking in Fine-Grained Leakage Models: Construction, Implementation and Verification. IACR Cryptol. ePrint Arch. Gilles Barthe, Marc Gourjon, Benjamin Grégoire, Maximilian Orlt, Clara Paglialonga, Lars Porth
2020	—	`conf`	Security Analysis of ElGamal Implementations. ICETE (2) Mohamad El Laz, Benjamin Grégoire, Tamara Rezk
2020	A*	`conf`	The Last Mile: High-Assurance and High-Speed Cryptographic Implementations. SP José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Vincent Laporte, Tiago Oliveira, Pierre-Yves Strub
2019	A*	`conf`	A Machine-Checked Proof of Security for AWS Key Management Service. CCS José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Matthew Campagna, Ernie Cohen, Benjamin Grégoire, Vitor Pereira, Bernardo Portela, Pierre-Yves Strub, Serdar Tasiran
2019	J	`jnl`	A Machine-Checked Proof of Security for AWS Key Management Service. IACR Cryptol. ePrint Arch. José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Matthew Campagna, Ernie Cohen, Benjamin Grégoire, Vitor Pereira, Bernardo Portela, Pierre-Yves Strub, Serdar Tasiran
2019	A*	`conf`	FaCT: a DSL for timing-sensitive computation. PLDI Sunjay Cauligi, Gary Soeller, Brian Johannesmeyer, Fraser Brown, Riad S. Wahby, John Renner, Benjamin Grégoire, Gilles Barthe, Ranjit Jhala, Deian Stefan
2019	J	`jnl`	Formal Verification of a Constant-Time Preserving C Compiler. IACR Cryptol. ePrint Arch. Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, Alix Trieu
2019	J	`jnl`	Machine-Checked Proofs for Cryptographic Standards. IACR Cryptol. ePrint Arch. José Bacelar Almeida, Cécile Baritel-Ruet, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Alley Stoughton, Pierre-Yves Strub
2019	A*	`conf`	Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3. CCS José Bacelar Almeida, Cécile Baritel-Ruet, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Alley Stoughton, Pierre-Yves Strub
2019	A	`conf`	Symbolic Methods in Computational Cryptography Proofs. CSF Gilles Barthe, Benjamin Grégoire, Charlie Jacomme, Steve Kremer, Pierre-Yves Strub
2019	J	`jnl`	The Last Mile: High-Assurance and High-Speed Cryptographic Implementations. CoRR José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Vincent Laporte, Tiago Oliveira, Pierre-Yves Strub
2019	—	`conf`	maskVerif: Automated Verification of Higher-Order Masking in Presence of Physical Defaults. ESORICS (1) Gilles Barthe, Sonia Belaïd, Gaëtan Cassiers, Pierre-Alain Fouque, Benjamin Grégoire, François-Xavier Standaert
2018	A	`conf`	An Assertion-Based Program Logic for Probabilistic Programs. ESOP Gilles Barthe, Thomas Espitau, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
2018	J	`jnl`	An Assertion-Based Program Logic for Probabilistic Programs. CoRR Gilles Barthe, Thomas Espitau, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
2018	A	`conf`	Formal Security Proof of CMAC and Its Variants. CSF Cécile Baritel-Ruet, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire
2018	J	`jnl`	Improved Parallel Mask Refreshing Algorithms: Generic Solutions with Parametrized Non-Interference & Automated Optimizations. IACR Cryptol. ePrint Arch. Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, François-Xavier Standaert, Pierre-Yves Strub
2018	—	`conf`	Masking the GLP Lattice-Based Signature Scheme at Any Order. EUROCRYPT (2) Gilles Barthe, Sonia Belaïd, Thomas Espitau, Pierre-Alain Fouque, Benjamin Grégoire, Mélissa Rossi, Mehdi Tibouchi
2018	J	`jnl`	Masking the GLP Lattice-Based Signature Scheme at Any Order. IACR Cryptol. ePrint Arch. Gilles Barthe, Sonia Belaïd, Thomas Espitau, Pierre-Alain Fouque, Benjamin Grégoire, Mélissa Rossi, Mehdi Tibouchi
2018	J	`jnl`	Proving expected sensitivity of probabilistic programs. Proc. ACM Program. Lang. Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
2018	A	`conf`	Secure Compilation of Side-Channel Countermeasures: The Case of Cryptographic "Constant-Time". CSF Gilles Barthe, Benjamin Grégoire, Vincent Laporte
2018	A*	`conf`	Symbolic Proofs for Lattice-Based Cryptography. CCS Gilles Barthe, Xiong Fan, Joshua Gancher, Benjamin Grégoire, Charlie Jacomme, Elaine Shi
2018	J	`jnl`	Symbolic Proofs for Lattice-Based Cryptography. IACR Cryptol. ePrint Arch. Gilles Barthe, Xiong Fan, Joshua Gancher, Benjamin Grégoire, Charlie Jacomme, Elaine Shi
2018	—	`conf`	Vectorizing Higher-Order Masking. COSADE Benjamin Grégoire, Kostas Papagiannopoulos, Peter Schwabe, Ko Stoffelen
2018	J	`jnl`	Vectorizing Higher-Order Masking. IACR Cryptol. ePrint Arch. Benjamin Grégoire, Kostas Papagiannopoulos, Peter Schwabe, Ko Stoffelen
2018	J	`jnl`	maskVerif: a formal tool for analyzing software and hardware masked implementations. IACR Cryptol. ePrint Arch. Gilles Barthe, Sonia Belaïd, Pierre-Alain Fouque, Benjamin Grégoire
2017	A*	`conf`	A Fast and Verified Software Stack for Secure Function Evaluation. CCS José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Vitor Pereira
2017	J	`jnl`	A Fast and Verified Software Stack for Secure Function Evaluation. IACR Cryptol. ePrint Arch. José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Vitor Pereira
2017	J	`jnl`	A Note on 'Further Improving Efficiency of Higher-Order Masking Scheme by Decreasing Randomness Complexity'. IACR Cryptol. ePrint Arch. Gilles Barthe, François Dupressoir, Benjamin Grégoire
2017	A*	`conf`	Coupling proofs are probabilistic product programs. POPL Gilles Barthe, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
2017	A*	`conf`	Jasmin: High-Assurance and High-Speed Cryptography. CCS José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Arthur Blot, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Hugo Pacheco, Benedikt Schmidt, Pierre-Yves Strub
2017	—	`conf`	Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model. EUROCRYPT (1) Gilles Barthe, François Dupressoir, Sebastian Faust, Benjamin Grégoire, François-Xavier Standaert, Pierre-Yves Strub
2017	J	`jnl`	Provably secure compilation of side-channel countermeasures. IACR Cryptol. ePrint Arch. Gilles Barthe, Benjamin Grégoire, Vincent Laporte
2017	J	`jnl`	Proving Expected Sensitivity of Probabilistic Programs. CoRR Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
2017	B	`conf`	Proving uniformity and independence by self-composition and coupling. LPAR Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
2017	J	`jnl`	Proving uniformity and independence by self-composition and coupling. CoRR Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
2016	A*	`conf`	A Program Logic for Union Bounds. ICALP Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
2016	J	`jnl`	A program logic for union bounds. CoRR Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
2016	A*	`conf`	Advanced Probabilistic Couplings for Differential Privacy. CCS Gilles Barthe, Noémie Fong, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
2016	J	`jnl`	Advanced Probabilistic Couplings for Differential Privacy. CoRR Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
2016	J	`jnl`	Coupling proofs are probabilistic product programs. CoRR Gilles Barthe, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
2016	J	`jnl`	Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model. IACR Cryptol. ePrint Arch. Gilles Barthe, François Dupressoir, Sebastian Faust, Benjamin Grégoire, François-Xavier Standaert, Pierre-Yves Strub
2016	A*	`conf`	Proving Differential Privacy via Probabilistic Couplings. LICS Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
2016	J	`jnl`	Proving Differential Privacy via Probabilistic Couplings. CoRR Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
2016	A*	`conf`	Strong Non-Interference and Type-Directed Higher-Order Masking. CCS Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Pierre-Yves Strub, Rébecca Zucchini
2015	A*	`conf`	Automated Proofs of Pairing-Based Cryptography. CCS Gilles Barthe, Benjamin Grégoire, Benedikt Schmidt
2015	J	`jnl`	Compositional Verification of Higher-Order Masking: Application to a Verifying Masking Compiler. IACR Cryptol. ePrint Arch. Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire
2015	B	`conf`	Relational Reasoning via Probabilistic Coupling. LPAR Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Léo Stefanesco, Pierre-Yves Strub
2015	J	`jnl`	Relational reasoning via probabilistic coupling. CoRR Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Léo Stefanesco, Pierre-Yves Strub
2015	—	`conf`	Verified Proofs of Higher-Order Masking. EUROCRYPT (1) Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Pierre-Yves Strub
2015	J	`jnl`	Verified Proofs of Higher-Order Masking. IACR Cryptol. ePrint Arch. Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Pierre-Yves Strub
2014	A	`conf`	Certified Synthesis of Efficient Batch Verifiers. CSF Joseph A. Akinyele, Gilles Barthe, Benjamin Grégoire, Benedikt Schmidt, Pierre-Yves Strub
2014	J	`jnl`	Making RSA-PSS Provably Secure Against Non-Random Faults. IACR Cryptol. ePrint Arch. Gilles Barthe, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Mehdi Tibouchi, Jean-Christophe Zapalowicz
2014	A	`conf`	Making RSA-PSS Provably Secure against Non-random Faults. CHES Gilles Barthe, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Mehdi Tibouchi, Jean-Christophe Zapalowicz
2014	A*	`conf`	Probabilistic relational verification for cryptographic implementations. POPL Gilles Barthe, Cédric Fournet, Benjamin Grégoire, Pierre-Yves Strub, Nikhil Swamy, Santiago Zanella-Béguelin
2014	A*	`conf`	Synthesis of Fault Attacks on Cryptographic Implementations. CCS Gilles Barthe, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Jean-Christophe Zapalowicz
2014	J	`jnl`	Synthesis of Fault Attacks on Cryptographic Implementations. IACR Cryptol. ePrint Arch. Gilles Barthe, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Jean-Christophe Zapalowicz
2014	J	`jnl`	Verified Implementations for Secure and Verifiable Computation. IACR Cryptol. ePrint Arch. José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Guillaume Davy, François Dupressoir, Benjamin Grégoire, Pierre-Yves Strub
2013	—	`conf`	EasyCrypt: A Tutorial. FOSAD Gilles Barthe, François Dupressoir, Benjamin Grégoire, César Kunz, Benedikt Schmidt, Pierre-Yves Strub
2013	A*	`conf`	Fully automated analysis of padding-based encryption in the computational model. CCS Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Yassine Lakhnech, Benedikt Schmidt, Santiago Zanella-Béguelin
2013	A	`conf`	Verified Computational Differential Privacy with Applications to Smart Metering. CSF Gilles Barthe, George Danezis, Benjamin Grégoire, César Kunz, Santiago Zanella-Béguelin
2013	J	`jnl`	Verified indifferentiable hashing into elliptic curves. J. Comput. Secur. Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Federico Olmedo, Santiago Zanella-Béguelin
2012	J	`jnl`	Automated Analysis and Synthesis of Padding-Based Encryption Schemes. IACR Cryptol. ePrint Arch. Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Yassine Lakhnech, Santiago Zanella-Béguelin
2012	B	`conf`	Automation in Computer-Aided Cryptography: Proofs, Attacks and Designs. CPP Gilles Barthe, Benjamin Grégoire, César Kunz, Yassine Lakhnech, Santiago Zanella-Béguelin
2012	B	`conf`	Computer-Aided Cryptographic Proofs. ITP Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Santiago Zanella-Béguelin
2012	B	`conf`	Computer-Aided Cryptographic Proofs. SAS Gilles Barthe, Benjamin Grégoire, Santiago Zanella-Béguelin
2012	B	`conf`	Probabilistic Relational Hoare Logics for Computer-Aided Security Proofs. MPC Gilles Barthe, Benjamin Grégoire, Santiago Zanella-Béguelin
2012	J	`jnl`	Recent Advances in the Formal Verification of Cryptographic Systems: Turing's Legacy ERCIM News Benjamin Grégoire
2012	—	`conf`	Verified Indifferentiable Hashing into Elliptic Curves. POST Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Federico Olmedo, Santiago Zanella-Béguelin
2012	A	`conf`	Verified Security of Merkle-Damgård. CSF Michael Backes, Gilles Barthe, Matthias Berg, Benjamin Grégoire, César Kunz, Malte Skoruppa, Santiago Zanella-Béguelin
2011	B	`conf`	A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses. CPP Michaël Armand, Germain Faure, Benjamin Grégoire, Chantal Keller, Laurent Théry, Benjamin Werner
2011	B	`conf`	Beyond Provable Security Verifiable IND-CCA Security of OAEP. CT-RSA Gilles Barthe, Benjamin Grégoire, Yassine Lakhnech, Santiago Zanella-Béguelin
2011	J	`jnl`	Certifying compilers using higher-order theorem provers as certificate checkers. Formal Methods Syst. Des. Jan Olaf Blech, Benjamin Grégoire
2011	A*	`conf`	Computer-Aided Security Proofs for the Working Cryptographer. CRYPTO Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Santiago Zanella-Béguelin
2011	B	`conf`	Full Reduction at Full Throttle. CPP Mathieu Boespflug, Maxime Dénès, Benjamin Grégoire
2010	A	`conf`	A Machine-Checked Formalization of Sigma-Protocols. CSF Gilles Barthe, Daniel Hedin, Santiago Zanella-Béguelin, Benjamin Grégoire, Sylvain Heraud
2010	B	`conf`	Extending Coq with Imperative Features and Its Application to SAT Verification. ITP Michaël Armand, Benjamin Grégoire, Arnaud Spiwack, Laurent Théry
2010	—	`conf`	On Strong Normalization of the Calculus of Constructions with Type-Based Termination. LPAR (Yogyakarta) Benjamin Grégoire, Jorge luis Sacchini
2010	B	`conf`	Programming Language Techniques for Cryptographic Proofs. ITP Gilles Barthe, Benjamin Grégoire, Santiago Zanella-Béguelin
2009	J	`jnl`	Certificate translation for optimizing compilers. ACM Trans. Program. Lang. Syst. Gilles Barthe, Benjamin Grégoire, César Kunz, Tamara Rezk
2009	A*	`conf`	Formal certification of code-based cryptographic proofs. POPL Gilles Barthe, Benjamin Grégoire, Santiago Zanella-Béguelin
2009	A*	`conf`	Formally Certifying the Security of Digital Signature Schemes. SP Santiago Zanella-Béguelin, Gilles Barthe, Benjamin Grégoire, Federico Olmedo
2009	C	`conf`	Implementing a Direct Method for Certificate Translation. ICFEM Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, César Kunz, Anne Pacalet
2008	—	`conf`	A New Elimination Rule for the Calculus of Inductive Constructions. TYPES Bruno Barras, Pierre Corbineau, Benjamin Grégoire, Hugo Herbelin, Jorge luis Sacchini
2008	—	`conf`	A Tutorial on Type-Based Termination. LerNet ALFA Summer School Gilles Barthe, Benjamin Grégoire, Colin Riba
2008	—	`conf`	Formal Certification of ElGamal Encryption. Formal Aspects in Security and Trust Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Santiago Zanella-Béguelin
2008	A	`conf`	Preservation of Proof Obligations from Java to the Java Virtual Machine. IJCAR Gilles Barthe, Benjamin Grégoire, Mariela Pavlova
2008	—	`conf`	Proof Certificates for Algebra and Their Application to Automatic Geometry Theorem Proving. Automated Deduction in Geometry Benjamin Grégoire, Loïc Pottier, Laurent Théry
2008	B	`conf`	Type-Based Termination with Sized Products. CSL Gilles Barthe, Benjamin Grégoire, Colin Riba
2007	—	`conf`	Combining a Verification Condition Generator for a Bytecode Language with Static Analyses. TGC Benjamin Grégoire, Jorge luis Sacchini
2007	—	`conf`	The MOBIUS Proof Carrying Code Infrastructure. FMCO Gilles Barthe, Pierre Crégut, Benjamin Grégoire, Thomas P. Jensen, David Pichardie
2006	Misc	`conf`	A Computational Approach to Pocklington Certificates in Type Theory. FLOPS Benjamin Grégoire, Laurent Théry, Benjamin Werner
2006	A	`conf`	A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers. IJCAR Benjamin Grégoire, Laurent Théry
2006	B	`conf`	CIC[^( )]: Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions. LPAR Gilles Barthe, Benjamin Grégoire, Fernando Pastawski
2006	B	`conf`	Certificate Translation for Optimizing Compilers. SAS Gilles Barthe, Benjamin Grégoire, César Kunz, Tamara Rezk
2006	—	`ed.`	Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, Second International Workshop, CASSIS 2005, Nice, France, March 8-11, 2005, Revised Selected Papers CASSIS Gilles Barthe, Benjamin Grégoire, Marieke Huisman, Jean-Louis Lanet
2006	—	`conf`	JACK - A Tool for Validation of Security and Behaviour of Java Applications. FMCO Gilles Barthe, Lilian Burdy, Julien Charles, Benjamin Grégoire, Marieke Huisman, Jean-Louis Lanet, Mariela Pavlova, Antoine Requet
2006	—	`conf`	MOBIUS: Mobility, Ubiquity, Security. TGC Gilles Barthe, Lennart Beringer, Pierre Crégut, Benjamin Grégoire, Martin Hofmann, Peter Müller, Erik Poll, Germán Puebla, Ian Stark, Eric Vétillard
2005	B	`conf`	On the Role of Type Decorations in the Calculus of Inductive Constructions. CSL Bruno Barras, Benjamin Grégoire
2005	—	`conf`	Practical Inference for Type-Based Termination in a Polymorphic Setting. TLCA Gilles Barthe, Benjamin Grégoire, Fernando Pastawski
2005	—	`conf`	Proving Equalities in a Commutative Ring Done Right in Coq. TPHOLs Benjamin Grégoire, Assia Mahboubi
2004	—	`conf`	A Structured Approach to Proving Compiler Optimizations Based on Dataflow Analysis. TYPES Yves Bertot, Benjamin Grégoire, Xavier Leroy
2002	A	`conf`	A compiled implementation of strong reduction. ICFP Benjamin Grégoire, Xavier Leroy