Benjamin Grégoire

Orcid: 0000-0001-6650-9924

Affiliations:
  • Research Centre Inria Sophia Antipolis - Méditerranée: Valbonne, France


According to our database1, Benjamin Grégoire authored at least 98 papers between 2002 and 2024.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
Masking the GLP Lattice-Based Signature Scheme at Any Order.
J. Cryptol., March, 2024

High-assurance zeroization.
IACR Trans. Cryptogr. Hardw. Embed. Syst., 2024

2023
Mechanized Proofs of Adversarial Complexity and Application to Universal Composability.
ACM Trans. Priv. Secur., August, 2023

Formally verifying Kyber Episode IV: Implementation correctness.
IACR Trans. Cryptogr. Hardw. Embed. Syst., 2023

Machine-Checked Security for $\mathrm{XMSS}$ as in RFC 8391 and $\mathrm{SPHINCS}^{+}$.
IACR Cryptol. ePrint Arch., 2023

Fixing and Mechanizing the Security Proof of Fiat-Shamir with Aborts and Dilithium.
IACR Cryptol. ePrint Arch., 2023

Formally verifying Kyber Part I: Implementation Correctness.
IACR Cryptol. ePrint Arch., 2023

Machine-Checked Security for rmXMSS as in RFC 8391 and $\mathrm {SPHINCS^{+}} $.
Proceedings of the Advances in Cryptology - CRYPTO 2023, 2023

Practical and Sound Equality Tests, Automatically: Deriving eqType Instances for Jasmin's Data Types with Coq-Elpi.
Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2023

2022
Enforcing fine-grained constant-time policies.
IACR Cryptol. ePrint Arch., 2022

Typing High-Speed Cryptography against Spectre v1.
IACR Cryptol. ePrint Arch., 2022

2021
Masking in Fine-Grained Leakage Models: Construction, Implementation and Verification.
IACR Trans. Cryptogr. Hardw. Embed. Syst., 2021

Hardware Private Circuits: From Trivial Composition to Full Verification.
IEEE Trans. Computers, 2021

Structured Leakage and Applications to Cryptographic Constant-Time and Cost.
IACR Cryptol. ePrint Arch., 2021

EasyPQC: Verifying Post-Quantum Cryptography.
IACR Cryptol. ePrint Arch., 2021

High-Assurance Cryptography in the Spectre Era.
Proceedings of the 42nd IEEE Symposium on Security and Privacy, 2021

2020
Formal verification of a constant-time preserving C compiler.
Proc. ACM Program. Lang., 2020

Improved parallel mask refreshing algorithms: generic solutions with parametrized non-interference and automated optimizations.
J. Cryptogr. Eng., 2020

High-Assurance Cryptography Software in the Spectre Era.
IACR Cryptol. ePrint Arch., 2020

The Last Mile: High-Assurance and High-Speed Cryptographic Implementations.
Proceedings of the 2020 IEEE Symposium on Security and Privacy, 2020

Security Analysis of ElGamal Implementations.
Proceedings of the 17th International Joint Conference on e-Business and Telecommunications, 2020

2019
A Machine-Checked Proof of Security for AWS Key Management Service.
IACR Cryptol. ePrint Arch., 2019

Machine-Checked Proofs for Cryptographic Standards.
IACR Cryptol. ePrint Arch., 2019

FaCT: a DSL for timing-sensitive computation.
Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2019

maskVerif: Automated Verification of Higher-Order Masking in Presence of Physical Defaults.
Proceedings of the Computer Security - ESORICS 2019, 2019

Symbolic Methods in Computational Cryptography Proofs.
Proceedings of the 32nd IEEE Computer Security Foundations Symposium, 2019

Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3.
Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, 2019

2018
Proving expected sensitivity of probabilistic programs.
Proc. ACM Program. Lang., 2018

Vectorizing Higher-Order Masking.
IACR Cryptol. ePrint Arch., 2018

Symbolic Proofs for Lattice-Based Cryptography.
IACR Cryptol. ePrint Arch., 2018

maskVerif: a formal tool for analyzing software and hardware masked implementations.
IACR Cryptol. ePrint Arch., 2018

