default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDFrançois Dupressoir
Person information
- affiliation: University of Bristol, UK
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2024
[j4]Mohammed Alsadi
, Matthew Casey, Constantin Catalin Dragan, François Dupressoir, Luke Riley, Muntadher Sallal, Steve Schneider, Helen Treharne, Joe Wadsworth, Phil Wright:
Towards End-to-End Verifiable Online Voting: Adding Verifiability to Established Voting Systems. IEEE Trans. Dependable Secur. Comput. 21(4): 3357-3374 (2024)- [c24]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:
Formally Verifying Kyber - Episode V: Machine-Checked IND-CCA Security and Correctness of ML-KEM in EasyCrypt. CRYPTO (2) 2024: 384-421 - [i20]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:
Formally verifying Kyber Episode V: Machine-checked IND-CCA security and correctness of ML-KEM in EasyCrypt. IACR Cryptol. ePrint Arch. 2024: 843 (2024) - [i19]Manuel Barbosa, François Dupressoir, Andreas Hülsing, Matthias Meijers, Pierre-Yves Strub:
A Tight Security Proof for $\mathrm{SPHINCS^{+}}$, Formally Verified. IACR Cryptol. ePrint Arch. 2024: 910 (2024) - 2023
- [j3]Constantin Catalin Dragan, François Dupressoir, Ehsan Estaji, Kristian Gjøsteen, Thomas Haines, Peter Y. A. Ryan, Peter B. Rønne, Morten Rotvold Solberg:
Machine-checked proofs of privacy against malicious boards for Selene & Co. J. Comput. Secur. 31(5): 469-499 (2023) - [c23]Manuel Barbosa, François Dupressoir, Benjamin Grégoire, Andreas Hülsing, Matthias Meijers, Pierre-Yves Strub:
Machine-Checked Security for rmXMSS as in RFC 8391 and $\mathrm {SPHINCS^{+}} $. CRYPTO (5) 2023: 421-454 - [c22]Constantin Catalin Dragan, François Dupressoir, Kristian Gjøsteen, Thomas Haines, Peter B. Rønne, Morten Rotvold Solberg:
Machine-Checked Proofs of Accountability: How to sElect Who is to Blame. ESORICS (3) 2023: 471-491 - [i18]Manuel Barbosa, François Dupressoir, Benjamin Grégoire, Andreas Hülsing, Matthias Meijers, Pierre-Yves Strub:
Machine-Checked Security for $\mathrm{XMSS}$ as in RFC 8391 and $\mathrm{SPHINCS}^{+}$. IACR Cryptol. ePrint Arch. 2023: 408 (2023) - 2022
- [c21]François Dupressoir, Konrad Kohbrok, Sabine Oechsner:
Bringing State-Separating Proofs to EasyCrypt A Security Proof for Cryptobox. CSF 2022: 227-242 - [c20]Constantin Catalin Dragan, François Dupressoir, Ehsan Estaji, Kristian Gjøsteen, Thomas Haines, Peter Y. A. Ryan, Peter B. Rønne, Morten Rotvold Solberg:
Machine-Checked Proofs of Privacy Against Malicious Boards for Selene & Co. CSF 2022: 335-347 - [i17]Constantin Catalin Dragan, François Dupressoir, Ehsan Estaji, Kristian Gjøsteen, Thomas Haines, Peter Y. A. Ryan, Peter B. Rønne, Morten Rotvold Solberg:
Machine-Checked Proofs of Privacy Against Malicious Boards for Selene & Co. IACR Cryptol. ePrint Arch. 2022: 1182 (2022) - 2021
- [c19]Ioana Boureanu, Constantin Catalin Dragan, François Dupressoir, David Gérault, Pascal Lafourcade:
Mechanised Models and Proofs for Distance-Bounding. CSF 2021: 1-16 - [c18]François Dupressoir, Sara Zain:
Machine-Checking Unforgeability Proofs for Signature Schemes with Tight Reductions to the Computational Diffie-Hellman Problem. CSF 2021: 1-15 - [i16]François Dupressoir, Konrad Kohbrok, Sabine Oechsner:
Bringing State-Separating Proofs to EasyCrypt - A Security Proof for Cryptobox. IACR Cryptol. ePrint Arch. 2021: 326 (2021) - 2020
- [j2]Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, François-Xavier Standaert, Pierre-Yves Strub:
Improved parallel mask refreshing algorithms: generic solutions with parametrized non-interference and automated optimizations. J. Cryptogr. Eng. 10(1): 17-26 (2020) - [c17]Muntadher Sallal, Steve Schneider, Matthew Casey, François Dupressoir, Helen Treharne, Constantin Catalin Dragan, Luke Riley, Phil Wright:
Augmenting an Internet Voting System with Selene Verifiability using Permissioned Distributed Ledger. ICDCS 2020: 1167-1168 - [i15]Ioana Boureanu, Constantin Catalin Dragan, François Dupressoir, David Gérault, Pascal Lafourcade:
Precise and Mechanised Models and Proofs for Distance-Bounding and an Application to Contactless Payments. IACR Cryptol. ePrint Arch. 2020: 1000 (2020)
2010 – 2019
- 2019
- [c16]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:
Machine-Checked Proofs for Cryptographic Standards: Indifferentiability of Sponge and Secure High-Assurance Implementations of SHA-3. CCS 2019: 1607-1622 - [i14]Muntadher Sallal, Steve A. Schneider, Matthew Casey, Constantin Catalin Dragan, François Dupressoir, Luke Riley, Helen Treharne, Joe Wadsworth, Phil Wright:
VMV: Augmenting an Internet Voting System with Selene Verifiability. CoRR abs/1912.00288 (2019) - [i13]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:
Machine-Checked Proofs for Cryptographic Standards. IACR Cryptol. ePrint Arch. 2019: 1155 (2019) - 2018
- [c15]Cécile Baritel-Ruet, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire:
Formal Security Proof of CMAC and Its Variants. CSF 2018: 91-104 - [c14]Véronique Cortier, Constantin Catalin Dragan, François Dupressoir, Bogdan Warinschi:
Machine-Checked Proofs for Electronic Voting: Privacy and Verifiability for Belenios. CSF 2018: 298-312 - [i12]Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, François-Xavier Standaert, Pierre-Yves Strub:
Improved Parallel Mask Refreshing Algorithms: Generic Solutions with Parametrized Non-Interference & Automated Optimizations. IACR Cryptol. ePrint Arch. 2018: 505 (2018) - 2017
- [c13]José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Vitor Pereira:
A Fast and Verified Software Stack for Secure Function Evaluation. CCS 2017: 1989-2006 - [c12]Gilles Barthe, François Dupressoir, Sebastian Faust, Benjamin Grégoire, François-Xavier Standaert, Pierre-Yves Strub:
Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model. EUROCRYPT (1) 2017: 535-566 - [c11]Véronique Cortier, Constantin Catalin Dragan, François Dupressoir, Benedikt Schmidt, Pierre-Yves Strub, Bogdan Warinschi:
Machine-Checked Proofs of Privacy for Electronic Voting Protocols. IEEE Symposium on Security and Privacy 2017: 993-1008 - [i11]José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, Vitor Pereira:
A Fast and Verified Software Stack for Secure Function Evaluation. IACR Cryptol. ePrint Arch. 2017: 821 (2017) - [i10]Gilles Barthe, François Dupressoir, Benjamin Grégoire:
A Note on 'Further Improving Efficiency of Higher-Order Masking Scheme by Decreasing Randomness Complexity'. IACR Cryptol. ePrint Arch. 2017: 1053 (2017) - 2016
- [c10]Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Pierre-Yves Strub, Rébecca Zucchini:
Strong Non-Interference and Type-Directed Higher-Order Masking. CCS 2016: 116-129 - [c9]José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir:
Verifiable Side-Channel Security of Cryptographic Implementations: Constant-Time MEE-CBC. FSE 2016: 163-184 - [c8]José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, Michael Emmi:
Verifying Constant-Time Implementations. USENIX Security Symposium 2016: 53-70 - [i9]Gilles Barthe, François Dupressoir, Sebastian Faust, Benjamin Grégoire, François-Xavier Standaert, Pierre-Yves Strub:
Parallel Implementations of Masking Schemes and the Bounded Moment Leakage Model. IACR Cryptol. ePrint Arch. 2016: 912 (2016) - 2015
- [c7]Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Pierre-Yves Strub:
Verified Proofs of Higher-Order Masking. EUROCRYPT (1) 2015: 457-485 - [i8]Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Pierre-Yves Strub:
Verified Proofs of Higher-Order Masking. IACR Cryptol. ePrint Arch. 2015: 60 (2015) - [i7]Gilles Barthe, Sonia Belaïd, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire:
Compositional Verification of Higher-Order Masking: Application to a Verifying Masking Compiler. IACR Cryptol. ePrint Arch. 2015: 506 (2015) - [i6]José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir:
Verifiable side-channel security of cryptographic implementations: constant-time MEE-CBC. IACR Cryptol. ePrint Arch. 2015: 1241 (2015) - 2014
- [j1]François Dupressoir, Andrew D. Gordon, Jan Jürjens, David A. Naumann:
Guiding a general-purpose C verifier to prove cryptographic protocols. J. Comput. Secur. 22(5): 823-866 (2014) - [c6]Gilles Barthe, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Jean-Christophe Zapalowicz:
Synthesis of Fault Attacks on Cryptographic Implementations. CCS 2014: 1016-1027 - [c5]Gilles Barthe, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Mehdi Tibouchi, Jean-Christophe Zapalowicz:
Making RSA-PSS Provably Secure against Non-random Faults. CHES 2014: 206-222 - [i5]Gilles Barthe, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Mehdi Tibouchi, Jean-Christophe Zapalowicz:
Making RSA-PSS Provably Secure Against Non-Random Faults. IACR Cryptol. ePrint Arch. 2014: 252 (2014) - [i4]Gilles Barthe, François Dupressoir, Pierre-Alain Fouque, Benjamin Grégoire, Jean-Christophe Zapalowicz:
Synthesis of Fault Attacks on Cryptographic Implementations. IACR Cryptol. ePrint Arch. 2014: 436 (2014) - [i3]José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Guillaume Davy, François Dupressoir, Benjamin Grégoire, Pierre-Yves Strub:
Verified Implementations for Secure and Verifiable Computation. IACR Cryptol. ePrint Arch. 2014: 456 (2014) - 2013
- [b1]François Dupressoir:
Proving cryptographic C programs secure with general-purpose verification tools. Open University, Milton Keynes, UK, 2013 - [c4]José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir:
Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations. CCS 2013: 1217-1230 - [c3]Gilles Barthe, François Dupressoir, Benjamin Grégoire, César Kunz, Benedikt Schmidt, Pierre-Yves Strub:
EasyCrypt: A Tutorial. FOSAD 2013: 146-166 - [i2]François Dupressoir, Andrew D. Gordon, Jan Jürjens, David A. Naumann:
Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols. CoRR abs/1312.6532 (2013) - [i1]José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir:
Certified computer-aided cryptography: efficient provably secure machine code from high-level implementations. IACR Cryptol. ePrint Arch. 2013: 316 (2013) - 2011
- [c2]François Dupressoir, Andrew D. Gordon, Jan Jürjens, David A. Naumann:
Guiding a General-Purpose C Verifier to Prove Cryptographic Protocols. CSF 2011: 3-17 - [c1]Mihhail Aizatulin, François Dupressoir, Andrew D. Gordon, Jan Jürjens:
Verifying Cryptographic Code in C: Some Experience and the Csec Challenge. Formal Aspects in Security and Trust 2011: 1-20
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-11-05 21:59 CET by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
