Verifying Cryptographic Code in C: Some Experience and the Csec Challenge. - Mihhail Aizatulin; François Dupressoir; Andrew D. Gordon 001; Jan Jürjens (Formal Aspects in Security and Trust, 2011)

EasyCrypt: A Tutorial. - Gilles Barthe; François Dupressoir; Benjamin Grégoire; César Kunz; Benedikt Schmidt; Pierre-Yves Strub (FOSAD, 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)

Proving cryptographic C programs secure with general-purpose verification tools. - François Dupressoir (2013)

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

Guiding a general-purpose C verifier to prove cryptographic protocols. - François Dupressoir; Andrew D. Gordon 001; Jan Jürjens; David A. Naumann (J. Comput. Secur., 2014)

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)

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

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 (CCS, 2016)

Verifying Constant-Time Implementations. - José Bacelar Almeida; Manuel Barbosa; Gilles Barthe; François Dupressoir; Michael Emmi (USENIX Security Symposium, 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)

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 (IEEE Symposium on Security and Privacy, 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 002 (IACR Cryptol. ePrint Arch., 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)

Formal Security Proof of CMAC and Its Variants. - Cécile Baritel-Ruet; François Dupressoir; Pierre-Alain Fouque; Benjamin Grégoire (CSF, 2018)

Machine-Checked Proofs for Electronic Voting: Privacy and Verifiability for Belenios. - Véronique Cortier; Constantin Catalin Dragan; François Dupressoir; Bogdan Warinschi (CSF, 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 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 004; Alley Stoughton; Pierre-Yves Strub (CCS, 2019)

VMV: Augmenting an Internet Voting System with Selene Verifiability. - Muntadher Sallal; Steve A. Schneider; Matthew Casey 001; Constantin Catalin Dragan; François Dupressoir; Luke Riley; Helen Treharne; Joe Wadsworth; Phil Wright (CoRR, 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 004; Alley Stoughton; Pierre-Yves Strub (IACR Cryptol. ePrint Arch., 2019)

Augmenting an Internet Voting System with Selene Verifiability using Permissioned Distributed Ledger. - Muntadher Sallal; Steve Schneider; Matthew Casey 001; François Dupressoir; Helen Treharne; Constantin Catalin Dragan; Luke Riley; Phil Wright (ICDCS, 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 001 (IACR Cryptol. ePrint Arch., 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)

Mechanised Models and Proofs for Distance-Bounding. - Ioana Boureanu; Constantin Catalin Dragan; François Dupressoir; David Gérault; Pascal Lafourcade 001 (CSF, 2021)

Machine-Checking Unforgeability Proofs for Signature Schemes with Tight Reductions to the Computational Diffie-Hellman Problem. - François Dupressoir; Sara Zain (CSF, 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-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 (CRYPTO (5), 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 (ESORICS (3), 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 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)

A Tight Security Proof for SPHINCS+, Formally Verified. - Manuel Barbosa; François Dupressoir; Andreas Hülsing; Matthias Meijers; Pierre-Yves Strub (ASIACRYPT (4), 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 004; Hugo Pacheco 001; Miguel Quaresma; et al. (IACR Cryptol. ePrint Arch., 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)

Towards End-to-End Verifiable Online Voting: Adding Verifiability to Established Voting Systems. - Mohammed Alsadi 001; Matthew Casey 001; Constantin Catalin Dragan; François Dupressoir; Luke Riley; Muntadher Sallal; Steve Schneider; Helen Treharne; Joe Wadsworth; Phil Wright (IEEE Trans. Dependable Secur. Comput., 2024)

Work in Progress: Secure Deletion on Cloud - a Constant Battle. - Konstantina Fotari; François Dupressoir; Kopo Marvin Ramokapane (EuroS&P (Workshops), 2025)