Improved Parallel Mask Refreshing Algorithms: Generic Solutions with Parametrized Non-Interference & Automated Optimizations.
IACR Cryptol. ePrint Arch., 2018

An Assertion-Based Program Logic for Probabilistic Programs.
Proceedings of the Programming Languages and Systems, 2018

Secure Compilation of Side-Channel Countermeasures: The Case of Cryptographic "Constant-Time".
Proceedings of the 31st IEEE Computer Security Foundations Symposium, 2018

Formal Security Proof of CMAC and Its Variants.
Proceedings of the 31st IEEE Computer Security Foundations Symposium, 2018

2017
Provably secure compilation of side-channel countermeasures.
IACR Cryptol. ePrint Arch., 2017

A Note on 'Further Improving Efficiency of Higher-Order Masking Scheme by Decreasing Randomness Complexity'.
IACR Cryptol. ePrint Arch., 2017

A Fast and Verified Software Stack for Secure Function Evaluation.
IACR Cryptol. ePrint Arch., 2017

Coupling proofs are probabilistic product programs.
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017

Proving uniformity and independence by self-composition and coupling.
Proceedings of the LPAR-21, 2017

Jasmin: High-Assurance and High-Speed Cryptography.
Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, 2017

2016
Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model.
IACR Cryptol. ePrint Arch., 2016

Advanced Probabilistic Couplings for Differential Privacy.
CoRR, 2016

Proving Differential Privacy via Probabilistic Couplings.
Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, 2016

A Program Logic for Union Bounds.
Proceedings of the 43rd International Colloquium on Automata, Languages, and Programming, 2016

Advanced Probabilistic Couplings for Differential Privacy.
Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, 2016

Strong Non-Interference and Type-Directed Higher-Order Masking.
Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, 2016

2015
Verified Proofs of Higher-Order Masking.
IACR Cryptol. ePrint Arch., 2015

Compositional Verification of Higher-Order Masking: Application to a Verifying Masking Compiler.
IACR Cryptol. ePrint Arch., 2015

Relational Reasoning via Probabilistic Coupling.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2015

Automated Proofs of Pairing-Based Cryptography.
Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security, 2015

2014
Synthesis of Fault Attacks on Cryptographic Implementations.
IACR Cryptol. ePrint Arch., 2014

Making RSA-PSS Provably Secure Against Non-Random Faults.
IACR Cryptol. ePrint Arch., 2014

Verified Implementations for Secure and Verifiable Computation.
IACR Cryptol. ePrint Arch., 2014

Probabilistic relational verification for cryptographic implementations.
Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014

Certified Synthesis of Efficient Batch Verifiers.
Proceedings of the IEEE 27th Computer Security Foundations Symposium, 2014

2013
Verified indifferentiable hashing into elliptic curves.
J. Comput. Secur., 2013

EasyCrypt: A Tutorial.
Proceedings of the Foundations of Security Analysis and Design VII, 2013

Verified Computational Differential Privacy with Applications to Smart Metering.
Proceedings of the 2013 IEEE 26th Computer Security Foundations Symposium, 2013

Fully automated analysis of padding-based encryption in the computational model.
Proceedings of the 2013 ACM SIGSAC Conference on Computer and Communications Security, 2013

2012
Automated Analysis and Synthesis of Padding-Based Encryption Schemes.
IACR Cryptol. ePrint Arch., 2012

Recent Advances in the Formal Verification of Cryptographic Systems: Turing's Legacy
ERCIM News, 2012

Computer-Aided Cryptographic Proofs.
Proceedings of the Static Analysis - 19th International Symposium, 2012

Probabilistic Relational Hoare Logics for Computer-Aided Security Proofs.
Proceedings of the Mathematics of Program Construction - 11th International Conference, 2012

Computer-Aided Cryptographic Proofs.
Proceedings of the Interactive Theorem Proving - Third International Conference, 2012

Verified Security of Merkle-Damgård.
Proceedings of the 25th IEEE Computer Security Foundations Symposium, 2012

Automation in Computer-Aided Cryptography: Proofs, Attacks and Designs.
Proceedings of the Certified Programs and Proofs - Second International Conference, 2012

