| Publication | Date of Publication | Type |
|---|
| Formally verifying Kyber. Episode V: machine-checked IND-CCA security and correctness of ML-KEM in Easycrypt | 2024-12-04 | Paper |
Fixing and mechanizing the security proof of Fiat-Shamir with aborts and Dilithium
Advances in Cryptology – CRYPTO 2023 | 2024-02-06 | Paper |
Machine-checked security for XMSS as in RFC 8391 and SPHINCS\textsuperscript{+}
Advances in Cryptology – CRYPTO 2023 | 2024-02-06 | Paper |
Masking the GLP lattice-based signature scheme at any order
Journal of Cryptology | 2024-01-23 | Paper |
Hardware Private Circuits: From Trivial Composition to Full Verification
IEEE Transactions on Computers | 2022-03-23 | Paper |
Vectorizing higher-order masking
Constructive Side-Channel Analysis and Secure Design | 2020-07-20 | Paper |
| scientific article; zbMATH DE number 7178368 (Why is no real title available?) | 2020-03-09 | Paper |
An assertion-based program logic for probabilistic programs
(available as arXiv preprint) | 2019-09-13 | Paper |
Proving uniformity and independence by self-composition and coupling
EPiC Series in Computing | 2019-01-10 | Paper |
| Masking the GLP lattice-based signature scheme at any order | 2018-07-09 | Paper |
Proving differential privacy via probabilistic couplings
Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science | 2018-04-23 | Paper |
scientific article; zbMATH DE number 6820296 (Why is no real title available?)
(available as arXiv preprint) | 2017-12-19 | Paper |
Coupling proofs are probabilistic product programs
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages | 2017-10-20 | Paper |
Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model
Lecture Notes in Computer Science | 2017-06-13 | Paper |
Relational reasoning via probabilistic coupling
Logic for Programming, Artificial Intelligence, and Reasoning | 2016-01-12 | Paper |
A compiled implementation of strong reduction
Proceedings of the seventh ACM SIGPLAN international conference on Functional programming | 2015-10-07 | Paper |
Verified Proofs of Higher-Order Masking
Advances in Cryptology -- EUROCRYPT 2015 | 2015-09-30 | Paper |
Making RSA–PSS Provably Secure against Non-random Faults
Advanced Information Systems Engineering | 2015-07-21 | Paper |
Formal certification of code-based cryptographic proofs
Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages | 2015-07-03 | Paper |
EasyCrypt: a tutorial
Foundations of Security Analysis and Design VII | 2015-05-27 | Paper |
Probabilistic relational verification for cryptographic implementations
Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | 2014-04-10 | Paper |
Computer-aided cryptographic proofs
Interactive Theorem Proving | 2012-09-20 | Paper |
Probabilistic relational Hoare logics for computer-aided security proofs
Lecture Notes in Computer Science | 2012-09-05 | Paper |
Verified indifferentiable hashing into elliptic curves
Lecture Notes in Computer Science | 2012-06-29 | Paper |
A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses
Certified Programs and Proofs | 2011-11-22 | Paper |
Computer-Aided Security Proofs for the Working Cryptographer
Advances in Cryptology – CRYPTO 2011 | 2011-08-12 | Paper |
Proof certificates for algebra and their application to automatic geometry theorem proving
Automated Deduction in Geometry | 2011-05-26 | Paper |
Certifying compilers using higher-order theorem provers as certificate checkers
Formal Methods in System Design | 2011-03-31 | Paper |
Beyond provable security verifiable IND-CCA security of OAEP
Topics in Cryptology – CT-RSA 2011 | 2011-02-11 | Paper |
On strong normalization of the calculus of constructions with type-based termination
Logic for Programming, Artificial Intelligence, and Reasoning | 2010-10-12 | Paper |
Extending Coq with Imperative Features and Its Application to SAT Verification
Interactive Theorem Proving | 2010-09-14 | Paper |
Programming language techniques for cryptographic proofs
Interactive Theorem Proving | 2010-09-14 | Paper |
A Tutorial on Type-Based Termination
Language Engineering and Rigorous Software Development | 2009-07-28 | Paper |
A New Elimination Rule for the Calculus of Inductive Constructions
Lecture Notes in Computer Science | 2009-07-02 | Paper |
Formal Certification of ElGamal Encryption
Formal Aspects in Security and Trust | 2009-04-07 | Paper |
A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers
Automated Reasoning | 2009-03-12 | Paper |
Certificate Translation for Optimizing Compilers
Static Analysis | 2009-03-12 | Paper |
Preservation of Proof Obligations from Java to the Java Virtual Machine
Automated Reasoning | 2008-11-27 | Paper |
Type-Based Termination with Sized Products
Computer Science Logic | 2008-11-20 | Paper |
CIC $\widehat{~}$ : Type-Based Termination of Recursive Definitions in the Calculus of Inductive Constructions
Logic for Programming, Artificial Intelligence, and Reasoning | 2008-05-27 | Paper |
A Computational Approach to Pocklington Certificates in Type Theory
Functional and Logic Programming | 2007-05-02 | Paper |
Types for Proofs and Programs
Lecture Notes in Computer Science | 2006-11-13 | Paper |
Computer Science Logic
Lecture Notes in Computer Science | 2006-11-01 | Paper |
Theorem Proving in Higher Order Logics
Lecture Notes in Computer Science | 2006-07-06 | Paper |
Typed Lambda Calculi and Applications
Lecture Notes in Computer Science | 2005-11-11 | Paper |
