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

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
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

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

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

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

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

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}
}

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

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

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}
}

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

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

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}
}

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

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
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

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

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

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}
}

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

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
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

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}
}

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}
}

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

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

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}
}

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}
}

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

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
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
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

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

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
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
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

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}
}

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}
}

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

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
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

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}
}

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}
}

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

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}
}

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}
}