François Dupressoir

According to our database, François Dupressoir authored at least 39 papers between 2011 and 2025.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of three.

2025

How Hard Can It Be to Formalize a Proof? Lessons from Formalizing CryptoBox Three Times in EasyCrypt.

François Dupressoir, Andreas Hülsing, Cameron Low, Matthias Meijers, Charlotte Mylog, Sabine Oechsner

IACR Cryptol. ePrint Arch., 2025

Work in Progress: Secure Deletion on Cloud - a Constant Battle.

Konstantina Fotari, François Dupressoir, Kopo Marvin Ramokapane

Proceedings of the IEEE European Symposium on Security and Privacy, 2025

2024

Towards End-to-End Verifiable Online Voting: Adding Verifiability to Established Voting Systems.

Mohammed Alsadi, Matthew Casey, Constantin Catalin Dragan, François Dupressoir, Luke Riley, Muntadher Sallal, Steve Schneider, Helen Treharne, Joe Wadsworth, Phil Wright

IEEE Trans. Dependable Secur. Comput., 2024

A Tight Security Proof for $\mathrm{SPHINCS^{+}}$, Formally Verified.

Manuel Barbosa, François Dupressoir, Andreas Hülsing, Matthias Meijers, Pierre-Yves Strub

IACR Cryptol. ePrint Arch., 2024

Formally Verifying Kyber - Episode V: Machine-Checked IND-CCA Security and Correctness of ML-KEM in EasyCrypt.

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

Proceedings of the Advances in Cryptology - CRYPTO 2024, 2024

A Tight Security Proof for SPHINCS⁺, Formally Verified.

Manuel Barbosa, François Dupressoir, Andreas Hülsing, Matthias Meijers, Pierre-Yves Strub

Proceedings of the Advances in Cryptology - ASIACRYPT 2024, 2024

2023

Machine-Checked Security for $\mathrm{XMSS}$ as in RFC 8391 and $\mathrm{SPHINCS}^{+}$.

Manuel Barbosa, François Dupressoir, Benjamin Grégoire, Andreas Hülsing, Matthias Meijers, Pierre-Yves Strub

IACR Cryptol. ePrint Arch., 2023

Machine-Checked Proofs of Accountability: How to sElect Who is to Blame.

Constantin Catalin Dragan, François Dupressoir, Kristian Gjøsteen, Thomas Haines, Peter B. Rønne, Morten Rotvold Solberg

Proceedings of the Computer Security - ESORICS 2023, 2023

Machine-Checked Security for rmXMSS as in RFC 8391 and $\mathrm {SPHINCS^{+}} $.

Manuel Barbosa, François Dupressoir, Benjamin Grégoire, Andreas Hülsing, Matthias Meijers, Pierre-Yves Strub

Proceedings of the Advances in Cryptology - CRYPTO 2023, 2023

2022

Bringing State-Separating Proofs to EasyCrypt A Security Proof for Cryptobox.

François Dupressoir, Konrad Kohbrok, Sabine Oechsner

Proceedings of the 35th IEEE Computer Security Foundations Symposium, 2022

Machine-Checked Proofs of Privacy Against Malicious Boards for Selene & Co.

Constantin Catalin Dragan, François Dupressoir, Ehsan Estaji, Kristian Gjøsteen, Thomas Haines, Peter Y. A. Ryan, Peter B. Rønne, Morten Rotvold Solberg

Proceedings of the 35th IEEE Computer Security Foundations Symposium, 2022

2021

Machine-Checking Unforgeability Proofs for Signature Schemes with Tight Reductions to the Computational Diffie-Hellman Problem.

François Dupressoir, Sara Zain

Proceedings of the 34th IEEE Computer Security Foundations Symposium, 2021

Mechanised Models and Proofs for Distance-Bounding.

Ioana Boureanu, Constantin Catalin Dragan, François Dupressoir, David Gérault, Pascal Lafourcade

Proceedings of the 34th IEEE Computer Security Foundations Symposium, 2021

2020

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

Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, François-Xavier Standaert, Pierre-Yves Strub

J. Cryptogr. Eng., 2020

Precise and Mechanised Models and Proofs for Distance-Bounding and an Application to Contactless Payments.

Ioana Boureanu, Constantin Catalin Dragan, François Dupressoir, David Gérault, Pascal Lafourcade

IACR Cryptol. ePrint Arch., 2020

