Publications

This list may be slightly out of date. For an up-to-date list and bibliometric information, please visit the links in the side menu.

2022

  1. Bringing State-Separating Proofs to EasyCrypt-A Security Proof for Cryptobox
    François DupressoirKonrad Kohbrok, and Sabine Oechsner
    In 35th IEEE Computer Security Foundations Symposium 2022
  2. Machine-checked proofs of privacy against malicious boards for Selene & Co
    In 35th IEEE Computer Security Foundations Symposium 2022

2021

  1. Bringing State-Separating Proofs to EasyCrypt - A Security Proof for Cryptobox
    François DupressoirKonrad Kohbrok, and Sabine Oechsner
    IACR Cryptol. ePrint Arch. 2021
  2. Mechanised Models and Proofs for Distance-Bounding
    In 34th IEEE Computer Security Foundations Symposium, CSF 2021, Dubrovnik, Croatia, June 21-25, 2021 2021
  3. Machine-Checking Unforgeability Proofs for Signature Schemes with Tight Reductions to the Computational Diffie-Hellman Problem
    François Dupressoir, and Sara Zain
    In 34th IEEE Computer Security Foundations Symposium, CSF 2021, Dubrovnik, Croatia, June 21-25, 2021 2021

2020

  1. Precise and Mechanised Models and Proofs for Distance-Bounding and an Application to Contactless Payments
    IACR Cryptol. ePrint Arch. 2020
  2. Improved parallel mask refreshing algorithms: generic solutions with parametrized non-interference and automated optimizations
    J. Cryptogr. Eng. 2020
  3. Augmenting an Internet Voting System with Selene Verifiability using Permissioned Distributed Ledger
    Muntadher SallalSteve Schneider, Matthew Casey,  François DupressoirHelen TreharneConstantin Cătălin Drăgan, Luke Riley, and Phil Wright
    In 40th IEEE International Conference on Distributed Computing Systems, ICDCS 2020, Singapore, November 29 - December 1, 2020 2020

2019

  1. VMV: Augmenting an Internet Voting System with Selene Verifiability
    Muntadher SallalSteve A. Schneider, Matthew Casey, Constantin Cătălin DrăganFrançois Dupressoir, Luke Riley, Helen Treharne, Joe Wadsworth, and Phil Wright
    CoRR 2019
  2. Machine-Checked Proofs for Cryptographic Standards
    IACR Cryptol. ePrint Arch. 2019
  3. Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3
    In Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, CCS 2019, London, UK, November 11-15, 2019 2019

2018

  1. Improved Parallel Mask Refreshing Algorithms: Generic Solutions with Parametrized Non-Interference & Automated Optimizations
    IACR Cryptol. ePrint Arch. 2018
  2. Formal Security Proof of CMAC and Its Variants
    In 31st IEEE Computer Security Foundations Symposium, CSF 2018, Oxford, United Kingdom, July 9-12, 2018 2018
  3. Machine-Checked Proofs for Electronic Voting: Privacy and Verifiability for Belenios
    In 31st IEEE Computer Security Foundations Symposium, CSF 2018, Oxford, United Kingdom, July 9-12, 2018 2018

2017

  1. A Fast and Verified Software Stack for Secure Function Evaluation
    IACR Cryptol. ePrint Arch. 2017
  2. A Note on ’Further Improving Efficiency of Higher-Order Masking Scheme by Decreasing Randomness Complexity’
    Gilles BartheFrançois Dupressoir, and Benjamin Grégoire
    IACR Cryptol. ePrint Arch. 2017
  3. A Fast and Verified Software Stack for Secure Function Evaluation
    In Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, TX, USA, October 30 - November 03, 2017 2017
  4. Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model
    In Advances in Cryptology - EUROCRYPT 2017 - 36th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Paris, France, April 30 - May 4, 2017, Proceedings, Part I 2017
  5. Machine-Checked Proofs of Privacy for Electronic Voting Protocols
    In 2017 IEEE Symposium on Security and Privacy, SP 2017, San Jose, CA, USA, May 22-26, 2017 2017

