Benjamin Grégoire

Available identifiers

zbMath Open gregoire.benjaminMaRDI QIDQ633301

List of research outcomes

Publication	Date of Publication	Type
Fixing and mechanizing the security proof of Fiat-Shamir with aborts and Dilithium	2024-02-06	Paper
Machine-checked security for XMSS as in RFC 8391 and SPHINCS\textsuperscript{+}	2024-02-06	Paper
Masking the GLP lattice-based signature scheme at any order	2024-01-23	Paper
Hardware Private Circuits: From Trivial Composition to Full Verification	2022-03-23	Paper
Vectorizing Higher-Order Masking	2020-07-20	Paper
https://portal.mardi4nfdi.de/entity/Q5219933	2020-03-09	Paper
An assertion-based program logic for probabilistic programs	2019-09-13	Paper
Proving uniformity and independence by self-composition and coupling	2019-01-10	Paper
Masking the GLP lattice-based signature scheme at any order	2018-07-09	Paper
Proving Differential Privacy via Probabilistic Couplings	2018-04-23	Paper
https://portal.mardi4nfdi.de/entity/Q4598248	2017-12-19	Paper
Coupling proofs are probabilistic product programs	2017-10-20	Paper
Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model	2017-06-13	Paper
Relational Reasoning via Probabilistic Coupling	2016-01-12	Paper
A compiled implementation of strong reduction	2015-10-07	Paper
Verified Proofs of Higher-Order Masking	2015-09-30	Paper
Making RSA–PSS Provably Secure against Non-random Faults	2015-07-21	Paper
Formal certification of code-based cryptographic proofs	2015-07-03	Paper
EasyCrypt: A Tutorial	2015-05-27	Paper
Probabilistic relational verification for cryptographic implementations	2014-04-10	Paper
Computer-Aided Cryptographic Proofs	2012-09-20	Paper
Probabilistic Relational Hoare Logics for Computer-Aided Security Proofs	2012-09-05	Paper
Verified Indifferentiable Hashing into Elliptic Curves	2012-06-29	Paper
A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses	2011-11-22	Paper
Computer-Aided Security Proofs for the Working Cryptographer	2011-08-12	Paper
Proof Certificates for Algebra and Their Application to Automatic Geometry Theorem Proving	2011-05-26	Paper
Certifying compilers using higher-order theorem provers as certificate checkers	2011-03-31	Paper
Beyond Provable Security Verifiable IND-CCA Security of OAEP	2011-02-11	Paper
On Strong Normalization of the Calculus of Constructions with Type-Based Termination	2010-10-12	Paper
Extending Coq with Imperative Features and Its Application to SAT Verification	2010-09-14	Paper
Programming Language Techniques for Cryptographic Proofs	2010-09-14	Paper
A Tutorial on Type-Based Termination	2009-07-28	Paper
A New Elimination Rule for the Calculus of Inductive Constructions	2009-07-02	Paper
Formal Certification of ElGamal Encryption	2009-04-07	Paper
Certificate Translation for Optimizing Compilers	2009-03-12	Paper
A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers	2009-03-12	Paper
Preservation of Proof Obligations from Java to the Java Virtual Machine	2008-11-27	Paper
Type-Based Termination with Sized Products	2008-11-20	Paper
CIC $\widehat{~}$ : Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions	2008-05-27	Paper
A Computational Approach to Pocklington Certificates in Type Theory	2007-05-02	Paper
Types for Proofs and Programs	2006-11-13	Paper
Computer Science Logic	2006-11-01	Paper
Theorem Proving in Higher Order Logics	2006-07-06	Paper
Typed Lambda Calculi and Applications	2005-11-11	Paper

Research outcomes over time

Doctoral students

No records found.

Known relations from the MaRDI Knowledge Graph

Property	Value
MaRDI profile type	MaRDI person profile
instance of	human

This page was built for person: Benjamin Grégoire