2011
Certifying compilers using higher-order theorem provers as certificate checkers.
Formal Methods Syst. Des., 2011

Beyond Provable Security Verifiable IND-CCA Security of OAEP.
Proceedings of the Topics in Cryptology - CT-RSA 2011, 2011

Computer-Aided Security Proofs for the Working Cryptographer.
Proceedings of the Advances in Cryptology - CRYPTO 2011, 2011

Full Reduction at Full Throttle.
Proceedings of the Certified Programs and Proofs - First International Conference, 2011

A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses.
Proceedings of the Certified Programs and Proofs - First International Conference, 2011

2010
On Strong Normalization of the Calculus of Constructions with Type-Based Termination.
Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2010

Programming Language Techniques for Cryptographic Proofs.
Proceedings of the Interactive Theorem Proving, First International Conference, 2010

Extending Coq with Imperative Features and Its Application to SAT Verification.
Proceedings of the Interactive Theorem Proving, First International Conference, 2010

A Machine-Checked Formalization of Sigma-Protocols.
Proceedings of the 23rd IEEE Computer Security Foundations Symposium, 2010

2009
Certificate translation for optimizing compilers.
ACM Trans. Program. Lang. Syst., 2009

Formally Certifying the Security of Digital Signature Schemes.
Proceedings of the 30th IEEE Symposium on Security and Privacy (SP 2009), 2009

Formal certification of code-based cryptographic proofs.
Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2009

Implementing a Direct Method for Certificate Translation.
Proceedings of the Formal Methods and Software Engineering, 2009

2008
A New Elimination Rule for the Calculus of Inductive Constructions.
Proceedings of the Types for Proofs and Programs, International Conference, 2008

A Tutorial on Type-Based Termination.
Proceedings of the Language Engineering and Rigorous Software Development, International LerNet ALFA Summer School 2008, Piriapolis, Uruguay, February 24, 2008

Formal Certification of ElGamal Encryption.
Proceedings of the Formal Aspects in Security and Trust, 5th International Workshop, 2008

Type-Based Termination with Sized Products.
Proceedings of the Computer Science Logic, 22nd International Workshop, 2008

Preservation of Proof Obligations from Java to the Java Virtual Machine.
Proceedings of the Automated Reasoning, 4th International Joint Conference, 2008

Proof Certificates for Algebra and Their Application to Automatic Geometry Theorem Proving.
Proceedings of the Automated Deduction in Geometry - 7th International Workshop, 2008

2007
Combining a Verification Condition Generator for a Bytecode Language with Static Analyses.
Proceedings of the Trustworthy Global Computing, Third Symposium, 2007

The MOBIUS Proof Carrying Code Infrastructure.
Proceedings of the Formal Methods for Components and Objects, 6th International Symposium, 2007

2006
MOBIUS: Mobility, Ubiquity, Security.
Proceedings of the Trustworthy Global Computing, Second Symposium, 2006

CIC[^( )]: Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions.
Proceedings of the Logic for Programming, 2006

JACK - A Tool for Validation of Security and Behaviour of Java Applications.
Proceedings of the Formal Methods for Components and Objects, 5th International Symposium, 2006

A Computational Approach to Pocklington Certificates in Type Theory.
Proceedings of the Functional and Logic Programming, 8th International Symposium, 2006

A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers.
Proceedings of the Automated Reasoning, Third International Joint Conference, 2006

2005
Proving Equalities in a Commutative Ring Done Right in Coq.
Proceedings of the Theorem Proving in Higher Order Logics, 18th International Conference, 2005

Practical Inference for Type-Based Termination in a Polymorphic Setting.
Proceedings of the Typed Lambda Calculi and Applications, 7th International Conference, 2005

On the Role of Type Decorations in the Calculus of Inductive Constructions.
Proceedings of the Computer Science Logic, 19th International Workshop, 2005

2004
A Structured Approach to Proving Compiler Optimizations Based on Dataflow Analysis.
Proceedings of the Types for Proofs and Programs, International Workshop, 2004

2002
A compiled implementation of strong reduction.
Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming (ICFP '02), 2002


  Loading...