Google
Google Scholar
MS Academic
CiteSeerX
CORE
Semantic ScholarBenjamin Grégoire
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
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)- [c61]Gilles Barthe, Xiong Fan, Joshua Gancher, Benjamin Grégoire, Charlie Jacomme, Elaine Shi:
Symbolic Proofs for Lattice-Based Cryptography. ACM Conference on Computer and Communications Security 2018: 538-555 - [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. ACM Conference on Computer and Communications Security 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. ACM Conference on Computer and Communications Security 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] [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]
maintained by 
, founded at 
, founded at 
last updated on 2019-01-09 01:16 CET by the dblp team
data released under the ODC-BY 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
the dblp computer science bibliography is funded by:
