François Dupressoir

54 papers A* 8A 9Journal 26Unranked 10
YearRankTypeTitle / Venue / Authors
2026 J jnl
Completing the Chain: Verified Implementations of Hash-Based Signatures and Their Security.
IACR Cryptol. ePrint Arch.
Manuel Barbosa, François Dupressoir, Rui Fernandes, Andreas Hülsing, Matthias Meijers, Pierre-Yves Strub
2025 J jnl
How Hard Can It Be to Formalize a Proof? Lessons from Formalizing CryptoBox Three Times in EasyCrypt.
IACR Cryptol. ePrint Arch.
François Dupressoir, Andreas Hülsing, Cameron Low, Matthias Meijers, Charlotte Mylog, Sabine Oechsner
2025 — conf
How Hard can it be to Formalize a Proof? - Lessons from Formalizing CryptoBox Three Times in EasyCrypt.
ASIACRYPT (2)
François Dupressoir, Andreas Hülsing, Cameron Low, Matthias Meijers, Charlotte Mylog, Sabine Oechsner
2025 — conf
Work in Progress: Secure Deletion on Cloud - a Constant Battle.
EuroS&P (Workshops)
Konstantina Fotari, François Dupressoir, Kopo Marvin Ramokapane
2024 J jnl
A Tight Security Proof for $\mathrm{SPHINCS^{+}}$, Formally Verified.
IACR Cryptol. ePrint Arch.
Manuel Barbosa, François Dupressoir, Andreas Hülsing, Matthias Meijers, Pierre-Yves Strub
2024 — conf
A Tight Security Proof for SPHINCS
ASIACRYPT (4)
Manuel Barbosa, François Dupressoir, Andreas Hülsing, Matthias Meijers, Pierre-Yves Strub
2024 — conf
Formally Verifying Kyber - Episode V: Machine-Checked IND-CCA Security and Correctness of ML-KEM in EasyCrypt.
CRYPTO (2)
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
2024 J jnl
Formally verifying Kyber Episode V: Machine-checked IND-CCA security and correctness of ML-KEM in EasyCrypt.
IACR Cryptol. ePrint Arch.
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
2024 J jnl
Towards End-to-End Verifiable Online Voting: Adding Verifiability to Established Voting Systems.
IEEE Trans. Dependable Secur. Comput.
Mohammed Alsadi, Matthew Casey, Constantin Catalin Dragan, François Dupressoir, Luke Riley, Muntadher Sallal, Steve Schneider, Helen Treharne, Joe Wadsworth, Phil Wright
2023 — conf
Machine-Checked Proofs of Accountability: How to sElect Who is to Blame.
ESORICS (3)
Constantin Catalin Dragan, François Dupressoir, Kristian Gjøsteen, Thomas Haines, Peter B. Rønne, Morten Rotvold Solberg
2023 J jnl
Machine-Checked Security for $\mathrm{XMSS}$ as in RFC 8391 and $\mathrm{SPHINCS}^{+}$.
IACR Cryptol. ePrint Arch.
Manuel Barbosa, François Dupressoir, Benjamin Grégoire, Andreas Hülsing, Matthias Meijers, Pierre-Yves Strub
2023 — conf
Machine-Checked Security for rmXMSS as in RFC 8391 and $\mathrm {SPHINCS^{+}} $.
CRYPTO (5)
Manuel Barbosa, François Dupressoir, Benjamin Grégoire, Andreas Hülsing, Matthias Meijers, Pierre-Yves Strub
2023 J jnl
Machine-checked proofs of privacy against malicious boards for Selene & Co.
J. Comput. Secur.
Constantin Catalin Dragan, François Dupressoir, Ehsan Estaji, Kristian Gjøsteen, Thomas Haines, Peter Y. A. Ryan, Peter B. Rønne, Morten Rotvold Solberg
2022 A conf
Bringing State-Separating Proofs to EasyCrypt A Security Proof for Cryptobox.
CSF
François Dupressoir, Konrad Kohbrok, Sabine Oechsner
2022 A conf
Machine-Checked Proofs of Privacy Against Malicious Boards for Selene & Co.
CSF
Constantin Catalin Dragan, François Dupressoir, Ehsan Estaji, Kristian Gjøsteen, Thomas Haines, Peter Y. A. Ryan, Peter B. Rønne, Morten Rotvold Solberg
2022 J jnl
Machine-Checked Proofs of Privacy Against Malicious Boards for Selene & Co.
IACR Cryptol. ePrint Arch.
Constantin Catalin Dragan, François Dupressoir, Ehsan Estaji, Kristian Gjøsteen, Thomas Haines, Peter Y. A. Ryan, Peter B. Rønne, Morten Rotvold Solberg
2021 J jnl
Bringing State-Separating Proofs to EasyCrypt - A Security Proof for Cryptobox.
IACR Cryptol. ePrint Arch.
François Dupressoir, Konrad Kohbrok, Sabine Oechsner
2021 A conf
Machine-Checking Unforgeability Proofs for Signature Schemes with Tight Reductions to the Computational Diffie-Hellman Problem.
CSF
François Dupressoir, Sara Zain
2021 A conf
Mechanised Models and Proofs for Distance-Bounding.
CSF
Ioana Boureanu, Constantin Catalin Dragan, François Dupressoir, David Gérault, Pascal Lafourcade
2020 A conf
Augmenting an Internet Voting System with Selene Verifiability using Permissioned Distributed Ledger.
ICDCS
Muntadher Sallal, Steve Schneider, Matthew Casey, François Dupressoir, Helen Treharne, Constantin Catalin Dragan, Luke Riley, Phil Wright
2020 J jnl
Improved parallel mask refreshing algorithms: generic solutions with parametrized non-interference and automated optimizations.
J. Cryptogr. Eng.
Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, François-Xavier Standaert, Pierre-Yves Strub
2020 J jnl
Precise and Mechanised Models and Proofs for Distance-Bounding and an Application to Contactless Payments.
IACR Cryptol. ePrint Arch.
Ioana Boureanu, Constantin Catalin Dragan, François Dupressoir, David Gérault, Pascal Lafourcade
2019 J jnl
Machine-Checked Proofs for Cryptographic Standards.
IACR Cryptol. ePrint Arch.
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
2019 A* conf
Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3.
CCS
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
2019 J jnl
VMV: Augmenting an Internet Voting System with Selene Verifiability.
CoRR
Muntadher Sallal, Steve A. Schneider, Matthew Casey, Constantin Catalin Dragan, François Dupressoir, Luke Riley, Helen Treharne, Joe Wadsworth, Phil Wright
2018 A conf
Formal Security Proof of CMAC and Its Variants.
CSF
Cécile Baritel-Ruet, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire
2018 J jnl
Improved Parallel Mask Refreshing Algorithms: Generic Solutions with Parametrized Non-Interference & Automated Optimizations.
IACR Cryptol. ePrint Arch.
Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, François-Xavier Standaert, Pierre-Yves Strub
2018 A conf
Machine-Checked Proofs for Electronic Voting: Privacy and Verifiability for Belenios.
CSF
Véronique Cortier, Constantin Catalin Dragan, François Dupressoir, Bogdan Warinschi
2017 A* conf
A Fast and Verified Software Stack for Secure Function Evaluation.
CCS
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Vitor Pereira
2017 J jnl
A Fast and Verified Software Stack for Secure Function Evaluation.
IACR Cryptol. ePrint Arch.
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Vitor Pereira
2017 J jnl
A Note on 'Further Improving Efficiency of Higher-Order Masking Scheme by Decreasing Randomness Complexity'.
IACR Cryptol. ePrint Arch.
Gilles Barthe, François Dupressoir, Benjamin Grégoire
2017 A* conf
Machine-Checked Proofs of Privacy for Electronic Voting Protocols.
IEEE Symposium on Security and Privacy
Véronique Cortier, Constantin Catalin Dragan, François Dupressoir, Benedikt Schmidt, Pierre-Yves Strub, Bogdan Warinschi
2017 — conf
Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model.
EUROCRYPT (1)
Gilles Barthe, François Dupressoir, Sebastian Faust, Benjamin Grégoire, François-Xavier Standaert, Pierre-Yves Strub
2016 J jnl
Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model.
IACR Cryptol. ePrint Arch.
Gilles Barthe, François Dupressoir, Sebastian Faust, Benjamin Grégoire, François-Xavier Standaert, Pierre-Yves Strub
2016 A* conf
Strong Non-Interference and Type-Directed Higher-Order Masking.
CCS
Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Pierre-Yves Strub, Rébecca Zucchini
2016 A* conf
Verifiable Side-Channel Security of Cryptographic Implementations: Constant-Time MEE-CBC.
FSE
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir
2016 A* conf
Verifying Constant-Time Implementations.
USENIX Security Symposium
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, Michael Emmi
2015 J jnl
Compositional Verification of Higher-Order Masking: Application to a Verifying Masking Compiler.
IACR Cryptol. ePrint Arch.
Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire
2015 J jnl
Verifiable side-channel security of cryptographic implementations: constant-time MEE-CBC.
IACR Cryptol. ePrint Arch.
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir
2015 — conf
Verified Proofs of Higher-Order Masking.
EUROCRYPT (1)
Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Pierre-Yves Strub
2015 J jnl
Verified Proofs of Higher-Order Masking.
IACR Cryptol. ePrint Arch.
Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Pierre-Yves Strub
2014 J jnl
Guiding a general-purpose C verifier to prove cryptographic protocols.
J. Comput. Secur.
François Dupressoir, Andrew D. Gordon, Jan Jürjens, David A. Naumann
2014 J jnl
Making RSA-PSS Provably Secure Against Non-Random Faults.
IACR Cryptol. ePrint Arch.
Gilles Barthe, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Mehdi Tibouchi, Jean-Christophe Zapalowicz
2014 A conf
Making RSA-PSS Provably Secure against Non-random Faults.
CHES
Gilles Barthe, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Mehdi Tibouchi, Jean-Christophe Zapalowicz
2014 A* conf
Synthesis of Fault Attacks on Cryptographic Implementations.
CCS
Gilles Barthe, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Jean-Christophe Zapalowicz
2014 J jnl
Synthesis of Fault Attacks on Cryptographic Implementations.
IACR Cryptol. ePrint Arch.
Gilles Barthe, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Jean-Christophe Zapalowicz
2014 J jnl
Verified Implementations for Secure and Verifiable Computation.
IACR Cryptol. ePrint Arch.
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Guillaume Davy, François Dupressoir, Benjamin Grégoire, Pierre-Yves Strub
2013 A* conf
Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations.
CCS
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir
2013 J jnl
Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations.
IACR Cryptol. ePrint Arch.
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir
2013 — conf
EasyCrypt: A Tutorial.
FOSAD
Gilles Barthe, François Dupressoir, Benjamin Grégoire, César Kunz, Benedikt Schmidt, Pierre-Yves Strub
2013 J jnl
Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols.
CoRR
François Dupressoir, Andrew D. Gordon, Jan Jürjens, David A. Naumann
2013 — —
Proving cryptographic C programs secure with general-purpose verification tools.
François Dupressoir
2011 A conf
Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols.
CSF
François Dupressoir, Andrew D. Gordon, Jan Jürjens, David A. Naumann
2011 — conf
Verifying Cryptographic Code in C: Some Experience and the Csec Challenge.
Formal Aspects in Security and Trust
Mihhail Aizatulin, François Dupressoir, Andrew D. Gordon, Jan Jürjens