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.

2024

1. 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, and Pierre-Yves Strub

   IACR Cryptol. ePrint Arch. 2024

   HTML
2. A Tight Security Proof for SPHINCS⁺, Formally Verified

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

   IACR Cryptol. ePrint Arch. 2024

   HTML
3. 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, and Phil Wright

   IEEE Trans. Dependable Secur. Comput. 2024

   Bib HTML

   @article{TDSC:ACDDRSSTWW24,
     author = {Alsadi, Mohammed and Casey, Matthew and Dragan, Constantin Catalin and Dupressoir, François and Riley, Luke and Sallal, Muntadher and Schneider, Steve and Treharne, Helen and Wadsworth, Joe and Wright, Phil},
     title = {Towards End-to-End Verifiable Online Voting: Adding Verifiability
                       to Established Voting Systems},
     journal = {{IEEE} Trans. Dependable Secur. Comput.},
     volume = {21},
     number = {4},
     pages = {3357--3374},
     year = {2024},
     url = {https://doi.org/10.1109/TDSC.2023.3327859},
     doi = {10.1109/TDSC.2023.3327859},
     bibtex_show = {true}
   }

2023

1. Machine-Checked Security for XMSS as in RFC 8391 and SPHINCS⁺

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

   IACR Cryptol. ePrint Arch. 2023

   HTML
2. Machine-Checked Security for XMSS as in RFC 8391 and SPHINCS⁺

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

   In CRYPTO 2023 2023

   Eprint Bib Code

   @inproceedings{CRYPTO:BDGHMS23,
     author = {Barbosa, Manuel and Dupressoir, François and Grégoire, Benjamin and Hülsing, Andreas and Meijers, Matthias and Strub, Pierre{-}Yves},
     title = {Machine-Checked Security for {XMSS} as in {RFC} 8391 and {SPHINCS}<sup>+</sup>},
     booktitle = {{CRYPTO} 2023},
     note = {To appear.},
     year = {2023},
     eprint = {https://eprint.iacr.org/2023/408},
     code = {https://github.com/MM45/FV-XMSS-EC},
     selected = {true},
     bibtex_show = {true}
   }

2022

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

   Constantin Cătălin Drăgan,  François Dupressoir, Ehsan Estaji, Kristian Gjøsteen, Thomas Haines, Peter Y. A. Ryan, Peter B. Rønne, and Morten Rotvold Solberg

   IACR Cryptol. ePrint Arch. 2022

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

   François Dupressoir, Konrad Kohbrok, and Sabine Oechsner

   In 35th IEEE Computer Security Foundations Symposium, CSF 2022, Haifa, Israel, August 7-10, 2022 2022

   Eprint Bib Code

   @inproceedings{CSF:DupKohOec22,
     author = {Dupressoir, François and Kohbrok, Konrad and Oechsner, Sabine},
     title = {Bringing State-Separating Proofs to {EasyCrypt}-A Security Proof
                      for {Cryptobox}},
     booktitle = {35th {IEEE} Computer Security Foundations Symposium, {CSF}
                      2022, Haifa, Israel, August 7-10, 2022},
     year = {2022},
     eprint = {https://eprint.iacr.org/2021/326},
     code = {https://gitlab.com/fdupress/ec-cryptobox.git},
     selected = {true},
     bibtex_show = {true}
   }

3. Machine-checked proofs of privacy against malicious boards for Selene & Co

   Constantin Cătălin Drăgan,  François Dupressoir, Ehsan Estaji, Kristian Gjøsteen, Thomas Haines, Peter Y. A. Ryan, Peter B. Rønne, and Morten Rotvold Solberg

   In 35th IEEE Computer Security Foundations Symposium, CSF 2022, Haifa, Israel, August 7-10, 2022 2022

   Eprint Bib Code

   @inproceedings{CSF:DDEGHRRS22,
     author = {Drăgan, Constantin Cătălin and Dupressoir, François and Estaji, Ehsan and Gjøsteen, Kristian and Haines, Thomas and Ryan, Peter Y. A. and Rønne, Peter B. and Solberg, Morten Rotvold},
     title = {Machine-checked proofs of privacy against malicious boards
                      for {Selene} \& {Co}},
     booktitle = {35th {IEEE} Computer Security Foundations Symposium, {CSF}
                      2022, Haifa, Israel, August 7-10, 2022},
     year = {2022},
     eprint = {https://eprint.iacr.org/2022/1182},
     code = {https://github.com/mortensol/du-mb-bpriv},
     bibtex_show = {true}
   }

2021

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

   François Dupressoir, Konrad Kohbrok, and Sabine Oechsner

   IACR Cryptol. ePrint Arch. 2021

   HTML
2. Mechanised Models and Proofs for Distance-Bounding

   Ioana Boureanu, Constantin Cătălin Drăgan,  François Dupressoir, David Gérault, and Pascal Lafourcade

   In 34th IEEE Computer Security Foundations Symposium, CSF 2021, Dubrovnik, Croatia, June 21-25, 2021 2021

   Eprint Bib HTML Code

   @inproceedings{CSF:BDDG021,
     author = {Boureanu, Ioana and Drăgan, Constantin Cătălin and Dupressoir, François and Gérault, David and Lafourcade, Pascal},
     title = {Mechanised Models and Proofs for Distance-Bounding},
     booktitle = {34th {IEEE} Computer Security Foundations Symposium, {CSF}
                      2021, Dubrovnik, Croatia, June 21-25, 2021},
     pages = {1--16},
     publisher = {{IEEE}},
     year = {2021},
     url = {https://doi.org/10.1109/CSF51468.2021.00049},
     doi = {10.1109/CSF51468.2021.00049},
     eprint = {https://eprint.iacr.org/2020/1000},
     code = {https://gitlab.com/ec-db/ec-db.git},
     selected = {true},
     bibtex_show = {true}
   }

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

   Bib HTML Code

   @inproceedings{CSF:DupZai21,
     author = {Dupressoir, François and Zain, Sara},
     title = {Machine-Checking Unforgeability Proofs for Signature Schemes with
                      Tight Reductions to the Computational Diffie-Hellman Problem},
     booktitle = {34th {IEEE} Computer Security Foundations Symposium, {CSF} 2021, Dubrovnik,
                      Croatia, June 21-25, 2021},
     pages = {1--15},
     publisher = {{IEEE}},
     year = {2021},
     url = {https://doi.org/10.1109/CSF51468.2021.00014},
     doi = {10.1109/CSF51468.2021.00014},
     code = {https://gitlab.com/ec-zksigs/edl.git},
     bibtex_show = {true}
   }

2020

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

   Ioana Boureanu, Constantin Cătălin Drăgan,  François Dupressoir, David Gérault, and Pascal Lafourcade

   IACR Cryptol. ePrint Arch. 2020

   HTML
2. 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, and Pierre-Yves Strub

   J. Cryptogr. Eng. 2020

   Eprint Bib HTML

   @article{JCEN:BBDFGSS20,
     author = {Barthe, Gilles and Belaïd, Sonia and Dupressoir, François and Fouque, Pierre{-}Alain and Grégoire, Benjamin and Standaert, François{-}Xavier and Strub, Pierre{-}Yves},
     title = {Improved parallel mask refreshing algorithms: generic solutions with
                      parametrized non-interference and automated optimizations},
     journal = {J. Cryptogr. Eng.},
     volume = {10},
     number = {1},
     pages = {17--26},
     year = {2020},
     url = {https://doi.org/10.1007/s13389-018-00202-2},
     doi = {10.1007/s13389-018-00202-2},
     eprint = {https://eprint.iacr.org/2018/505},
     bibtex_show = {true}
   }

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

   Muntadher Sallal, Steve Schneider, Matthew Casey,  François Dupressoir, Helen Treharne, Constantin 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

   Bib HTML

   @inproceedings{ICDCS:SSCDTDRW20,
     author = {Sallal, Muntadher and Schneider, Steve and Casey, Matthew and Dupressoir, François and Treharne, Helen and Drăgan, Constantin Cătălin and Riley, Luke and Wright, Phil},
     title = {Augmenting an Internet Voting System with Selene Verifiability using
                      Permissioned Distributed Ledger},
     booktitle = {40th {IEEE} International Conference on Distributed Computing Systems,
                      {ICDCS} 2020, Singapore, November 29 - December 1, 2020},
     pages = {1167--1168},
     publisher = {{IEEE}},
     year = {2020},
     url = {https://doi.org/10.1109/ICDCS47774.2020.00124},
     doi = {10.1109/ICDCS47774.2020.00124},
     bibtex_show = {true}
   }

2019

1. VMV: Augmenting an Internet Voting System with Selene Verifiability

   Muntadher Sallal, Steve A. Schneider, Matthew Casey, Constantin Cătălin Drăgan,  François Dupressoir, Luke Riley, Helen Treharne, Joe Wadsworth, and Phil Wright

   CoRR 2019

   HTML
2. 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, and Pierre-Yves Strub

   IACR Cryptol. ePrint Arch. 2019

   HTML
3. 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, and Pierre-Yves Strub

   In Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, CCS 2019, London, UK, November 11-15, 2019 2019

   Eprint Bib HTML Code

   @inproceedings{CCS:ABBBDGL0S19,
     author = {Almeida, José Bacelar and Baritel{-}Ruet, Cécile and Barbosa, Manuel and Barthe, Gilles and Dupressoir, François and Grégoire, Benjamin and Laporte, Vincent and Oliveira, Tiago and Stoughton, Alley and Strub, Pierre{-}Yves},
     editor = {Cavallaro, Lorenzo and Kinder, Johannes and Wang, XiaoFeng and Katz, Jonathan},
     title = {Machine-Checked Proofs for Cryptographic Standards: Indifferentiability
                      of Sponge and Secure High-Assurance Implementations of {SHA-3}},
     booktitle = {Proceedings of the 2019 {ACM} {SIGSAC} Conference on Computer and
                      Communications Security, {CCS} 2019, London, UK, November 11-15, 2019},
     pages = {1607--1622},
     publisher = {{ACM}},
     year = {2019},
     url = {https://doi.org/10.1145/3319535.3363211},
     doi = {10.1145/3319535.3363211},
     eprint = {https://eprint.iacr.org/2019/1155},
     code = {https://gitlab.com/easycrypt/sha3.git},
     bibtex_show = {true},
     selected = {true}
   }

2018

1. 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, and Pierre-Yves Strub

   IACR Cryptol. ePrint Arch. 2018

   HTML
2. Formal Security Proof of CMAC and Its Variants

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

   In 31st IEEE Computer Security Foundations Symposium, CSF 2018, Oxford, United Kingdom, July 9-12, 2018 2018

   Bib HTML

   @inproceedings{CSF:BDFG18,
     author = {Baritel{-}Ruet, Cécile and Dupressoir, François and Fouque, Pierre{-}Alain and Grégoire, Benjamin},
     title = {Formal Security Proof of {CMAC} and Its Variants},
     booktitle = {31st {IEEE} Computer Security Foundations Symposium, {CSF} 2018, Oxford,
                      United Kingdom, July 9-12, 2018},
     pages = {91--104},
     publisher = {{IEEE} Computer Society},
     year = {2018},
     url = {https://doi.org/10.1109/CSF.2018.00014},
     doi = {10.1109/CSF.2018.00014},
     bibtex_show = {true}
   }

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

   Véronique Cortier, Constantin Cătălin Drăgan,  François Dupressoir, and Bogdan Warinschi

   In 31st IEEE Computer Security Foundations Symposium, CSF 2018, Oxford, United Kingdom, July 9-12, 2018 2018

   Bib HTML Code

   @inproceedings{CSF:CDDW18,
     author = {Cortier, Véronique and Drăgan, Constantin Cătălin and Dupressoir, François and Warinschi, Bogdan},
     title = {Machine-Checked Proofs for Electronic Voting: Privacy and Verifiability
                      for Belenios},
     booktitle = {31st {IEEE} Computer Security Foundations Symposium, {CSF} 2018, Oxford,
                      United Kingdom, July 9-12, 2018},
     pages = {298--312},
     publisher = {{IEEE} Computer Society},
     year = {2018},
     url = {https://doi.org/10.1109/CSF.2018.00029},
     doi = {10.1109/CSF.2018.00029},
     code = {https://gitlab.com/ec-evoting/belenios.git},
     bibtex_show = {true}
   }

2017

1. 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, and Vitor Pereira

   IACR Cryptol. ePrint Arch. 2017

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

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

   IACR Cryptol. ePrint Arch. 2017

   HTML
3. 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, and Vitor Pereira

   In Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, TX, USA, October 30 - November 03, 2017 2017

   Eprint Bib HTML Code

   @inproceedings{CCS:ABBDGLP17,
     author = {Almeida, José Bacelar and Barbosa, Manuel and Barthe, Gilles and Dupressoir, François and Grégoire, Benjamin and Laporte, Vincent and Pereira, Vitor},
     editor = {Thuraisingham, Bhavani M. and Evans, David and Malkin, Tal and Xu, Dongyan},
     title = {A Fast and Verified Software Stack for Secure Function Evaluation},
     booktitle = {Proceedings of the 2017 {ACM} {SIGSAC} Conference on Computer and
                      Communications Security, {CCS} 2017, Dallas, TX, USA, October 30 -
                      November 03, 2017},
     pages = {1989--2006},
     publisher = {{ACM}},
     year = {2017},
     url = {https://doi.org/10.1145/3133956.3134017},
     doi = {10.1145/3133956.3134017},
     eprint = {http://eprint.iacr.org/2017/821},
     code = {https://gitlab.com/gcircuits/yao.git},
     bibtex_show = {true},
     selected = {true}
   }

4. 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, and Pierre-Yves Strub

   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

   Eprint Bib HTML

   @inproceedings{EC:BDFGSS17,
     author = {Barthe, Gilles and Dupressoir, François and Faust, Sebastian and Grégoire, Benjamin and Standaert, François{-}Xavier and Strub, Pierre{-}Yves},
     editor = {Coron, Jean{-}Sébastien and Nielsen, Jesper Buus},
     title = {Parallel Implementations of Masking Schemes and the Bounded Moment
                      Leakage Model},
     booktitle = {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}},
     series = {Lecture Notes in Computer Science},
     volume = {10210},
     pages = {535--566},
     year = {2017},
     url = {https://doi.org/10.1007/978-3-319-56620-7\_19},
     doi = {10.1007/978-3-319-56620-7\_19},
     eprint = {http://eprint.iacr.org/2016/912},
     bibtex_show = {true}
   }

5. Machine-Checked Proofs of Privacy for Electronic Voting Protocols

   Véronique Cortier, Constantin Cătălin Drăgan,  François Dupressoir, Benedikt Schmidt, Pierre-Yves Strub, and Bogdan Warinschi

   In 2017 IEEE Symposium on Security and Privacy, SP 2017, San Jose, CA, USA, May 22-26, 2017 2017

   Bib HTML Code

   @inproceedings{SP:CDDSSW17,
     author = {Cortier, Véronique and Drăgan, Constantin Cătălin and Dupressoir, François and Schmidt, Benedikt and Strub, Pierre{-}Yves and Warinschi, Bogdan},
     title = {Machine-Checked Proofs of Privacy for Electronic Voting Protocols},
     booktitle = {2017 {IEEE} Symposium on Security and Privacy, {SP} 2017, San Jose,
                      CA, USA, May 22-26, 2017},
     pages = {993--1008},
     publisher = {{IEEE} Computer Society},
     year = {2017},
     url = {https://doi.org/10.1109/SP.2017.28},
     doi = {10.1109/SP.2017.28},
     code = {https://gitlab.com/ec-evoting/helios.git},
     bibtex_show = {true}
   }

2016

1. 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, and Pierre-Yves Strub

   IACR Cryptol. ePrint Arch. 2016

   HTML
2. 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, and Rébecca Zucchini

   In Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, Vienna, Austria, October 24-28, 2016 2016

   Eprint Bib HTML

   @inproceedings{CCS:BBDFGSZ16,
     author = {Barthe, Gilles and Belaïd, Sonia and Dupressoir, François and Fouque, Pierre{-}Alain and Grégoire, Benjamin and Strub, Pierre{-}Yves and Zucchini, Rébecca},
     editor = {Weippl, Edgar R. and Katzenbeisser, Stefan and Kruegel, Christopher and Myers, Andrew C. and Halevi, Shai},
     title = {Strong Non-Interference and Type-Directed Higher-Order Masking},
     booktitle = {Proceedings of the 2016 {ACM} {SIGSAC} Conference on Computer and
                      Communications Security, Vienna, Austria, October 24-28, 2016},
     pages = {116--129},
     publisher = {{ACM}},
     year = {2016},
     url = {https://doi.org/10.1145/2976749.2978427},
     doi = {10.1145/2976749.2978427},
     eprint = {http://eprint.iacr.org/2015/506},
     bibtex_show = {true}
   }

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

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

   In Fast Software Encryption - 23rd International Conference, FSE 2016, Bochum, Germany, March 20-23, 2016, Revised Selected Papers 2016

   Eprint Bib HTML Code

   @inproceedings{FSE:ABBD16,
     author = {Almeida, José Bacelar and Barbosa, Manuel and Barthe, Gilles and Dupressoir, François},
     editor = {Peyrin, Thomas},
     title = {Verifiable Side-Channel Security of Cryptographic Implementations:
                      Constant-Time {MEE-CBC}},
     booktitle = {Fast Software Encryption - 23rd International Conference, {FSE} 2016,
                      Bochum, Germany, March 20-23, 2016, Revised Selected Papers},
     series = {Lecture Notes in Computer Science},
     volume = {9783},
     pages = {163--184},
     publisher = {Springer},
     year = {2016},
     url = {https://doi.org/10.1007/978-3-662-52993-5\_9},
     doi = {10.1007/978-3-662-52993-5\_9},
     note = {\bfseries Best paper award.},
     eprint = {http://eprint.iacr.org/2015/1241},
     code = {https://github.com/EasyCrypt/easycrypt/tree/1.0/examples/MEE-CBC},
     bibtex_show = {true}
   }

4. Verifying Constant-Time Implementations

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

   In 25th USENIX Security Symposium, USENIX Security 16, Austin, TX, USA, August 10-12, 2016 2016

   Bib HTML

   @inproceedings{USS:ABBDE16,
     author = {Almeida, José Bacelar and Barbosa, Manuel and Barthe, Gilles and Dupressoir, François and Emmi, Michael},
     editor = {Holz, Thorsten and Savage, Stefan},
     title = {Verifying Constant-Time Implementations},
     booktitle = {25th {USENIX} Security Symposium, {USENIX} Security 16, Austin, TX,
                      USA, August 10-12, 2016},
     pages = {53--70},
     publisher = {{USENIX} Association},
     year = {2016},
     url = {https://www.usenix.org/conference/usenixsecurity16/technical-sessions/presentation/almeida},
     bibtex_show = {true}
   }

2015

1. Verified Proofs of Higher-Order Masking

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

   IACR Cryptol. ePrint Arch. 2015

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

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

   IACR Cryptol. ePrint Arch. 2015

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

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

   IACR Cryptol. ePrint Arch. 2015

   HTML
4. Verified Proofs of Higher-Order Masking

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

   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

   Eprint Bib HTML

   @inproceedings{EC:BBDFGS15,
     author = {Barthe, Gilles and Belaïd, Sonia and Dupressoir, François and Fouque, Pierre{-}Alain and Grégoire, Benjamin and Strub, Pierre{-}Yves},
     editor = {Oswald, Elisabeth and Fischlin, Marc},
     title = {Verified Proofs of Higher-Order Masking},
     booktitle = {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}},
     series = {Lecture Notes in Computer Science},
     volume = {9056},
     pages = {457--485},
     publisher = {Springer},
     year = {2015},
     url = {https://doi.org/10.1007/978-3-662-46800-5\_18},
     doi = {10.1007/978-3-662-46800-5\_18},
     eprint = {http://eprint.iacr.org/2015/060},
     bibtex_show = {true}
   }

2014

1. Making RSA-PSS Provably Secure Against Non-Random Faults

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

   IACR Cryptol. ePrint Arch. 2014

   HTML
2. Synthesis of Fault Attacks on Cryptographic Implementations

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

   IACR Cryptol. ePrint Arch. 2014

   HTML
3. Verified Implementations for Secure and Verifiable Computation

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

   IACR Cryptol. ePrint Arch. 2014

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

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

   J. Comput. Secur. 2014

   Eprint Bib HTML

   @article{JCS:DGJN14,
     author = {Dupressoir, François and Gordon, Andrew D. and Jürjens, Jan and Naumann, David A.},
     title = {Guiding a general-purpose {C} verifier to prove cryptographic protocols},
     journal = {J. Comput. Secur.},
     volume = {22},
     number = {5},
     pages = {823--866},
     year = {2014},
     url = {https://doi.org/10.3233/JCS-140508},
     doi = {10.3233/JCS-140508},
     eprint = {http://arxiv.org/abs/1312.6532},
     bibtex_show = {true}
   }

5. Synthesis of Fault Attacks on Cryptographic Implementations

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

   In Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, Scottsdale, AZ, USA, November 3-7, 2014 2014

   Eprint Bib HTML

   @inproceedings{CCS:BDFGZ14,
     author = {Barthe, Gilles and Dupressoir, François and Fouque, Pierre{-}Alain and Grégoire, Benjamin and Zapalowicz, Jean{-}Christophe},
     editor = {Ahn, Gail{-}Joon and Yung, Moti and Li, Ninghui},
     title = {Synthesis of Fault Attacks on Cryptographic Implementations},
     booktitle = {Proceedings of the 2014 {ACM} {SIGSAC} Conference on Computer and
                      Communications Security, Scottsdale, AZ, USA, November 3-7, 2014},
     pages = {1016--1027},
     publisher = {{ACM}},
     year = {2014},
     url = {https://doi.org/10.1145/2660267.2660304},
     doi = {10.1145/2660267.2660304},
     eprint = {http://eprint.iacr.org/2014/436},
     bibtex_show = {true}
   }

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

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

   In Cryptographic Hardware and Embedded Systems - CHES 2014 - 16th International Workshop, Busan, South Korea, September 23-26, 2014. Proceedings 2014

   Eprint Bib HTML

   @inproceedings{CHES:BDFGTZ14,
     author = {Barthe, Gilles and Dupressoir, François and Fouque, Pierre{-}Alain and Grégoire, Benjamin and Tibouchi, Mehdi and Zapalowicz, Jean{-}Christophe},
     editor = {Batina, Lejla and Robshaw, Matthew},
     title = {Making {RSA-PSS} Provably Secure against Non-random Faults},
     booktitle = {Cryptographic Hardware and Embedded Systems - {CHES} 2014 - 16th International
                      Workshop, Busan, South Korea, September 23-26, 2014. Proceedings},
     series = {Lecture Notes in Computer Science},
     volume = {8731},
     pages = {206--222},
     publisher = {Springer},
     year = {2014},
     url = {https://doi.org/10.1007/978-3-662-44709-3\_12},
     doi = {10.1007/978-3-662-44709-3\_12},
     eprint = {http://eprint.iacr.org/2014/252},
     bibtex_show = {true}
   }

2013

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

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

   CoRR 2013

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

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

   IACR Cryptol. ePrint Arch. 2013

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

   François Dupressoir

   IACR Cryptol. ePrint Arch. 2013

   Bib HTML

   @phdthesis{PhD:Dupressoir13,
     author = {Dupressoir, François},
     title = {Proving cryptographic {C} programs secure with general-purpose verification
                      tools},
     school = {Open University, Milton Keynes, {UK}},
     year = {2013},
     url = {http://oro.open.ac.uk/37627/},
     bibtex_show = {true}
   }

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

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

   In 2013 ACM SIGSAC Conference on Computer and Communications Security, CCS’13, Berlin, Germany, November 4-8, 2013 2013

   Eprint Bib HTML

   @inproceedings{CCS:ABBD13,
     author = {Almeida, José Bacelar and Barbosa, Manuel and Barthe, Gilles and Dupressoir, François},
     editor = {Sadeghi, Ahmad{-}Reza and Gligor, Virgil D. and Yung, Moti},
     title = {Certified computer-aided cryptography: efficient provably secure machine
                      code from high-level implementations},
     booktitle = {2013 {ACM} {SIGSAC} Conference on Computer and Communications Security,
                      CCS'13, Berlin, Germany, November 4-8, 2013},
     pages = {1217--1230},
     publisher = {{ACM}},
     year = {2013},
     url = {https://doi.org/10.1145/2508859.2516652},
     doi = {10.1145/2508859.2516652},
     eprint = {http://eprint.iacr.org/2013/316},
     bibtex_show = {true}
   }

5. EasyCrypt: A Tutorial

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

   In Foundations of Security Analysis and Design VII - FOSAD 2012/2013 Tutorial Lectures 2013

   Bib HTML

   @inproceedings{FOSAD:BDGKSS13,
     author = {Barthe, Gilles and Dupressoir, François and Grégoire, Benjamin and Kunz, César and Schmidt, Benedikt and Strub, Pierre{-}Yves},
     editor = {Aldini, Alessandro and López, Javier and Martinelli, Fabio},
     title = {EasyCrypt: {A} Tutorial},
     booktitle = {Foundations of Security Analysis and Design {VII} - {FOSAD} 2012/2013
                      Tutorial Lectures},
     series = {Lecture Notes in Computer Science},
     volume = {8604},
     pages = {146--166},
     publisher = {Springer},
     year = {2013},
     url = {https://doi.org/10.1007/978-3-319-10082-1\_6},
     doi = {10.1007/978-3-319-10082-1\_6},
     bibtex_show = {true}
   }

2011

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

   François Dupressoir, Andrew D. Gordon, Jan 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

   Bib HTML

   @inproceedings{CSF:DGJN11,
     author = {Dupressoir, François and Gordon, Andrew D. and Jürjens, Jan and Naumann, David A.},
     title = {Guiding a General-Purpose {C} Verifier to Prove Cryptographic Protocols},
     booktitle = {Proceedings of the 24th {IEEE} Computer Security Foundations Symposium,
                      {CSF} 2011, Cernay-la-Ville, France, 27-29 June, 2011},
     pages = {3--17},
     publisher = {{IEEE} Computer Society},
     year = {2011},
     url = {https://doi.org/10.1109/CSF.2011.8},
     doi = {10.1109/CSF.2011.8},
     bibtex_show = {true}
   }

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

   Mihhail Aizatulin,  François Dupressoir, Andrew 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

   Bib HTML

   @inproceedings{FAST:ADGJ11,
     author = {Aizatulin, Mihhail and Dupressoir, François and Gordon, Andrew D. and Jürjens, Jan},
     editor = {Barthe, Gilles and Datta, Anupam and Etalle, Sandro},
     title = {Verifying Cryptographic Code in {C:} Some Experience and the Csec
                      Challenge},
     booktitle = {Formal Aspects of Security and Trust - 8th International Workshop,
                      {FAST} 2011, Leuven, Belgium, September 12-14, 2011. Revised Selected
                      Papers},
     series = {Lecture Notes in Computer Science},
     volume = {7140},
     pages = {1--20},
     publisher = {Springer},
     year = {2011},
     url = {https://doi.org/10.1007/978-3-642-29420-4\_1},
     doi = {10.1007/978-3-642-29420-4\_1},
     bibtex_show = {true}
   }