Benjamin Grégoire

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

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

On csauthors.net:

Bibliography

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

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

2018
Proving expected sensitivity of probabilistic programs.
PACMPL, 2018

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

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

Masking the GLP Lattice-Based Signature Scheme at Any Order.
Proceedings of the Advances in Cryptology - EUROCRYPT 2018 - 37th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Tel Aviv, Israel, April 29, 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

Vectorizing Higher-Order Masking.
Proceedings of the Constructive Side-Channel Analysis and Secure Design, 2018

Symbolic Proofs for Lattice-Based Cryptography.
Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, 2018

2017
Provably secure compilation of side-channel countermeasures.
IACR Cryptology ePrint Archive, 2017

A Note on 'Further Improving Efficiency of Higher-Order Masking Scheme by Decreasing Randomness Complexity'.
IACR Cryptology ePrint Archive, 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

Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model.
Proceedings of the Advances in Cryptology - EUROCRYPT 2017 - 36th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Paris, France, April 30, 2017

A Fast and Verified Software Stack for Secure Function Evaluation.
Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, TX, USA, October 30, 2017

Jasmin: High-Assurance and High-Speed Cryptography.
Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, TX, USA, October 30, 2017

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
Compositional Verification of Higher-Order Masking: Application to a Verifying Masking Compiler.
IACR Cryptology ePrint Archive, 2015

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

Verified Proofs of Higher-Order Masking.
Proceedings of the Advances in Cryptology - EUROCRYPT 2015, 2015

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

2014
Verified Implementations for Secure and Verifiable Computation.
IACR Cryptology ePrint Archive, 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

Making RSA-PSS Provably Secure against Non-random Faults.
Proceedings of the Cryptographic Hardware and Embedded Systems - CHES 2014, 2014

Synthesis of Fault Attacks on Cryptographic Implementations.
Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, 2014

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 Cryptology ePrint Archive, 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

Verified Indifferentiable Hashing into Elliptic Curves.
Proceedings of the Principles of Security and Trust - First International Conference, 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 in System Design, 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
Formally Certifying the Security of Digital Signature Schemes.
Proceedings of the 30th IEEE Symposium on Security and Privacy (S&P 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

Certificate Translation for Optimizing Compilers.
Proceedings of the Static Analysis, 13th International 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...