Augmenting an Internet Voting System with Selene Verifiability using Permissioned Distributed Ledger.

Muntadher Sallal, Steve Schneider, Matthew Casey, François Dupressoir, Helen Treharne, Constantin Catalin Dragan, Luke Riley, Phil Wright

Proceedings of the 40th IEEE International Conference on Distributed Computing Systems, 2020

2019

Machine-Checked Proofs for Cryptographic Standards.

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

IACR Cryptol. ePrint Arch., 2019

VMV: Augmenting an Internet Voting System with Selene Verifiability.

Muntadher Sallal, Steve A. Schneider, Matthew Casey, Constantin Catalin Dragan, François Dupressoir, Luke Riley, Helen Treharne, Joe Wadsworth, Phil Wright

CoRR, 2019

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

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

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

2018

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

Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, François-Xavier Standaert, Pierre-Yves Strub

IACR Cryptol. ePrint Arch., 2018

Machine-Checked Proofs for Electronic Voting: Privacy and Verifiability for Belenios.

Véronique Cortier, Constantin Catalin Dragan, François Dupressoir, Bogdan Warinschi

Proceedings of the 31st IEEE Computer Security Foundations Symposium, 2018

Formal Security Proof of CMAC and Its Variants.

Cécile Baritel-Ruet, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire

Proceedings of the 31st IEEE Computer Security Foundations Symposium, 2018

2017

A Note on 'Further Improving Efficiency of Higher-Order Masking Scheme by Decreasing Randomness Complexity'.

Gilles Barthe, François Dupressoir, Benjamin Grégoire

IACR Cryptol. ePrint Arch., 2017

Machine-Checked Proofs of Privacy for Electronic Voting Protocols.

Véronique Cortier, Constantin Catalin Dragan, François Dupressoir, Benedikt Schmidt, Pierre-Yves Strub, Bogdan Warinschi

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

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

Gilles Barthe, François Dupressoir, Sebastian Faust, Benjamin Grégoire, François-Xavier Standaert, Pierre-Yves Strub

Proceedings of the Advances in Cryptology - EUROCRYPT 2017 - 36th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Paris, France, April 30, 2017

A Fast and Verified Software Stack for Secure Function Evaluation.

José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Vitor Pereira

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

2016

Verifying Constant-Time Implementations.

José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, Michael Emmi

Proceedings of the 25th USENIX Security Symposium, 2016

Verifiable Side-Channel Security of Cryptographic Implementations: Constant-Time MEE-CBC.

José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir

Proceedings of the Fast Software Encryption - 23rd International Conference, 2016

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

Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Pierre-Yves Strub, Rébecca Zucchini

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

2015

Compositional Verification of Higher-Order Masking: Application to a Verifying Masking Compiler.

Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire

IACR Cryptol. ePrint Arch., 2015

Verified Proofs of Higher-Order Masking.

Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Pierre-Yves Strub

Proceedings of the Advances in Cryptology - EUROCRYPT 2015, 2015

2014

Verified Implementations for Secure and Verifiable Computation.

José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Guillaume Davy, François Dupressoir, Benjamin Grégoire, Pierre-Yves Strub

IACR Cryptol. ePrint Arch., 2014

Making RSA-PSS Provably Secure against Non-random Faults.

Gilles Barthe, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Mehdi Tibouchi, Jean-Christophe Zapalowicz

Proceedings of the Cryptographic Hardware and Embedded Systems - CHES 2014, 2014

Synthesis of Fault Attacks on Cryptographic Implementations.

Gilles Barthe, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Jean-Christophe Zapalowicz

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

2013

Proving cryptographic C programs secure with general-purpose verification tools.

François Dupressoir

PhD thesis, 2013

EasyCrypt: A Tutorial.

Gilles Barthe, François Dupressoir, Benjamin Grégoire, César Kunz, Benedikt Schmidt, Pierre-Yves Strub

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

Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations.

José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir

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

2011

Verifying Cryptographic Code in C: Some Experience and the Csec Challenge.

Mihhail Aizatulin, François Dupressoir, Andrew D. Gordon, Jan Jürjens

Proceedings of the Formal Aspects of Security and Trust - 8th International Workshop, 2011

Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols.

François Dupressoir, Andrew D. Gordon, Jan Jürjens, David A. Naumann

Proceedings of the 24th IEEE Computer Security Foundations Symposium, 2011