Pierre-Yves Strub

Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2023

2022

Formalizing the Face Lattice of Polyhedra.

[BibT_eX]

[DOI]

Xavier Allamigeon

Ricardo D. Katz

Log. Methods Comput. Sci., 2022

Formal Verification of Saber's Public-Key Encryption Scheme in EasyCrypt.

[BibT_eX]

[DOI]

Andreas Hülsing

Matthias Meijers

IACR Cryptol. ePrint Arch., 2022

A drag-and-drop proof tactic.

[BibT_eX]

[DOI]

Pablo Donato

François-Xavier Standaert

Benjamin Werner

Proceedings of the CPP '22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17, 2022

2021

EasyPQC: Verifying Post-Quantum Cryptography.

[BibT_eX]

[DOI]

IACR Cryptol. ePrint Arch., 2021

Unsolvability of the Quintic Formalized in Dependent Type Theory.

[BibT_eX]

[DOI]

Proceedings of the 12th International Conference on Interactive Theorem Proving, 2021

2020

Improved parallel mask refreshing algorithms: generic solutions with parametrized non-interference and automated optimizations.

[BibT_eX]

[DOI]

François-Xavier Standaert

J. Cryptogr. Eng., 2020

The Last Mile: High-Assurance and High-Speed Cryptographic Implementations.

[BibT_eX]

[DOI]

Proceedings of the 2020 IEEE Symposium on Security and Privacy, 2020

2019

Relational ⋆⋆\star-Liftings for Differential Privacy.

[BibT_eX]

[DOI]

Log. Methods Comput. Sci., 2019

A Machine-Checked Proof of Security for AWS Key Management Service.

[BibT_eX]

[DOI]

IACR Cryptol. ePrint Arch., 2019

Machine-Checked Proofs for Cryptographic Standards.

[BibT_eX]

[DOI]

IACR Cryptol. ePrint Arch., 2019

Symbolic Methods in Computational Cryptography Proofs.

[BibT_eX]

[DOI]

Proceedings of the 32nd IEEE Computer Security Foundations Symposium, 2019

Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3.

[BibT_eX]

[DOI]

Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, 2019

2018

Proving expected sensitivity of probabilistic programs.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2018

Computer-aided proofs for multiparty computation with active security.

[BibT_eX]

[DOI]

IACR Cryptol. ePrint Arch., 2018

Improved Parallel Mask Refreshing Algorithms: Generic Solutions with Parametrized Non-Interference & Automated Optimizations.

[BibT_eX]

[DOI]

IACR Cryptol. ePrint Arch., 2018

hacspec: Towards Verifiable Crypto Standards.

[BibT_eX]

[DOI]

Franziskus Kiefer

Proceedings of the Security Standardisation Research - 4th International Conference, 2018

An Assertion-Based Program Logic for Probabilistic Programs.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2018

2017

A relational logic for higher-order programs.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2017

A messy state of the union: taming the composite state machines of TLS.

[BibT_eX]

[DOI]

Benjamin Beurdouche

Constantin Catalin Dragan

Antoine Delignat-Lavaud

Jean Karim Zinzindohoue

Commun. ACM, 2017

Machine-Checked Proofs of Privacy for Electronic Voting Protocols.

[BibT_eX]

[DOI]

Véronique Cortier

Proceedings of the 2017 IEEE Symposium on Security and Privacy, 2017

Coupling proofs are probabilistic product programs.

[BibT_eX]

[DOI]

Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017

Coq without Type Casts: A Complete Proof of Coq Modulo Theory.

[BibT_eX]

[DOI]

François-Xavier Standaert

Proceedings of the LPAR-21, 2017

Proving uniformity and independence by self-composition and coupling.

[BibT_eX]

[DOI]

Proceedings of the LPAR-21, 2017

*-Liftings for Differential Privacy.

[BibT_eX]

[DOI]

Proceedings of the 44th International Colloquium on Automata, Languages, and Programming, 2017

Jasmin: High-Assurance and High-Speed Cryptography.

[BibT_eX]

[DOI]

Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, 2017

2016

Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model.

[BibT_eX]

[DOI]

IACR Cryptol. ePrint Arch., 2016

Advanced Probabilistic Couplings for Differential Privacy.

[BibT_eX]

[DOI]

CoRR, 2016

Computer-Aided Verification for Mechanism Design.

[BibT_eX]

[DOI]

Aaron Roth

Proceedings of the Web and Internet Economics - 12th International Conference, 2016

Dependent types and multi-monadic effects in F.

[BibT_eX]

[DOI]

Antoine Delignat-Lavaud

Simon Forest

Santiago Zanella Béguelin

Markulf Kohlweiss

Jean Karim Zinzindohoue

Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016

Proving Differential Privacy via Probabilistic Couplings.

[BibT_eX]

[DOI]

Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, 2016

A Program Logic for Union Bounds.

[BibT_eX]

[DOI]