2016

  1. Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model
    IACR Cryptol. ePrint Arch. 2016
  2. Strong Non-Interference and Type-Directed Higher-Order Masking
    Gilles BartheSonia BelaïdFrançois DupressoirPierre-Alain FouqueBenjamin GrégoirePierre-Yves Strub, and Rébecca Zucchini
    In Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, Vienna, Austria, October 24-28, 2016 2016
  3. Verifiable Side-Channel Security of Cryptographic Implementations: Constant-Time MEE-CBC
    José Bacelar AlmeidaManuel BarbosaGilles Barthe, and François Dupressoir
    In Fast Software Encryption - 23rd International Conference, FSE 2016, Bochum, Germany, March 20-23, 2016, Revised Selected Papers 2016
  4. Verifying Constant-Time Implementations
    In 25th USENIX Security Symposium, USENIX Security 16, Austin, TX, USA, August 10-12, 2016 2016

2015

  1. Verified Proofs of Higher-Order Masking
    IACR Cryptol. ePrint Arch. 2015
  2. Compositional Verification of Higher-Order Masking: Application to a Verifying Masking Compiler
    IACR Cryptol. ePrint Arch. 2015
  3. Verifiable side-channel security of cryptographic implementations: constant-time MEE-CBC
    José Bacelar AlmeidaManuel BarbosaGilles Barthe, and François Dupressoir
    IACR Cryptol. ePrint Arch. 2015
  4. Verified Proofs of Higher-Order Masking
    In Advances in Cryptology - EUROCRYPT 2015 - 34th Annual International Conference on the Theory and Applications of Cryptographic Techniques, Sofia, Bulgaria, April 26-30, 2015, Proceedings, Part I 2015

2014

  1. Making RSA-PSS Provably Secure Against Non-Random Faults
    IACR Cryptol. ePrint Arch. 2014
  2. Synthesis of Fault Attacks on Cryptographic Implementations
    IACR Cryptol. ePrint Arch. 2014
  3. Verified Implementations for Secure and Verifiable Computation
    José Bacelar AlmeidaManuel BarbosaGilles Barthe, Guillaume Davy,  François DupressoirBenjamin Grégoire, and Pierre-Yves Strub
    IACR Cryptol. ePrint Arch. 2014
  4. Guiding a general-purpose C verifier to prove cryptographic protocols
    François DupressoirAndrew D. GordonJan Jürjens, and David A. Naumann
    J. Comput. Secur. 2014
  5. Synthesis of Fault Attacks on Cryptographic Implementations
    In Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, Scottsdale, AZ, USA, November 3-7, 2014 2014
  6. Making RSA-PSS Provably Secure against Non-random Faults
    In Cryptographic Hardware and Embedded Systems - CHES 2014 - 16th International Workshop, Busan, South Korea, September 23-26, 2014. Proceedings 2014

2013

  1. Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols
    François DupressoirAndrew D. GordonJan Jürjens, and David A. Naumann
    CoRR 2013
  2. Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations
    José Bacelar AlmeidaManuel BarbosaGilles Barthe, and François Dupressoir
    IACR Cryptol. ePrint Arch. 2013
  3. Proving cryptographic C programs secure with general-purpose verification tools
    François Dupressoir
    IACR Cryptol. ePrint Arch. 2013
  4. Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations
    José Bacelar AlmeidaManuel BarbosaGilles Barthe, and François Dupressoir
    In 2013 ACM SIGSAC Conference on Computer and Communications Security, CCS’13, Berlin, Germany, November 4-8, 2013 2013
  5. EasyCrypt: A Tutorial
    In Foundations of Security Analysis and Design VII - FOSAD 2012/2013 Tutorial Lectures 2013

2011

  1. Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols
    François DupressoirAndrew D. GordonJan Jürjens, and David A. Naumann
    In Proceedings of the 24th IEEE Computer Security Foundations Symposium, CSF 2011, Cernay-la-Ville, France, 27-29 June, 2011 2011
  2. Verifying Cryptographic Code in C: Some Experience and the Csec Challenge
    Mihhail Aizatulin,  François DupressoirAndrew D. Gordon, and Jan Jürjens
    In Formal Aspects of Security and Trust - 8th International Workshop, FAST 2011, Leuven, Belgium, September 12-14, 2011. Revised Selected Papers 2011