| 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 | 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 |
| A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers | 2009-03-12 | Paper |
| Certificate Translation for Optimizing Compilers | 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 |
