default search action
Benjamin Grégoire
Person information
- affiliation: Research Centre Inria Sophia Antipolis - Méditerranée: Valbonne, France
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
- [j13]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): 5 (2024) - [j12]Martin Avanzini, Gilles Barthe
, Benjamin Grégoire
Hopping Proofs of Expectation-Based Properties: Applications to Skiplists and Security Proofs. Proc. ACM Program. Lang. 8(OOPSLA1): 784-809 (2024) - [j11]Santiago Arranz Olmos, Gilles Barthe, Ruben Gonzalez, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet
High-assurance zeroization. IACR Trans. Cryptogr. Hardw. Embed. Syst. 2024(1): 375-397 (2024) - [c79]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: 384-421 - [c78]Bruno Blanchet, Pierre Boutry, Christian Doczkal, Benjamin Grégoire, Pierre-Yves Strub:
CV2EC: Getting the Best of Both Worlds. CSF 2024: 279-294 - [i44]Martin Avanzini, Gilles Barthe, Davide Davoli, Benjamin Grégoire:
A quantitative probabilistic relational Hoare logic. CoRR abs/2407.17127 (2024) - [i43]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: 843 (2024) - [i42]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: 1070 (2024) - [i41]Santiago Arranz Olmos, Gilles Barthe, Lionel Blatter, Benjamin Grégoire, Vincent Laporte:
Preservation of Speculative Constant-time by Compilation. IACR Cryptol. ePrint Arch. 2024: 1203 (2024) - 2023
- [j10]José Bacelar Almeida
Formally verifying Kyber Episode IV: Implementation correctness. IACR Trans. Cryptogr. Hardw. Embed. Syst. 2023(3): 164-193 (2023) - [j9]Manuel Barbosa
Mechanized Proofs of Adversarial Complexity and Application to Universal Composability. ACM Trans. Priv. Secur. 26(3): 41:1-41:34 (2023) - [c77]Benjamin Grégoire, Jean-Christophe Léchenet
Practical and Sound Equality Tests, Automatically: Deriving eqType Instances for Jasmin's Data Types with Coq-Elpi. CPP 2023: 167-181 - [c76]Manuel Barbosa
Fixing and Mechanizing the Security Proof of Fiat-Shamir with Aborts and Dilithium. CRYPTO (5) 2023: 358-389 - [c75]Manuel Barbosa
Machine-Checked Security for rmXMSS as in RFC 8391 and $\mathrm {SPHINCS^{+}} $. CRYPTO (5) 2023: 421-454 - [c74]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: 1094-1111 - [i40]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: 215 (2023) - [i39]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: 246 (2023) - [i38]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: 408 (2023) - [i37]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: 1713 (2023) - 2022
- [c73]Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Swarn Priya:
Enforcing Fine-grained Constant-time Policies. CCS 2022: 83-96 - [i36]Basavesh Ammanaghatta Shivakumar, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Swarn Priya:
Enforcing fine-grained constant-time policies. IACR Cryptol. ePrint Arch. 2022: 630 (2022) - [i35]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: 1270 (2022) - 2021
- [j8]Gaëtan Cassiers
Hardware Private Circuits: From Trivial Composition to Full Verification. IEEE Trans. Computers 70(10): 1677-1690 (2021) - [j7]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): 189-228 (2021) - [c72]Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Swarn Priya:
Structured Leakage and Applications to Cryptographic Constant-Time and Cost. CCS 2021: 462-476 - [c71]Manuel Barbosa
Mechanized Proofs of Adversarial Complexity and Application to Universal Composability. CCS 2021: 2541-2563 - [c70]Manuel Barbosa
EasyPQC: Verifying Post-Quantum Cryptography. CCS 2021: 2564-2586 - [c69]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. SP 2021: 1884-1901 - [i34]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: 156 (2021) - [i33]Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Swarn Priya:
Structured Leakage and Applications to Cryptographic Constant-Time and Cost. IACR Cryptol. ePrint Arch. 2021: 650 (2021) - [i32]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: 1253 (2021) - 2020
- [j6]Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque
Improved parallel mask refreshing algorithms: generic solutions with parametrized non-interference and automated optimizations. J. Cryptogr. Eng. 10(1): 17-26 (2020) - [j5]Gilles Barthe, Sandrine Blazy
Formal verification of a constant-time preserving C compiler. Proc. ACM Program. Lang. 4(POPL): 7:1-7:30 (2020) - [c68]Mohamad El Laz, Benjamin Grégoire, Tamara Rezk:
Security Analysis of ElGamal Implementations. ICETE (2) 2020: 310-321 - [c67]José Bacelar Almeida
The Last Mile: High-Assurance and High-Speed Cryptographic Implementations. SP 2020: 965-982 - [i31]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: 185 (2020) - [i30]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: 603 (2020) - [i29]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: 1104 (2020)
2010 – 2019
- 2019
- [c66]José Bacelar Almeida
A Machine-Checked Proof of Security for AWS Key Management Service. CCS 2019: 63-78 - [c65]José Bacelar Almeida
Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3. CCS 2019: 1607-1622 - [c64]Gilles Barthe, Benjamin Grégoire, Charlie Jacomme, Steve Kremer
Symbolic Methods in Computational Cryptography Proofs. CSF 2019: 136-151 - [c63]Gilles Barthe, Sonia Belaïd, Gaëtan Cassiers
maskVerif: Automated Verification of Higher-Order Masking in Presence of Physical Defaults. ESORICS (1) 2019: 300-318 - [c62]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: 174-189 - [i28]José Bacelar Almeida
The Last Mile: High-Assurance and High-Speed Cryptographic Implementations. CoRR abs/1904.04606 (2019) - [i27]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: 926 (2019) - [i26]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: 1042 (2019) - [i25]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: 1155 (2019) - 2018
- [j4]Gilles Barthe
Proving expected sensitivity of probabilistic programs. Proc. ACM Program. Lang. 2(POPL): 57:1-57:29 (2018) - [c61]Gilles Barthe
Symbolic Proofs for Lattice-Based Cryptography. CCS 2018: 538-555 - [c60]Benjamin Grégoire, Kostas Papagiannopoulos
Vectorizing Higher-Order Masking. COSADE 2018: 23-43 - [c59]Cécile Baritel-Ruet, François Dupressoir
Formal Security Proof of CMAC and Its Variants. CSF 2018: 91-104 - [c58]Gilles Barthe
Secure Compilation of Side-Channel Countermeasures: The Case of Cryptographic "Constant-Time". CSF 2018: 328-343 - [c57]Gilles Barthe, Thomas Espitau, Marco Gaboardi, Benjamin Grégoire, Justin Hsu
An Assertion-Based Program Logic for Probabilistic Programs. ESOP 2018: 117-144 - [c56]Gilles Barthe, Sonia Belaïd, Thomas Espitau, Pierre-Alain Fouque
Masking the GLP Lattice-Based Signature Scheme at Any Order. EUROCRYPT (2) 2018: 354-384 - [i24]Gilles Barthe, Thomas Espitau, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
An Assertion-Based Program Logic for Probabilistic Programs. CoRR abs/1803.05535 (2018) - [i23]Benjamin Grégoire, Kostas Papagiannopoulos, Peter Schwabe, Ko Stoffelen:
Vectorizing Higher-Order Masking. IACR Cryptol. ePrint Arch. 2018: 173 (2018) - [i22]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: 381 (2018) - [i21]Gilles Barthe, Sonia Belaïd, François Dupressoir
Improved Parallel Mask Refreshing Algorithms: Generic Solutions with Parametrized Non-Interference & Automated Optimizations. IACR Cryptol. ePrint Arch. 2018: 505 (2018) - [i20]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: 562 (2018) - [i19]Gilles Barthe, Xiong Fan, Joshua Gancher, Benjamin Grégoire, Charlie Jacomme, Elaine Shi:
Symbolic Proofs for Lattice-Based Cryptography. IACR Cryptol. ePrint Arch. 2018: 765 (2018) - 2017
- [c55]José Bacelar Almeida
Jasmin: High-Assurance and High-Speed Cryptography. CCS 2017: 1807-1823 - [c54]José Bacelar Almeida
A Fast and Verified Software Stack for Secure Function Evaluation. CCS 2017: 1989-2006 - [c53]Gilles Barthe, François Dupressoir, Sebastian Faust, Benjamin Grégoire, François-Xavier Standaert
Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model. EUROCRYPT (1) 2017: 535-566 - [c52]Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu
Proving uniformity and independence by self-composition and coupling. LPAR 2017: 385-403 - [c51]Gilles Barthe, Benjamin Grégoire, Justin Hsu
Coupling proofs are probabilistic product programs. POPL 2017: 161-174 - [i18]Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
Proving uniformity and independence by self-composition and coupling. CoRR abs/1701.06477 (2017) - [i17]Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
Proving Expected Sensitivity of Probabilistic Programs. CoRR abs/1708.02537 (2017) - [i16]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: 821 (2017) - [i15]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: 1053 (2017) - [i14]Gilles Barthe, Benjamin Grégoire, Vincent Laporte:
Provably secure compilation of side-channel countermeasures. IACR Cryptol. ePrint Arch. 2017: 1233 (2017) - 2016
- [c50]Gilles Barthe
Advanced Probabilistic Couplings for Differential Privacy. CCS 2016: 55-67 - [c49]Gilles Barthe
Strong Non-Interference and Type-Directed Higher-Order Masking. CCS 2016: 116-129 - [c48]Gilles Barthe
A Program Logic for Union Bounds. ICALP 2016: 107:1-107:15 - [c47]Gilles Barthe
Proving Differential Privacy via Probabilistic Couplings. LICS 2016: 749-758 - [i13]Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
Proving Differential Privacy via Probabilistic Couplings. CoRR abs/1601.05047 (2016) - [i12]Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
A program logic for union bounds. CoRR abs/1602.05681 (2016) - [i11]Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
Advanced Probabilistic Couplings for Differential Privacy. CoRR abs/1606.07143 (2016) - [i10]Gilles Barthe, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
Coupling proofs are probabilistic product programs. CoRR abs/1607.03455 (2016) - [i9]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: 912 (2016) - 2015
- [c46]Gilles Barthe
Automated Proofs of Pairing-Based Cryptography. CCS 2015: 1156-1168 - [c45]Gilles Barthe, Sonia Belaïd, François Dupressoir
Verified Proofs of Higher-Order Masking. EUROCRYPT (1) 2015: 457-485 - [c44]Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu
Relational Reasoning via Probabilistic Coupling. LPAR 2015: 387-401 - [i8]Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Léo Stefanesco, Pierre-Yves Strub:
Relational reasoning via probabilistic coupling. CoRR abs/1509.03476 (2015) - [i7]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: 60 (2015) - [i6]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: 506 (2015) - 2014
- [c43]Gilles Barthe
Synthesis of Fault Attacks on Cryptographic Implementations. CCS 2014: 1016-1027 - [c42]Gilles Barthe, François Dupressoir
Making RSA-PSS Provably Secure against Non-random Faults. CHES 2014: 206-222 - [c41]Joseph A. Akinyele, Gilles Barthe
Certified Synthesis of Efficient Batch Verifiers. CSF 2014: 153-165 - [c40]Gilles Barthe
Probabilistic relational verification for cryptographic implementations. POPL 2014: 193-206 - [i5]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: 252 (2014) - [i4]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: 436 (2014) - [i3]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: 456 (2014) - 2013
- [j3]Gilles Barthe
Verified indifferentiable hashing into elliptic curves. J. Comput. Secur. 21(6): 881-917 (2013) - [c39]Gilles Barthe
Fully automated analysis of padding-based encryption in the computational model. CCS 2013: 1247-1260 - [c38]Gilles Barthe
Verified Computational Differential Privacy with Applications to Smart Metering. CSF 2013: 287-301 - [c37]Gilles Barthe, François Dupressoir
EasyCrypt: A Tutorial. FOSAD 2013: 146-166 - 2012
- [c36]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: 7-8 - [c35]Michael Backes, Gilles Barthe
Verified Security of Merkle-Damgård. CSF 2012: 354-368 - [c34]Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Santiago Zanella Béguelin
Computer-Aided Cryptographic Proofs. ITP 2012: 11-27 - [c33]Gilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin
Probabilistic Relational Hoare Logics for Computer-Aided Security Proofs. MPC 2012: 1-6 - [c32]Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Federico Olmedo
Verified Indifferentiable Hashing into Elliptic Curves. POST 2012: 209-228 - [c31]Gilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin
Computer-Aided Cryptographic Proofs. SAS 2012: 1-2 - [i2]Benjamin Grégoire:
Recent Advances in the Formal Verification of Cryptographic Systems: Turing's Legacy. ERCIM News 2012(91) (2012) - [i1]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: 695 (2012) - 2011
- [j2]Jan Olaf Blech
Certifying compilers using higher-order theorem provers as certificate checkers. Formal Methods Syst. Des. 38(1): 33-61 (2011) - [c30]Michaël Armand, Germain Faure, Benjamin Grégoire, Chantal Keller, Laurent Théry, Benjamin Werner:
A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses. CPP 2011: 135-150 - [c29]Mathieu Boespflug, Maxime Dénès, Benjamin Grégoire:
Full Reduction at Full Throttle. CPP 2011: 362-377 - [c28]Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Santiago Zanella Béguelin:
Computer-Aided Security Proofs for the Working Cryptographer. CRYPTO 2011: 71-90 - [c27]Gilles Barthe, Benjamin Grégoire, Yassine Lakhnech, Santiago Zanella Béguelin
Beyond Provable Security Verifiable IND-CCA Security of OAEP. CT-RSA 2011: 180-196 - 2010
- [c26]Gilles Barthe
A Machine-Checked Formalization of Sigma-Protocols. CSF 2010: 246-260 - [c25]Michaël Armand, Benjamin Grégoire, Arnaud Spiwack, Laurent Théry:
Extending Coq with Imperative Features and Its Application to SAT Verification. ITP 2010: 83-98 - [c24]Gilles Barthe, Benjamin Grégoire, Santiago Zanella Béguelin
Programming Language Techniques for Cryptographic Proofs. ITP 2010: 115-130 - [c23]Benjamin Grégoire, Jorge Luis Sacchini:
On Strong Normalization of the Calculus of Constructions with Type-Based Termination. LPAR (Yogyakarta) 2010: 333-347
2000 – 2009
- 2009
- [j1]Gilles Barthe
Certificate translation for optimizing compilers. ACM Trans. Program. Lang. Syst. 31(5): 18:1-18:45 (2009) - [c22]Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, César Kunz, Anne Pacalet:
Implementing a Direct Method for Certificate Translation. ICFEM 2009: 541-560 - [c21]Gilles Barthe
Formal certification of code-based cryptographic proofs. POPL 2009: 90-101 - [c20]Santiago Zanella Béguelin
Formally Certifying the Security of Digital Signature Schemes. SP 2009: 237-250 - 2008
- [c19]Benjamin Grégoire, Loïc Pottier, Laurent Théry:
Proof Certificates for Algebra and Their Application to Automatic Geometry Theorem Proving. Automated Deduction in Geometry 2008: 42-59 - [c18]Gilles Barthe, Benjamin Grégoire, Mariela Pavlova:
Preservation of Proof Obligations from Java to the Java Virtual Machine. IJCAR 2008: 83-99 - [c17]Gilles Barthe, Benjamin Grégoire, Colin Riba:
Type-Based Termination with Sized Products. CSL 2008: 493-507 - [c16]Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Santiago Zanella Béguelin
Formal Certification of ElGamal Encryption. Formal Aspects in Security and Trust 2008: 1-19 - [c15]Gilles Barthe, Benjamin Grégoire, Colin Riba:
A Tutorial on Type-Based Termination. LerNet ALFA Summer School 2008: 100-152 - [c14]Bruno Barras, Pierre Corbineau, Benjamin Grégoire, Hugo Herbelin, Jorge Luis Sacchini:
A New Elimination Rule for the Calculus of Inductive Constructions. TYPES 2008: 32-48 - 2007
- [c13]Gilles Barthe, Pierre Crégut, Benjamin Grégoire, Thomas P. Jensen, David Pichardie:
The MOBIUS Proof Carrying Code Infrastructure. FMCO 2007: 1-24 - [c12]Benjamin Grégoire, Jorge Luis Sacchini:
Combining a Verification Condition Generator for a Bytecode Language with Static Analyses. TGC 2007: 23-40 - 2006
- [c11]Benjamin Grégoire, Laurent Théry:
A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers. IJCAR 2006: 423-437 - [c10]Benjamin Grégoire, Laurent Théry, Benjamin Werner:
A Computational Approach to Pocklington Certificates in Type Theory. FLOPS 2006: 97-113 - [c9]Gilles Barthe, Lilian Burdy, Julien Charles, Benjamin Grégoire, Marieke Huisman
JACK - A Tool for Validation of Security and Behaviour of Java Applications. FMCO 2006: 152-174 - [c8]Gilles Barthe, Benjamin Grégoire, Fernando Pastawski
CIC[^( )]: Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions. LPAR 2006: 257-271 - [c7]Gilles Barthe, Benjamin Grégoire, César Kunz, Tamara Rezk:
Certificate Translation for Optimizing Compilers. SAS 2006: 301-317 - [c6]Gilles Barthe, Lennart Beringer, Pierre Crégut, Benjamin Grégoire, Martin Hofmann, Peter Müller, Erik Poll, Germán Puebla, Ian Stark
MOBIUS: Mobility, Ubiquity, Security. TGC 2006: 10-29 - [e1]Gilles Barthe
Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, Second International Workshop, CASSIS 2005, Nice, France, March 8-11, 2005, Revised Selected Papers. Lecture Notes in Computer Science 3956, Springer 2006, ISBN 3-540-33689-3 [contents] - 2005
- [c5]Bruno Barras, Benjamin Grégoire:
On the Role of Type Decorations in the Calculus of Inductive Constructions. CSL 2005: 151-166 - [c4]Gilles Barthe, Benjamin Grégoire, Fernando Pastawski
Practical Inference for Type-Based Termination in a Polymorphic Setting. TLCA 2005: 71-85 - [c3]Benjamin Grégoire, Assia Mahboubi:
Proving Equalities in a Commutative Ring Done Right in Coq. TPHOLs 2005: 98-113 - 2004
- [c2]Yves Bertot, Benjamin Grégoire, Xavier Leroy:
A Structured Approach to Proving Compiler Optimizations Based on Dataflow Analysis. TYPES 2004: 66-81 - 2002
- [c1]Benjamin Grégoire, Xavier Leroy:
A compiled implementation of strong reduction. ICFP 2002: 235-246
Coauthor Index
[j13] [j12] [j11] [c79] [i44] [i43] [i42] [i41] [j10] [j9] [c76] [c74] [i40] [i39] [i37] [c73] [i36] [i35] [j7] [c72] [c71] [c70] [c69] [i34] [i33] [i32] [j6] [j5] [c67] [i30] [i29] [c66] [c65] [c64] [c63] [c62] [i28] [i27] [i26] [i25] [j4] [c61] [c58] [c57] [c56] [i24] [i22] [i21] [i20] [i19] [c55] [c54] [c53] [c52] [c51] [i18] [i17] [i16] [i15] [i14] [c50] [c49] [c48] [c47] [i13] [i12] [i11] [i10] [i9] [c46] [c45] [c44] [i8] [i7] [i6] [c43] [c42] [c41] [c40] [i5] [i4] [i3] [j3] [c39] [c38] [c37] [c36] [c35] [c34] [c33] [c32] [c31] [i1] [c28] [c27] [c26] [c24] [j1] [c22] [c21] [c20] [c18] [c17] [c16] [c15] [c13] [c9] [c8] [c7] [c6] [e1] [c4]
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-10-07 22:09 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: