Benjamin Grégoire

ORCID

Publication Activity (10 Years)

Years Active: 2002-2024
Publications (10 Years): 78

Top Venues

IACR Cryptol. ePrint Arch.

CCS

CoRR

CSF

Publications

Santiago Arranz Olmos, Gilles Barthe, Lionel Blatter, Benjamin Grégoire, Vincent Laporte
Preservation of Speculative Constant-time by Compilation. IACR Cryptol. ePrint Arch. 2024 (2024)
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
Formally verifying Kyber Episode V: Machine-checked IND-CCA security and correctness of ML-KEM in EasyCrypt. IACR Cryptol. ePrint Arch. 2024 (2024)
Martin Avanzini, Gilles Barthe, Davide Davoli, Benjamin Grégoire
A quantitative probabilistic relational Hoare logic. CoRR (2024)
Santiago Arranz Olmos, Gilles Barthe, Ruben Gonzalez, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Tiago Oliveira, Peter Schwabe
High-assurance zeroization. IACR Trans. Cryptogr. Hardw. Embed. Syst. 2024 (1) (2024)
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
Formally Verifying Kyber - Episode V: Machine-Checked IND-CCA Security and Correctness of ML-KEM in EasyCrypt. CRYPTO (2) (2024)
Gilles Barthe, Sonia Belaïd, Thomas Espitau, Pierre-Alain Fouque, Benjamin Grégoire, Mélissa Rossi, Mehdi Tibouchi
Masking the GLP Lattice-Based Signature Scheme at Any Order. J. Cryptol. 37 (1) (2024)
Santiago Arranz Olmos, Gilles Barthe, Chitchanok Chuengsatiansup, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Peter Schwabe, Yuval Yarom, Zhiyuan Zhang
Protecting cryptographic code against Spectre-RSB. IACR Cryptol. ePrint Arch. 2024 (2024)
Martin Avanzini, Gilles Barthe, Benjamin Grégoire, Georg Moser, Gabriele Vanoni
Hopping Proofs of Expectation-Based Properties: Applications to Skiplists and Security Proofs. Proc. ACM Program. Lang. 8 (OOPSLA1) (2024)
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
Formally verifying Kyber Part I: Implementation Correctness. IACR Cryptol. ePrint Arch. 2023 (2023)
Benjamin Grégoire, Jean-Christophe Léchenet, Enrico Tassi
Practical and Sound Equality Tests, Automatically: Deriving eqType Instances for Jasmin's Data Types with Coq-Elpi. CPP (2023)
Santiago Arranz Olmos, Gilles Barthe, Ruben Gonzalez, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Tiago Oliveira, Peter Schwabe
High-assurance zeroization. IACR Cryptol. ePrint Arch. 2023 (2023)
Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Pierre-Yves Strub
Mechanized Proofs of Adversarial Complexity and Application to Universal Composability. ACM Trans. Priv. Secur. 26 (3) (2023)
Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Swarn Priya, Peter Schwabe, Lucas Tabary-Maujean
Typing High-Speed Cryptography against Spectre v1. SP (2023)
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
Formally verifying Kyber Episode IV: Implementation correctness. IACR Trans. Cryptogr. Hardw. Embed. Syst. 2023 (3) (2023)
Manuel Barbosa, Gilles Barthe, Christian Doczkal, Jelle Don, Serge Fehr, Benjamin Grégoire, Yu-Hsuan Huang, Andreas Hülsing, Yi Lee, Xiaodi Wu
Fixing and Mechanizing the Security Proof of Fiat-Shamir with Aborts and Dilithium. IACR Cryptol. ePrint Arch. 2023 (2023)
Manuel Barbosa, François Dupressoir, Benjamin Grégoire, Andreas Hülsing, Matthias Meijers, Pierre-Yves Strub
Machine-Checked Security for $\mathrm{XMSS}$ as in RFC 8391 and $\mathrm{SPHINCS}^{+}$. IACR Cryptol. ePrint Arch. 2023 (2023)
Manuel Barbosa, Gilles Barthe, Christian Doczkal, Jelle Don, Serge Fehr, Benjamin Grégoire, Yu-Hsuan Huang, Andreas Hülsing, Yi Lee, Xiaodi Wu
Fixing and Mechanizing the Security Proof of Fiat-Shamir with Aborts and Dilithium. CRYPTO (5) (2022)
Manuel Barbosa, François Dupressoir, Benjamin Grégoire, Andreas Hülsing, Matthias Meijers, Pierre-Yves Strub
Machine-Checked Security for rmXMSS as in RFC 8391 and $\mathrm {SPHINCS^{+}} $. CRYPTO (5) (2022)
Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Swarn Priya
Enforcing fine-grained constant-time policies. IACR Cryptol. ePrint Arch. 2022 (2022)
Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Swarn Priya
Enforcing Fine-grained Constant-time Policies. CCS (2022)
Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Swarn Priya, Peter Schwabe, Lucas Tabary-Maujean
Typing High-Speed Cryptography against Spectre v1. IACR Cryptol. ePrint Arch. 2022 (2022)
Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Swarn Priya
Structured Leakage and Applications to Cryptographic Constant-Time and Cost. IACR Cryptol. ePrint Arch. 2021 (2021)
Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Swarn Priya
Structured Leakage and Applications to Cryptographic Constant-Time and Cost. CCS (2021)
Gaëtan Cassiers, Benjamin Grégoire, Itamar Levi, François-Xavier Standaert
Hardware Private Circuits: From Trivial Composition to Full Verification. IEEE Trans. Computers 70 (10) (2021)
Manuel Barbosa, Gilles Barthe, Xiong Fan, Benjamin Grégoire, Shih-Han Hung, Jonathan Katz, Pierre-Yves Strub, Xiaodi Wu, Li Zhou
EasyPQC: Verifying Post-Quantum Cryptography. IACR Cryptol. ePrint Arch. 2021 (2021)
Gilles Barthe, Sunjay Cauligi, Benjamin Grégoire, Adrien Koutsos, Kevin Liao, Tiago Oliveira, Swarn Priya, Tamara Rezk, Peter Schwabe
High-Assurance Cryptography in the Spectre Era. IEEE Symposium on Security and Privacy (2021)
Manuel Barbosa, Gilles Barthe, Xiong Fan, Benjamin Grégoire, Shih-Han Hung, Jonathan Katz, Pierre-Yves Strub, Xiaodi Wu, Li Zhou
EasyPQC: Verifying Post-Quantum Cryptography. CCS (2021)
Gilles Barthe, Marc Gourjon, Benjamin Grégoire, Maximilian Orlt, Clara Paglialonga, Lars Porth
Masking in Fine-Grained Leakage Models: Construction, Implementation and Verification. IACR Trans. Cryptogr. Hardw. Embed. Syst. 2021 (2) (2021)
Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Pierre-Yves Strub
Mechanized Proofs of Adversarial Complexity and Application to Universal Composability. CCS (2021)
Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Pierre-Yves Strub
Mechanized Proofs of Adversarial Complexity and Application to Universal Composability. IACR Cryptol. ePrint Arch. 2021 (2021)
Gaëtan Cassiers, Benjamin Grégoire, Itamar Levi, François-Xavier Standaert
Hardware Private Circuits: From Trivial Composition to Full Verification. IACR Cryptol. ePrint Arch. 2020 (2020)
Gilles Barthe, Sunjay Cauligi, Benjamin Grégoire, Adrien Koutsos, Kevin Liao, Tiago Oliveira, Swarn Priya, Tamara Rezk, Peter Schwabe
High-Assurance Cryptography Software in the Spectre Era. IACR Cryptol. ePrint Arch. 2020 (2020)
Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, Alix Trieu
Formal verification of a constant-time preserving C compiler. Proc. ACM Program. Lang. 4 (POPL) (2020)
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Vincent Laporte, Tiago Oliveira, Pierre-Yves Strub
The Last Mile: High-Assurance and High-Speed Cryptographic Implementations. IEEE Symposium on Security and Privacy (2020)
Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, François-Xavier Standaert, Pierre-Yves Strub
Improved parallel mask refreshing algorithms: generic solutions with parametrized non-interference and automated optimizations. J. Cryptogr. Eng. 10 (1) (2020)
Mohamad El Laz, Benjamin Grégoire, Tamara Rezk
Security Analysis of ElGamal Implementations. ICETE (2) (2020)
Gilles Barthe, Marc Gourjon, Benjamin Grégoire, Maximilian Orlt, Clara Paglialonga, Lars Porth
Masking in Fine-Grained Leakage Models: Construction, Implementation and Verification. IACR Cryptol. ePrint Arch. 2020 (2020)
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
Machine-Checked Proofs for Cryptographic Standards. IACR Cryptol. ePrint Arch. 2019 (2019)
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
Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3. CCS (2019)
Sunjay Cauligi, Gary Soeller, Brian Johannesmeyer, Fraser Brown, Riad S. Wahby, John Renner, Benjamin Grégoire, Gilles Barthe, Ranjit Jhala, Deian Stefan
FaCT: a DSL for timing-sensitive computation. PLDI (2019)
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Matthew Campagna, Ernie Cohen, Benjamin Grégoire, Vitor Pereira, Bernardo Portela, Pierre-Yves Strub, Serdar Tasiran
A Machine-Checked Proof of Security for AWS Key Management Service. IACR Cryptol. ePrint Arch. 2019 (2019)
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Matthew Campagna, Ernie Cohen, Benjamin Grégoire, Vitor Pereira, Bernardo Portela, Pierre-Yves Strub, Serdar Tasiran
A Machine-Checked Proof of Security for AWS Key Management Service. CCS (2019)
Gilles Barthe, Benjamin Grégoire, Charlie Jacomme, Steve Kremer, Pierre-Yves Strub
Symbolic Methods in Computational Cryptography Proofs. CSF (2019)
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Vincent Laporte, Tiago Oliveira, Pierre-Yves Strub
The Last Mile: High-Assurance and High-Speed Cryptographic Implementations. CoRR (2019)
Gilles Barthe, Sandrine Blazy, Benjamin Grégoire, Rémi Hutin, Vincent Laporte, David Pichardie, Alix Trieu
Formal Verification of a Constant-Time Preserving C Compiler. IACR Cryptol. ePrint Arch. 2019 (2019)
Gilles Barthe, Sonia Belaïd, Gaëtan Cassiers, Pierre-Alain Fouque, Benjamin Grégoire, François-Xavier Standaert
maskVerif: Automated Verification of Higher-Order Masking in Presence of Physical Defaults. ESORICS (1) (2019)
Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, François-Xavier Standaert, Pierre-Yves Strub
Improved Parallel Mask Refreshing Algorithms: Generic Solutions with Parametrized Non-Interference & Automated Optimizations. IACR Cryptol. ePrint Arch. 2018 (2018)
Gilles Barthe, Xiong Fan, Joshua Gancher, Benjamin Grégoire, Charlie Jacomme, Elaine Shi
Symbolic Proofs for Lattice-Based Cryptography. IACR Cryptol. ePrint Arch. 2018 (2018)
Gilles Barthe, Sonia Belaïd, Thomas Espitau, Pierre-Alain Fouque, Benjamin Grégoire, Mélissa Rossi, Mehdi Tibouchi
Masking the GLP Lattice-Based Signature Scheme at Any Order. IACR Cryptol. ePrint Arch. 2018 (2018)
Gilles Barthe, Benjamin Grégoire, Vincent Laporte
Secure Compilation of Side-Channel Countermeasures: The Case of Cryptographic "Constant-Time". CSF (2018)
Gilles Barthe, Sonia Belaïd, Pierre-Alain Fouque, Benjamin Grégoire
maskVerif: a formal tool for analyzing software and hardware masked implementations. IACR Cryptol. ePrint Arch. 2018 (2018)
Benjamin Grégoire, Kostas Papagiannopoulos, Peter Schwabe, Ko Stoffelen
Vectorizing Higher-Order Masking. IACR Cryptol. ePrint Arch. 2018 (2018)
Cécile Baritel-Ruet, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire
Formal Security Proof of CMAC and Its Variants. CSF (2018)
Gilles Barthe, Thomas Espitau, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
An Assertion-Based Program Logic for Probabilistic Programs. ESOP (2018)
Gilles Barthe, Xiong Fan, Joshua Gancher, Benjamin Grégoire, Charlie Jacomme, Elaine Shi
Symbolic Proofs for Lattice-Based Cryptography. CCS (2018)
Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
Proving expected sensitivity of probabilistic programs. Proc. ACM Program. Lang. 2 (POPL) (2018)
Benjamin Grégoire, Kostas Papagiannopoulos, Peter Schwabe, Ko Stoffelen
Vectorizing Higher-Order Masking. COSADE (2018)
Gilles Barthe, Sonia Belaïd, Thomas Espitau, Pierre-Alain Fouque, Benjamin Grégoire, Mélissa Rossi, Mehdi Tibouchi
Masking the GLP Lattice-Based Signature Scheme at Any Order. EUROCRYPT (2) (2018)
Gilles Barthe, Thomas Espitau, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
An Assertion-Based Program Logic for Probabilistic Programs. CoRR (2018)
Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
Proving Expected Sensitivity of Probabilistic Programs. CoRR (2017)
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Arthur Blot, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Hugo Pacheco, Benedikt Schmidt, Pierre-Yves Strub
Jasmin: High-Assurance and High-Speed Cryptography. CCS (2017)
Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
Proving uniformity and independence by self-composition and coupling. LPAR (2017)
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Vitor Pereira
A Fast and Verified Software Stack for Secure Function Evaluation. IACR Cryptol. ePrint Arch. 2017 (2017)
Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
Proving uniformity and independence by self-composition and coupling. CoRR (2017)
Gilles Barthe, François Dupressoir, Benjamin Grégoire
A Note on 'Further Improving Efficiency of Higher-Order Masking Scheme by Decreasing Randomness Complexity'. IACR Cryptol. ePrint Arch. 2017 (2017)
Gilles Barthe, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
Coupling proofs are probabilistic product programs. POPL (2017)
Gilles Barthe, François Dupressoir, Sebastian Faust, Benjamin Grégoire, François-Xavier Standaert, Pierre-Yves Strub
Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model. EUROCRYPT (1) (2017)
Gilles Barthe, Benjamin Grégoire, Vincent Laporte
Provably secure compilation of side-channel countermeasures. IACR Cryptol. ePrint Arch. 2017 (2017)
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Vitor Pereira
A Fast and Verified Software Stack for Secure Function Evaluation. CCS (2017)
Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
Proving Differential Privacy via Probabilistic Couplings. LICS (2016)
Gilles Barthe, François Dupressoir, Sebastian Faust, Benjamin Grégoire, François-Xavier Standaert, Pierre-Yves Strub
Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model. IACR Cryptol. ePrint Arch. 2016 (2016)
Gilles Barthe, Noémie Fong, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
Advanced Probabilistic Couplings for Differential Privacy. CCS (2016)
Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
A program logic for union bounds. CoRR (2016)
Gilles Barthe, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
Coupling proofs are probabilistic product programs. CoRR (2016)
Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
Proving Differential Privacy via Probabilistic Couplings. CoRR (2016)
Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Pierre-Yves Strub, Rébecca Zucchini
Strong Non-Interference and Type-Directed Higher-Order Masking. CCS (2016)
Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
Advanced Probabilistic Couplings for Differential Privacy. CoRR (2016)
Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
A Program Logic for Union Bounds. ICALP (2016)
Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Léo Stefanesco, Pierre-Yves Strub
Relational Reasoning via Probabilistic Coupling. LPAR (2015)
Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Léo Stefanesco, Pierre-Yves Strub
Relational reasoning via probabilistic coupling. CoRR (2015)
Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire
Compositional Verification of Higher-Order Masking: Application to a Verifying Masking Compiler. IACR Cryptol. ePrint Arch. 2015 (2015)
Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Pierre-Yves Strub
Verified Proofs of Higher-Order Masking. IACR Cryptol. ePrint Arch. 2015 (2015)
Gilles Barthe, Benjamin Grégoire, Benedikt Schmidt
Automated Proofs of Pairing-Based Cryptography. CCS (2015)
Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Pierre-Yves Strub
Verified Proofs of Higher-Order Masking. EUROCRYPT (1) (2015)
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Guillaume Davy, François Dupressoir, Benjamin Grégoire, Pierre-Yves Strub
Verified Implementations for Secure and Verifiable Computation. IACR Cryptol. ePrint Arch. 2014 (2014)
Gilles Barthe, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Mehdi Tibouchi, Jean-Christophe Zapalowicz
Making RSA-PSS Provably Secure against Non-random Faults. CHES (2014)
Joseph A. Akinyele, Gilles Barthe, Benjamin Grégoire, Benedikt Schmidt, Pierre-Yves Strub
Certified Synthesis of Efficient Batch Verifiers. CSF (2014)
Gilles Barthe, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Mehdi Tibouchi, Jean-Christophe Zapalowicz
Making RSA-PSS Provably Secure Against Non-Random Faults. IACR Cryptol. ePrint Arch. 2014 (2014)
Gilles Barthe, Cédric Fournet, Benjamin Grégoire, Pierre-Yves Strub, Nikhil Swamy, Santiago Zanella Béguelin
Probabilistic relational verification for cryptographic implementations. POPL (2014)
Gilles Barthe, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Jean-Christophe Zapalowicz
Synthesis of Fault Attacks on Cryptographic Implementations. IACR Cryptol. ePrint Arch. 2014 (2014)
Gilles Barthe, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Jean-Christophe Zapalowicz
Synthesis of Fault Attacks on Cryptographic Implementations. CCS (2014)
Gilles Barthe, George Danezis, Benjamin Grégoire, César Kunz, Santiago Zanella Béguelin
Verified Computational Differential Privacy with Applications to Smart Metering. CSF (2013)
Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Federico Olmedo, Santiago Zanella Béguelin
Verified indifferentiable hashing into elliptic curves. J. Comput. Secur. 21 (6) (2013)
Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Yassine Lakhnech, Benedikt Schmidt, Santiago Zanella Béguelin
Fully automated analysis of padding-based encryption in the computational model. CCS (2013)
Gilles Barthe, François Dupressoir, Benjamin Grégoire, César Kunz, Benedikt Schmidt, Pierre-Yves Strub
EasyCrypt: A Tutorial. FOSAD (2013)
Gilles Barthe, Benjamin Grégoire, César Kunz, Yassine Lakhnech, Santiago Zanella Béguelin
Automation in Computer-Aided Cryptography: Proofs, Attacks and Designs. CPP (2012)
Michael Backes, Gilles Barthe, Matthias Berg, Benjamin Grégoire, César Kunz, Malte Skoruppa, Santiago Zanella Béguelin
Verified Security of Merkle-Damgård. CSF (2012)
Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Yassine Lakhnech, Santiago Zanella Béguelin
Automated Analysis and Synthesis of Padding-Based Encryption Schemes. IACR Cryptol. ePrint Arch. 2012 (2012)
Gilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin
Probabilistic Relational Hoare Logics for Computer-Aided Security Proofs. MPC (2012)
Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Federico Olmedo, Santiago Zanella Béguelin
Verified Indifferentiable Hashing into Elliptic Curves. POST (2012)

Benjamin Grégoire.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Benjamin Grégoire