Proceedings of the 43rd International Colloquium on Automata, Languages, and Programming, 2016

Formal proofs of transcendence for e and pi as an application of multivariate and symmetric polynomials.

[BibT_eX]

[DOI]

Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, 2016

Advanced Probabilistic Couplings for Differential Privacy.

[BibT_eX]

[DOI]

Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, 2016

Differentially Private Bayesian Programming.

[BibT_eX]

[DOI]

Gian Pietro Farina

Andy Gordon

Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, 2016

Strong Non-Interference and Type-Directed Higher-Order Masking.

[BibT_eX]

[DOI]

Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, 2016

2015

Verified Proofs of Higher-Order Masking.

[BibT_eX]

[DOI]

IACR Cryptol. ePrint Arch., 2015

Formal Proofs of Transcendence for e and $π$ as an Application of Multivariate and Symmetric Polynomials.

[BibT_eX]

[DOI]

CoRR, 2015

Higher-Order Approximate Relational Refinement Types for Mechanism Design and Differential Privacy.

[BibT_eX]

[DOI]

Aaron Roth

Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2015

Relational Reasoning via Probabilistic Coupling.

[BibT_eX]

[DOI]

Proceedings of the Logic for Programming, Artificial Intelligence, and Reasoning, 2015

2014

Proving the TLS Handshake Secure (as it is).

[BibT_eX]

[DOI]

Santiago Zanella Béguelin

IACR Cryptol. ePrint Arch., 2014

Verified Implementations for Secure and Verifiable Computation.

[BibT_eX]

[DOI]

IACR Cryptol. ePrint Arch., 2014

Triple Handshakes and Cookie Cutters: Breaking and Fixing Authentication over TLS.

[BibT_eX]

[DOI]

Antoine Delignat-Lavaud

Alfredo Pironti

Proceedings of the 2014 IEEE Symposium on Security and Privacy, 2014

Gradual typing embedded securely in JavaScript.

[BibT_eX]

[DOI]

Nikhil Swamy

Aseem Rastogi

Juan Chen

Santiago Zanella Béguelin

Gavin M. Bierman

Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014

Probabilistic relational verification for cryptographic implementations.

[BibT_eX]

[DOI]

Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014

A Formal Library for Elliptic Curves in the Coq Proof Assistant.

[BibT_eX]

[DOI]

Evmorfia-Iro Bartzia

Proceedings of the Interactive Theorem Proving - 5th International Conference, 2014

Proving Differential Privacy in Hoare Logic.

[BibT_eX]

[DOI]

César Kunz

Proceedings of the IEEE 27th Computer Security Foundations Symposium, 2014

Certified Synthesis of Efficient Batch Verifiers.

[BibT_eX]

[DOI]

Proceedings of the IEEE 27th Computer Security Foundations Symposium, 2014

2013

Secure distributed programming with value-dependent types.

[BibT_eX]

[DOI]

Jean Yang

J. Funct. Program., 2013

Implementing TLS with Verified Cryptographic Security.

[BibT_eX]

[DOI]

Proceedings of the 2013 IEEE Symposium on Security and Privacy, 2013

Fully abstract compilation to JavaScript.

[BibT_eX]

[DOI]

Nikhil Swamy

Juan Chen

Pierre-Évariste Dagand

Benjamin Livshits

Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2013

EasyCrypt: A Tutorial.

[BibT_eX]

[DOI]

Proceedings of the Foundations of Security Analysis and Design VII, 2013

2012

Self-certification: bootstrapping certified typecheckers in F* with Coq.

[BibT_eX]

[DOI]

Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2012

2011

CoQMTU: A Higher-Order Type Theory with a Predicative Hierarchy of Universes Parametrized by a Decidable First-Order Theory.

[BibT_eX]

[DOI]

Bruno Barras

Qian Wang

Proceedings of the 26th Annual IEEE Symposium on Logic in Computer Science, 2011

Modular code-based cryptographic verification.

[BibT_eX]

[DOI]

Markulf Kohlweiss

Proceedings of the 18th ACM Conference on Computer and Communications Security, 2011

2010

Coq Modulo Theory.

[BibT_eX]

[DOI]

Proceedings of the Computer Science Logic, 24th International Workshop, 2010

2008

Type Theory and Decision Procedures. (Théorie des Types et Procédures de Décision).

[BibT_eX]

[DOI]

PhD thesis, 2008

From Formal Proofs to Mathematical Proofs: A Safe, Incremental Way for Building in First-order Decision Procedures.

[BibT_eX]

[DOI]

Frédéric Blanqui

Proceedings of the Fifth IFIP International Conference On Theoretical Computer Science, 2008

2007

Building Decision Procedures in the Calculus of Inductive Constructions.

[BibT_eX]

[DOI]

Frédéric Blanqui

Proceedings of the Computer Science Logic, 21st International Workshop, 2007

2001

Color image segmentation based on automatic morphological clustering.

[BibT_eX]

[DOI]

Thierry Géraud