Pierre-Yves Strub

ORCID

Publication Activity (10 Years)

Years Active: 2001-2024
Publications (10 Years): 77

Top Venues

CoRR

IACR Cryptol. ePrint Arch.

CCS

POPL

École Polytechnique, Palaiseau, France (PHD)

Education History

École Polytechnique, Palaiseau, France

PHD

Publications

Manuel Barbosa, François Dupressoir, Andreas Hülsing, Matthias Meijers, Pierre-Yves Strub
A Tight Security Proof for $\mathrm{SPHINCS^{+}}$, Formally Verified. IACR Cryptol. ePrint Arch. 2024 (2024)
José Bacelar Almeida, Santiago Arranz Olmos, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Cameron Low, Tiago Oliveira, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Pierre-Yves Strub
Formally verifying Kyber Episode V: Machine-checked IND-CCA security and correctness of ML-KEM in EasyCrypt. IACR Cryptol. ePrint Arch. 2024 (2024)
José Bacelar Almeida, Santiago Arranz Olmos, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Cameron Low, Tiago Oliveira, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Pierre-Yves Strub
Formally Verifying Kyber - Episode V: Machine-Checked IND-CCA Security and Correctness of ML-KEM in EasyCrypt. CRYPTO (2) (2024)
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Tiago Oliveira, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Antoine Séré, Pierre-Yves Strub
Formally verifying Kyber Part I: Implementation Correctness. IACR Cryptol. ePrint Arch. 2023 (2023)
Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Pierre-Yves Strub
Mechanized Proofs of Adversarial Complexity and Application to Universal Composability. ACM Trans. Priv. Secur. 26 (3) (2023)
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Vincent Laporte, Jean-Christophe Léchenet, Tiago Oliveira, Hugo Pacheco, Miguel Quaresma, Peter Schwabe, Antoine Séré, Pierre-Yves Strub
Formally verifying Kyber Episode IV: Implementation correctness. IACR Trans. Cryptogr. Hardw. Embed. Syst. 2023 (3) (2023)
Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, Mingsheng Ying
CoqQ: Foundational Verification of Quantum Programs. Proc. ACM Program. Lang. 7 (POPL) (2023)
Xavier Allamigeon, Quentin Canu, Pierre-Yves Strub
A Formal Disproof of Hirsch Conjecture. CPP (2023)
Xavier Allamigeon, Quentin Canu, Pierre-Yves Strub
A Formal Disproof of the Hirsch Conjecture. CoRR (2023)
Manuel Barbosa, François Dupressoir, Benjamin Grégoire, Andreas Hülsing, Matthias Meijers, Pierre-Yves Strub
Machine-Checked Security for $\mathrm{XMSS}$ as in RFC 8391 and $\mathrm{SPHINCS}^{+}$. IACR Cryptol. ePrint Arch. 2023 (2023)
Pablo Donato, Pierre-Yves Strub, Benjamin Werner
A drag-and-drop proof tactic. CPP (2022)
Manuel Barbosa, François Dupressoir, Benjamin Grégoire, Andreas Hülsing, Matthias Meijers, Pierre-Yves Strub
Machine-Checked Security for rmXMSS as in RFC 8391 and $\mathrm {SPHINCS^{+}} $. CRYPTO (5) (2022)
Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, Mingsheng Ying
CoqQ: Foundational Verification of Quantum Programs. CoRR (2022)
Xavier Allamigeon, Ricardo D. Katz, Pierre-Yves Strub
Formalizing the Face Lattice of Polyhedra. Log. Methods Comput. Sci. 18 (2) (2022)
Andreas Hülsing, Matthias Meijers, Pierre-Yves Strub
Formal Verification of Saber's Public-Key Encryption Scheme in EasyCrypt. IACR Cryptol. ePrint Arch. 2022 (2022)
Andreas Hülsing, Matthias Meijers, Pierre-Yves Strub
Formal Verification of Saber's Public-Key Encryption Scheme in EasyCrypt. CRYPTO (1) (2022)
Pablo Donato, Pierre-Yves Strub, Benjamin Werner
A drag-and-drop proof tactic. CoRR (2022)
Manuel Barbosa, Gilles Barthe, Xiong Fan, Benjamin Grégoire, Shih-Han Hung, Jonathan Katz, Pierre-Yves Strub, Xiaodi Wu, Li Zhou
EasyPQC: Verifying Post-Quantum Cryptography. IACR Cryptol. ePrint Arch. 2021 (2021)
Xavier Allamigeon, Ricardo D. Katz, Pierre-Yves Strub
Formalizing the Face Lattice of Polyhedra. CoRR (2021)
Manuel Barbosa, Gilles Barthe, Xiong Fan, Benjamin Grégoire, Shih-Han Hung, Jonathan Katz, Pierre-Yves Strub, Xiaodi Wu, Li Zhou
EasyPQC: Verifying Post-Quantum Cryptography. CCS (2021)
Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Pierre-Yves Strub
Mechanized Proofs of Adversarial Complexity and Application to Universal Composability. CCS (2021)
Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Pierre-Yves Strub
Mechanized Proofs of Adversarial Complexity and Application to Universal Composability. IACR Cryptol. ePrint Arch. 2021 (2021)
Sophie Bernard, Cyril Cohen, Assia Mahboubi, Pierre-Yves Strub
Unsolvability of the Quintic Formalized in Dependent Type Theory. ITP (2021)
Xavier Allamigeon, Ricardo D. Katz, Pierre-Yves Strub
Formalizing the Face Lattice of Polyhedra. IJCAR (2) (2020)
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Vincent Laporte, Tiago Oliveira, Pierre-Yves Strub
The Last Mile: High-Assurance and High-Speed Cryptographic Implementations. IEEE Symposium on Security and Privacy (2020)
Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, François-Xavier Standaert, Pierre-Yves Strub
Improved parallel mask refreshing algorithms: generic solutions with parametrized non-interference and automated optimizations. J. Cryptogr. Eng. 10 (1) (2020)
José Bacelar Almeida, Cécile Baritel-Ruet, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Alley Stoughton, Pierre-Yves Strub
Machine-Checked Proofs for Cryptographic Standards. IACR Cryptol. ePrint Arch. 2019 (2019)
José Bacelar Almeida, Cécile Baritel-Ruet, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Alley Stoughton, Pierre-Yves Strub
Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3. CCS (2019)
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Matthew Campagna, Ernie Cohen, Benjamin Grégoire, Vitor Pereira, Bernardo Portela, Pierre-Yves Strub, Serdar Tasiran
A Machine-Checked Proof of Security for AWS Key Management Service. IACR Cryptol. ePrint Arch. 2019 (2019)
Gilles Barthe, Thomas Espitau, Justin Hsu, Tetsuya Sato, Pierre-Yves Strub
Relational ⋆⋆\star-Liftings for Differential Privacy. Log. Methods Comput. Sci. 15 (4) (2019)
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Matthew Campagna, Ernie Cohen, Benjamin Grégoire, Vitor Pereira, Bernardo Portela, Pierre-Yves Strub, Serdar Tasiran
A Machine-Checked Proof of Security for AWS Key Management Service. CCS (2019)
Gilles Barthe, Benjamin Grégoire, Charlie Jacomme, Steve Kremer, Pierre-Yves Strub
Symbolic Methods in Computational Cryptography Proofs. CSF (2019)
Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Pierre-Yves Strub
A relational logic for higher-order programs. J. Funct. Program. 29 (2019)
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Benjamin Grégoire, Adrien Koutsos, Vincent Laporte, Tiago Oliveira, Pierre-Yves Strub
The Last Mile: High-Assurance and High-Speed Cryptographic Implementations. CoRR (2019)
Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, François-Xavier Standaert, Pierre-Yves Strub
Improved Parallel Mask Refreshing Algorithms: Generic Solutions with Parametrized Non-Interference & Automated Optimizations. IACR Cryptol. ePrint Arch. 2018 (2018)
Karthikeyan Bhargavan, Franziskus Kiefer, Pierre-Yves Strub
hacspec: Towards Verifiable Crypto Standards. SSR (2018)
Gilles Barthe, Thomas Espitau, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
An Assertion-Based Program Logic for Probabilistic Programs. ESOP (2018)
Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
Proving expected sensitivity of probabilistic programs. Proc. ACM Program. Lang. 2 (POPL) (2018)
Helene Haagh, Aleksandr Karbyshev, Sabine Oechsner, Bas Spitters, Pierre-Yves Strub
Computer-aided proofs for multiparty computation with active security. IACR Cryptol. ePrint Arch. 2018 (2018)
Helene Haagh, Aleksandr Karbyshev, Sabine Oechsner, Bas Spitters, Pierre-Yves Strub
Computer-Aided Proofs for Multiparty Computation with Active Security. CSF (2018)
Helene Haagh, Aleksandr Karbyshev, Sabine Oechsner, Bas Spitters, Pierre-Yves Strub
Computer-aided proofs for multiparty computation with active security. CoRR (2018)
Gilles Barthe, Thomas Espitau, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
An Assertion-Based Program Logic for Probabilistic Programs. CoRR (2018)
Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Pierre-Yves Strub
A Relational Logic for Higher-Order Programs. CoRR (2017)
Véronique Cortier, Constantin Catalin Dragan, François Dupressoir, Benedikt Schmidt, Pierre-Yves Strub, Bogdan Warinschi
Machine-Checked Proofs of Privacy for Electronic Voting Protocols. IEEE Symposium on Security and Privacy (2017)
Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
Proving Expected Sensitivity of Probabilistic Programs. CoRR (2017)
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Arthur Blot, Benjamin Grégoire, Vincent Laporte, Tiago Oliveira, Hugo Pacheco, Benedikt Schmidt, Pierre-Yves Strub
Jasmin: High-Assurance and High-Speed Cryptography. CCS (2017)
Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
Proving uniformity and independence by self-composition and coupling. LPAR (2017)
Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
Proving uniformity and independence by self-composition and coupling. CoRR (2017)
Jean-Pierre Jouannaud, Pierre-Yves Strub
Coq without Type Casts: A Complete Proof of Coq Modulo Theory. LPAR (2017)
Gilles Barthe, Thomas Espitau, Justin Hsu, Tetsuya Sato, Pierre-Yves Strub
*-Liftings for Differential Privacy. CoRR (2017)
Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Deepak Garg, Pierre-Yves Strub
A relational logic for higher-order programs. Proc. ACM Program. Lang. 1 (ICFP) (2017)
Gilles Barthe, Thomas Espitau, Justin Hsu, Tetsuya Sato, Pierre-Yves Strub
*-Liftings for Differential Privacy. ICALP (2017)
Gilles Barthe, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
Coupling proofs are probabilistic product programs. POPL (2017)
Gilles Barthe, François Dupressoir, Sebastian Faust, Benjamin Grégoire, François-Xavier Standaert, Pierre-Yves Strub
Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model. EUROCRYPT (1) (2017)
Benjamin Beurdouche, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, Jean Karim Zinzindohoue
A messy state of the union: taming the composite state machines of TLS. Commun. ACM 60 (2) (2017)
Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
Proving Differential Privacy via Probabilistic Couplings. LICS (2016)
Gilles Barthe, François Dupressoir, Sebastian Faust, Benjamin Grégoire, François-Xavier Standaert, Pierre-Yves Strub
Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model. IACR Cryptol. ePrint Arch. 2016 (2016)
Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, Pierre-Yves Strub
Computer-Aided Verification for Mechanism Design. WINE (2016)
Gilles Barthe, Noémie Fong, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
Advanced Probabilistic Couplings for Differential Privacy. CCS (2016)
Sophie Bernard, Yves Bertot, Laurence Rideau, Pierre-Yves Strub
Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials. CPP (2016)
Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
A program logic for union bounds. CoRR (2016)
Nikhil Swamy, Catalin Hritcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean Karim Zinzindohoue, Santiago Zanella Béguelin
Dependent types and multi-monadic effects in F. POPL (2016)
Gilles Barthe, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
Coupling proofs are probabilistic product programs. CoRR (2016)
Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
Proving Differential Privacy via Probabilistic Couplings. CoRR (2016)
Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Pierre-Yves Strub, Rébecca Zucchini
Strong Non-Interference and Type-Directed Higher-Order Masking. CCS (2016)
Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
Advanced Probabilistic Couplings for Differential Privacy. CoRR (2016)
Gilles Barthe, Gian Pietro Farina, Marco Gaboardi, Emilio Jesús Gallego Arias, Andy Gordon, Justin Hsu, Pierre-Yves Strub
Differentially Private Bayesian Programming. CoRR (2016)
Gilles Barthe, Marco Gaboardi, Benjamin Grégoire, Justin Hsu, Pierre-Yves Strub
A Program Logic for Union Bounds. ICALP (2016)
Gilles Barthe, Gian Pietro Farina, Marco Gaboardi, Emilio Jesús Gallego Arias, Andy Gordon, Justin Hsu, Pierre-Yves Strub
Differentially Private Bayesian Programming. CCS (2016)
Sophie Bernard, Yves Bertot, Laurence Rideau, Pierre-Yves Strub
Formal Proofs of Transcendence for e and $π$ as an Application of Multivariate and Symmetric Polynomials. CoRR (2015)
Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, Pierre-Yves Strub
Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy. POPL (2015)
Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Léo Stefanesco, Pierre-Yves Strub
Relational Reasoning via Probabilistic Coupling. LPAR (2015)
Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, Pierre-Yves Strub
Computer-aided verification in mechanism design. CoRR (2015)
Gilles Barthe, Thomas Espitau, Benjamin Grégoire, Justin Hsu, Léo Stefanesco, Pierre-Yves Strub
Relational reasoning via probabilistic coupling. CoRR (2015)
Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Pierre-Yves Strub
Verified Proofs of Higher-Order Masking. IACR Cryptol. ePrint Arch. 2015 (2015)
Benjamin Beurdouche, Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, Jean Karim Zinzindohoue
A Messy State of the Union: Taming the Composite State Machines of TLS. IEEE Symposium on Security and Privacy (2015)
Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Pierre-Yves Strub
Verified Proofs of Higher-Order Masking. EUROCRYPT (1) (2015)
Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, Santiago Zanella Béguelin
Proving the TLS Handshake Secure (As It Is). CRYPTO (2) (2014)
Evmorfia-Iro Bartzia, Pierre-Yves Strub
A Formal Library for Elliptic Curves in the Coq Proof Assistant. ITP (2014)
Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, Santiago Zanella Béguelin
Proving the TLS Handshake Secure (as it is). IACR Cryptol. ePrint Arch. 2014 (2014)
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Guillaume Davy, François Dupressoir, Benjamin Grégoire, Pierre-Yves Strub
Verified Implementations for Secure and Verifiable Computation. IACR Cryptol. ePrint Arch. 2014 (2014)
Joseph A. Akinyele, Gilles Barthe, Benjamin Grégoire, Benedikt Schmidt, Pierre-Yves Strub
Certified Synthesis of Efficient Batch Verifiers. CSF (2014)
Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, César Kunz, Pierre-Yves Strub
Proving differential privacy in Hoare logic. CoRR (2014)
Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, César Kunz, Pierre-Yves Strub
Proving Differential Privacy in Hoare Logic. CSF (2014)
Gilles Barthe, Cédric Fournet, Benjamin Grégoire, Pierre-Yves Strub, Nikhil Swamy, Santiago Zanella Béguelin
Probabilistic relational verification for cryptographic implementations. POPL (2014)
Gilles Barthe, Marco Gaboardi, Emilio Jesús Gallego Arias, Justin Hsu, Aaron Roth, Pierre-Yves Strub
Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy. CoRR (2014)
Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Alfredo Pironti, Pierre-Yves Strub
Triple Handshakes and Cookie Cutters: Breaking and Fixing Authentication over TLS. IEEE Symposium on Security and Privacy (2014)
Nikhil Swamy, Cédric Fournet, Aseem Rastogi, Karthikeyan Bhargavan, Juan Chen, Pierre-Yves Strub, Gavin M. Bierman
Gradual typing embedded securely in JavaScript. POPL (2014)
Karthikeyan Bhargavan, Cédric Fournet, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub
Implementing TLS with Verified Cryptographic Security. IEEE Symposium on Security and Privacy (2013)
Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, Jean Yang
Secure distributed programming with value-dependent types. J. Funct. Program. 23 (4) (2013)
Cédric Fournet, Nikhil Swamy, Juan Chen, Pierre-Évariste Dagand, Pierre-Yves Strub, Benjamin Livshits
Fully abstract compilation to JavaScript. POPL (2013)
Gilles Barthe, François Dupressoir, Benjamin Grégoire, César Kunz, Benedikt Schmidt, Pierre-Yves Strub
EasyCrypt: A Tutorial. FOSAD (2013)
Pierre-Yves Strub, Nikhil Swamy, Cédric Fournet, Juan Chen
Self-certification: bootstrapping certified typecheckers in F* with Coq. POPL (2012)
Nikhil Swamy, Juan Chen, Cédric Fournet, Pierre-Yves Strub, Karthikeyan Bhargavan, Jean Yang
Secure distributed programming with value-dependent types. ICFP (2011)
Cédric Fournet, Markulf Kohlweiss, Pierre-Yves Strub
Modular code-based cryptographic verification. CCS (2011)
Bruno Barras, Jean-Pierre Jouannaud, Pierre-Yves Strub, Qian Wang
CoQMTU: A Higher-Order Type Theory with a Predicative Hierarchy of Universes Parametrized by a Decidable First-Order Theory. LICS (2011)
Pierre-Yves Strub
Coq Modulo Theory. CSL (2010)
Frédéric Blanqui, Jean-Pierre Jouannaud, Pierre-Yves Strub
From formal proofs to mathematical proofs: a safe, incremental way for building in first-order decision procedures CoRR (2008)
Frédéric Blanqui, Jean-Pierre Jouannaud, Pierre-Yves Strub
From Formal Proofs to Mathematical Proofs: A Safe, Incremental Way for Building in First-order Decision Procedures. IFIP TCS (2008)
Frédéric Blanqui, Jean-Pierre Jouannaud, Pierre-Yves Strub
Building Decision Procedures in the Calculus of Inductive Constructions CoRR (2007)

Pierre-Yves Strub.css-eqlu8i{font-size:small;padding-left:4px;}

Publication Activity (10 Years)

Top Topics

Top Venues

Pierre-Yves Strub