François Dupressoir

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

Collaborative distances:

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

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

IACR Cryptol. ePrint Arch., 2024

2023

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

J. Comput. Secur., 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

2021

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

François Dupressoir, Konrad Kohbrok, Sabine Oechsner

IACR Cryptol. ePrint Arch., 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

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

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

2016

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

IACR Cryptol. ePrint Arch., 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

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

Verified Proofs of Higher-Order Masking.

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

IACR Cryptol. ePrint Arch., 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

Verifiable side-channel security of cryptographic implementations: constant-time MEE-CBC.

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

IACR Cryptol. ePrint Arch., 2015

2014

Guiding a general-purpose C verifier to prove cryptographic protocols.

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

J. Comput. Secur., 2014

Synthesis of Fault Attacks on Cryptographic Implementations.

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

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

IACR Cryptol. ePrint Arch., 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

2013

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

François Dupressoir

PhD thesis, 2013

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

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

IACR Cryptol. ePrint Arch., 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

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