Google
Google Scholar
MS Academic
CiteSeerX
CORE
Semantic ScholarBenjamin Grégoire
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
showing all ?? records
2010 – today
- 2018
[j4]Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
Proving expected sensitivity of probabilistic programs. PACMPL 2(POPL): 57:1-57:29 (2018)- [c60]Benjamin Grégoire, Kostas Papagiannopoulos, Peter Schwabe, Ko Stoffelen:
Vectorizing Higher-Order Masking. COSADE 2018: 23-43 - [c59]Cecile Baritel-Ruet, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire:
Formal Security Proof of CMAC and Its Variants. CSF 2018: 91-104 - [c58]Gilles Barthe, Benjamin Grégoire, Vincent Laporte:
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, Pierre-Yves Strub:
An Assertion-Based Program Logic for Probabilistic Programs. ESOP 2018: 117-144 - [c56]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: 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 Cryptology ePrint Archive 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 Cryptology ePrint Archive 2018: 381 (2018) - [i21]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 Cryptology ePrint Archive 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 Cryptology ePrint Archive 2018: 562 (2018) - [i19]Gilles Barthe, Xiong Fan, Joshua Gancher, Benjamin Grégoire, Charlie Jacomme, Elaine Shi:
Symbolic Proofs for Lattice-Based Cryptography. IACR Cryptology ePrint Archive 2018: 765 (2018) - 2017
- [c55]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: 1807-1823 - [c54]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: 1989-2006 - [c53]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: 535-566 - [c52]Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
Proving uniformity and independence by self-composition and coupling. LPAR 2017: 385-403 - [c51]Gilles Barthe, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
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 Cryptology ePrint Archive 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 Cryptology ePrint Archive 2017: 1053 (2017) - [i14]Gilles Barthe, Benjamin Grégoire, Vincent Laporte:
Provably secure compilation of side-channel countermeasures. IACR Cryptology ePrint Archive 2017: 1233 (2017) - 2016
- [c50]Gilles Barthe, Noémie Fong, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
Advanced Probabilistic Couplings for Differential Privacy. ACM Conference on Computer and Communications Security 2016: 55-67 - [c49]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. ACM Conference on Computer and Communications Security 2016: 116-129 - [c48]Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
A Program Logic for Union Bounds. ICALP 2016: 107:1-107:15 - [c47]Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub:
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 Cryptology ePrint Archive 2016: 912 (2016) - 2015
- [c46]Gilles Barthe, Benjamin Grégoire, Benedikt Schmidt:
Automated Proofs of Pairing-Based Cryptography. ACM Conference on Computer and Communications Security 2015: 1156-1168 - [c45]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: 457-485 - [c44]Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Léo Stefanesco, Pierre-Yves Strub:
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 Cryptology ePrint Archive 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 Cryptology ePrint Archive 2015: 506 (2015) - 2014
- [c43]Gilles Barthe, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Jean-Christophe Zapalowicz:
Synthesis of Fault Attacks on Cryptographic Implementations. ACM Conference on Computer and Communications Security 2014: 1016-1027 - [c42]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: 206-222 - [c41]Joseph A. Akinyele, Gilles Barthe, Benjamin Grégoire, Benedikt Schmidt, Pierre-Yves Strub:
Certified Synthesis of Efficient Batch Verifiers. CSF 2014: 153-165 - [c40]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: 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 Cryptology ePrint Archive 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 Cryptology ePrint Archive 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 Cryptology ePrint Archive 2014: 456 (2014) - 2013
- [j3]Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Federico Olmedo, Santiago Zanella Béguelin:
Verified indifferentiable hashing into elliptic curves. Journal of Computer Security 21(6): 881-917 (2013) - [c39]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. ACM Conference on Computer and Communications Security 2013: 1247-1260 - [c38]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: 287-301 - [c37]Gilles Barthe, François Dupressoir, Benjamin Grégoire, César Kunz, Benedikt Schmidt, Pierre-Yves Strub:
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, Matthias Berg, Benjamin Grégoire, César Kunz, Malte Skoruppa, Santiago Zanella Béguelin:
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, Santiago Zanella Béguelin:
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 Cryptology ePrint Archive 2012: 695 (2012) - 2011
- [j2]Jan Olaf Blech, Benjamin Grégoire:
Certifying compilers using higher-order theorem provers as certificate checkers. Formal Methods in System Design 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, Daniel Hedin, Santiago Zanella Béguelin, Benjamin Grégoire, Sylvain Heraud:
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, Benjamin Grégoire, César Kunz, Tamara Rezk:
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, Benjamin Grégoire, Santiago Zanella Béguelin:
Formal certification of code-based cryptographic proofs. POPL 2009: 90-101 - [c20]Santiago Zanella Béguelin, Gilles Barthe, Benjamin Grégoire, Federico Olmedo:
Formally Certifying the Security of Digital Signature Schemes. IEEE Symposium on Security and Privacy 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, Jean-Louis Lanet, Mariela Pavlova, Antoine Requet:
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, Eric Vétillard:
MOBIUS: Mobility, Ubiquity, Security. TGC 2006: 10-29 - [e1]Gilles Barthe, Benjamin Grégoire, Marieke Huisman, Jean-Louis Lanet:
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]
Coauthor Index
[j4] [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]
maintained by 
at 
at 
last updated on 2018-10-11 09:00 CEST by the dblp team
data released under the ODC-BY 1.0 license
see also: Terms of Use | Privacy Policy | Imprint