Pierre-Yves Strub

Available identifiers

zbMath Open strub.pierre-yvesMaRDI QIDQ2323969

List of research outcomes

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
Machine-checked security for XMSS as in RFC 8391 and SPHINCS\textsuperscript{+}	2024-02-06	Paper
https://portal.mardi4nfdi.de/entity/Q6157249	2023-06-20	Paper
Formal verification of Saber's public-key encryption scheme in easycrypt	2023-06-12	Paper
Formalizing the Face Lattice of Polyhedra	2022-11-09	Paper
Formalizing the face lattice of polyhedra	2022-08-02	Paper
Formalizing the Face Lattice of Polyhedra	2021-04-30	Paper
\(*\)-liftings for differential privacy	2020-05-27	Paper
https://portal.mardi4nfdi.de/entity/Q5219933	2020-03-09	Paper
Relational \(\star\)-liftings for differential privacy	2020-01-03	Paper
An assertion-based program logic for probabilistic programs	2019-09-13	Paper
Theory of types and decision procedures	2019-02-15	Paper
Coq without type casts: a complete proof of Coq Modulo Theory	2019-01-10	Paper
Proving uniformity and independence by self-composition and coupling	2019-01-10	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
Computer-aided verification for mechanism design	2017-02-10	Paper
Dependent types and multi-monadic effects in \(\mathrm{F}^*\)	2016-10-24	Paper
Higher-order approximate relational refinement types for mechanism design and differential privacy	2016-09-29	Paper
Relational reasoning via probabilistic coupling	2016-01-12	Paper
Verified Proofs of Higher-Order Masking	2015-09-30	Paper
Self-certification: bootstrapping certified typecheckers in F\(^\ast\) with Coq	2015-09-11	Paper
EasyCrypt: a tutorial	2015-05-27	Paper
Secure distributed programming with value-dependent types	2015-03-05	Paper
Fully abstract compilation to JavaScript	2014-11-27	Paper
A formal library for elliptic curves in the Coq proof assistant	2014-09-08	Paper
Proving the TLS handshake secure (as it is)	2014-08-07	Paper
Gradual typing embedded securely in JavaScript	2014-04-10	Paper
Probabilistic relational verification for cryptographic implementations	2014-04-10	Paper
Secure distributed programming with value-dependent types	2014-02-27	Paper
Coq Modulo Theory	2010-09-03	Paper
Building Decision Procedures in the Calculus of Inductive Constructions	2009-03-05	Paper

Research outcomes over time

This page was built for person: Pierre-Yves Strub