Santiago Zanella-Béguelin

Principal Researcher

Connect on LinkedIn

Publications

View by:

- Project Everest: Perspectives from Developing Industrial-Grade High-Assurance Software
  
  D. Ahman, Karthik Bhargavan, Barry Bond, Jay Bosamiya, Chris Brzuska, Antoine Delignat-Lavaud, Cédric Fournet, Aymeric Fromherz, Sydney Gibson, Chris Hawblitzel, Cătălin Hrițcu, Markulf Kohlweiss, Guido Martínez, Haobin Ni, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Exequiel Rivas, Nikhil Swamy, Santiago Zanella-Béguelin
  
  ACM Transactions on Programming Languages and Systems | April 2026
  
  DOI
- Optimizing Agent Planning for Security and Autonomy
  
  Aashish Kolluri, Rishi Sharma, Manuel Costa, Boris Köpf, Tobias Niessen, Mark Russinovich, Shruti Tople, Santiago Zanella-Béguelin
  
  ICLR 2026 | February 2026
  
  Publication Preprint Project
- Beyond Membership: Limitations of Add/Remove Adjacency in Differential Privacy
  
  Gauri Pradhan, Joonas Jälkö, Santiago Zanella-Béguelin, Antti Honkela
  
  ICLR 2026 | November 2025
  
  DOI Publication
- Permissive Information-Flow Analysis for Large Language Models
  
  Shoaib Ahmed Siddiqui, Radhika Gaonkar, Boris Köpf, David Krueger, Andrew Paverd, Ahmed Salem, Shruti Tople, Lukas Wutschitz, Menglin Xia, Santiago Zanella-Béguelin
  
  Transactions on Machine Learning Research (TMLR) | October 2025
  
  Publication Publication Project
- Securing AI Agents with Information-Flow Control
  
  Manuel Costa, Boris Köpf, Aashish Kolluri, Andrew Paverd, Mark Russinovich, Ahmed Salem, Shruti Tople, Lukas Wutschitz, Santiago Zanella-Béguelin
  
  May 2025
  
  DOI Publication Publication Project Project
- The Canary’s Echo: Auditing Privacy Risks of LLM-Generated Synthetic Text
  
  Matthieu Meeus, Lukas Wutschitz, Santiago Zanella-Béguelin, Reza Shokri, Shruti Tople
  
  February 2025
  
  DOI Preprint Project
- The Canary’s Echo: Auditing Privacy Risks of LLM-Generated Synthetic Text
  
  Matthieu Meeus, Lukas Wutschitz, Santiago Zanella-Béguelin, Shruti Tople, Reza Shokri
  
  ICML 2025 | February 2025
  
  DOI Publication Publication
- Closed-Form Bounds for DP-SGD against Record-level Inference
  
  Giovanni Cherubin, Boris Köpf, Andrew Paverd, Shruti Tople, Lukas Wutschitz, Santiago Zanella-Béguelin
  
  USENIX Security Symposium | August 2024
  
  Publication Project
- Dataset and Lessons Learned from the 2024 SaTML LLM Capture-the-Flag Competition
  
  Edoardo Debenedetti, Javier Rando, Daniel Paleka, Fineas Silaghi, Dragos Albastroiu, Niv Cohen, Yuval Lemberg, Reshmi Ghosh, Ahmed Salem, Rui Wen, Giovanni Cherubin, Santiago Zanella-Béguelin, Robin Schmid, Victor Klemm, Takahiro Miki, Chenhao Li, Stefan Kraft, Mario Fritz, Florian Tramer, Sahar Abdelnabi, Lea Schönherr
  
  NeurIPS 2024 | June 2024
  
  Preprint Project
- On the Efficacy of Differentially Private Few-shot Image Classification
  
  Marlon Tobaben, Aliaksandra Shysheya, John Bronskill, Andrew Paverd, Shruti Tople, Santiago Zanella-Béguelin, Richard Turner, Antti Honkela
  
  Transactions on Machine Learning Research | December 2023, Vol 2023
  
  DOI Preprint Preprint Publication Project
- Bayesian Estimation of Differential Privacy
  
  Santiago Zanella-Béguelin, Lukas Wutschitz, Shruti Tople, Ahmed Salem, Victor Ruehle, Andrew Paverd, Mohammad Naseri, Boris Köpf, Daniel Jones
  
  2023 International Conference on Machine Learning | July 2023
  
  Editor(s): Barbara Engelhardt, Emma Brunskill, Kyunghyun Cho
  
  Publication Project
- Analyzing Leakage of Personally Identifiable Information in Language Models
  
  Nils Lukas, Ahmed Salem, Robert Sim, Shruti Tople, Lukas Wutschitz, Santiago Zanella-Béguelin
  
  2023 IEEE Symposium on Security and Privacy | May 2023
  
  Publication PDF DOI Project
- SoK: Let the Privacy Games Begin! A Unified Treatment of Data Inference Privacy in Machine Learning
  
  Ahmed Salem, Giovanni Cherubin, David Evans, Boris Köpf, Andrew Paverd, Anshuman Suri, Shruti Tople, Santiago Zanella-Béguelin
  
  2023 IEEE Symposium on Security and Privacy | May 2023
  
  Publication PDF DOI Project
- Grey-box Extraction of Natural Language Models
  
  Santiago Zanella-Béguelin, Shruti Tople, Andrew Paverd, Boris Köpf
  
  International Conference on Machine Learning | July 2021
  
  Editor(s): Marina Meila and Tong Zhang
  
  PDF Project
- HACL×N: Verified Generic SIMD Crypto (for all your favourite platforms)
  
  Marina Polubelova, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin Beurdouche, Aymeric Fromherz, Natalia Kulatova, Santiago Zanella-Béguelin
  
  ACM Conference on Computer and Communications Security (CCS) | November 2020
  
  Publication Access Project
- Analyzing Information Leakage of Updates to Natural Language Models
  
  Santiago Zanella-Béguelin, Lukas Wutschitz, Shruti Tople, Victor Ruehle, Andrew Paverd, Olga Ohrimenko, Boris Köpf, Marc Brockschmidt
  
  ACM Conference on Computer and Communication Security (CCS) | November 2020
  
  Author's Version Project
- EverCrypt: A Fast, Veriﬁed, Cross-Platform Cryptographic Provider
  
  Jonathan Protzenko, Bryan Parno, Aymeric Fromherz, Chris Hawblitzel, Marina Polubelova, Karthikeyan Bhargavan, Benjamin Beurdouche, Joonwon Choi, Antoine Delignat-Lavaud, Cédric Fournet, Natalia Kulatova, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Christoph M. Wintersteiger, Santiago Zanella-Béguelin
  
  IEEE Symposium on Security and Privacy | May 2020
  
  Publication Video Access Github Project
- Imperfect forward secrecy: how Diffie-Hellman fails in practice
  
  David Adrian, Karthik Bhargavan, Zakir Durumeric, Pierrick Gaudry, Matthew Green, J. Alex Halderman, Nadia Heninger, Drew Springall, Emmanuel Thomé, Luke Valenta, Benjamin VanderSloot, Eric Wustrow, Santiago Zanella-Béguelin, Paul Zimmermann
  
  Communications of The ACM | December 2018, Vol 62(1): pp. 106-114
  
  PDF DOI
- A monadic framework for relational verification: applied to information security, program equivalence, and optimizations
  
  Niklas Grimm, Kenji Maillard, Cédric Fournet, Catalin Hritcu, Matteo Maffei, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Santiago Zanella-Béguelin
  
  CPP 2018 | January 2018
  
  Publication Publication Publication Project
- Implementing and Proving the TLS 1.3 Record Layer
  
  Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy, Santiago Zanella-Béguelin, Karthikeyan Bhargavan , Jianyang Pan , Jean Karim Zinzindohoue
  
  SP '17 38th IEEE Symposium on Security and Privacy | May 2017
  
  Publication Publication Project
- Everest: Towards a Verified, Drop-In Replacement of HTTPS
  
  Karthikeyan Bhargavan, Barry Bond, Antoine Delignat-Lavaud, Cédric Fournet, Chris Hawblitzel, Catalin Hritcu, Samin Ishtiaq, Markulf Kohlweiss, Rustan Leino, Jay Lorch, Kenji Maillard, Jinyang Pang, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella-Béguelin, Jean-Karim Zinzindohoué
  
  SNAPL 2017 - 2nd Summit on Advances in Programming Languages | May 2017
  
  Publication Publication Publication Project
- Verified Low-Level Programming Embedded in F*
  
  Jonathan Protzenko, Jean Karim Zinzindohoue, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud, Cătălin Hriţcu, Karthikeyan Bhargavan, Cédric Fournet, Nikhil Swamy
  
  22nd International Conference on Functional Programming (ICFP 2017) | May 2017
  
  Publication Publication Publication Github Access Project Project
- Formal Verification of Smart Contracts: Short Paper
  
  Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Anitha Gollamudi, Georges Gonthier, Nadim Kobeissi, Natalia Kulatova, Aseem Rastogi, Thomas Sibut-Pinote, Nikhil Swamy, Santiago Zanella-Béguelin
  
  PLAS '16 Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security | October 2016
  
  ISBN: 978-1-4503-4574-3
  
  Publication Publication Publication
- Towards a Provably Secure Implementation of TLS 1.3
  
  Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Jonathan Protzenko, Nikhil Swamy, Santiago Zanella-Béguelin
  
  TRON Workshop | July 2016
  
  Publication Project
- Downgrade Resilience in Key-Exchange Protocols
  
  Karthikeyan Bhargavan, Christina Brzuska, Cédric Fournet, Matthew Green, Markulf Kohlweiss, Santiago Zanella-Béguelin
  
  2016 IEEE Symposium on Security and Privacy | May 2016
  
  Publication Publication Publication
- Dependent Types and Multi-Monadic Effects in F*
  
  Nikhil Swamy, Cătălin Hriţcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoue, Santiago Zanella-Béguelin
  
  POPL '16 Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | January 2016
  
  ISBN: 978-1-4503-3549-2
  
  Publication Publication Publication
- Proving the TLS Handshake Secure (As It Is)
  
  Karthikeyan Bhargavan, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, Santiago Zanella-Béguelin, Cédric Fournet
  
  Advances in Cryptology -- CRYPTO 2014 | July 2014
  
  Publication Publication
- Probabilistic Relational Verification for Cryptographic Implementations
  
  Gilles Barthe, Cédric Fournet, Benjamin Grégoire, Pierre-Yves Strub, Santiago Zanella-Béguelin, Nikhil Swamy
  
  41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014 | January 2014
  
  To appear
  
  Publication Publication
- Verified Indifferentiable Hashing into Elliptic Curves
  
  Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Federico Olmedo, Santiago Zanella-Béguelin
  
  Journal of Computer Security | December 2013, Vol 21(6): pp. 881-917
  
  Accepted pending minor revisions
  
  Publication Publication
- Probabilistic Relational Reasoning for Differential Privacy
  
  Gilles Barthe, Boris Koepf, Federico Olmedo, Santiago Zanella-Béguelin
  
  ACM Trans. Program. Lang. Syst. | November 2013, Vol 35
  
  Publication Publication
- Fully Automated Analysis of Padding-Based Encryption in the Computational Model
  
  Gilles Barthe, Juan Manuel Crespo, César Kunz, Benedikt Schmidt, Benjamin Grégoire, Yassine Lakhnech, Santiago Zanella-Béguelin
  
  20th ACM Conference on Computer and Communications Security, CCS 2013 | January 2013
  
  Publication Publication
- Smart Meter Aggregation via Secret-Sharing
  
  George Danezis, Cédric Fournet, Markulf Kohlweiss, Santiago Zanella-Béguelin
  
  2013 Smart Energy Grid Security Workshop, SEGS 2013 | January 2013
  
  To appear
  
  Publication
- Verified Computational Differential Privacy with Applications to Smart Metering
  
  Benjamin Grégoire, César Kunz, Santiago Zanella-Béguelin, Gilles Barthe, George Danezis,
  
  26th IEEE Computer Security Foundations Symposium, CSF 2013 | January 2013
  
  Publication
- Automated Analysis and Synthesis of Padding-Based Encryption Schemes
  
  Gilles Barthe, Santiago Zanella-Béguelin, Juan Manuel Crespo, César Kunz, Yassine Lakhnech, Benjamin Grégoire
  
  December 2012
  
  IACR Cryptology ePrint Archive 2012
  
  Publication Publication
- Fully Automated Analysis of Padding-Based Encryption in the Computational Model
  
  Gilles Barthe, Juan Manuel Crespo, César Kunz, Benjamin Grégoire, Yassine Lakhnech, Santiago Zanella-Béguelin
  
  MSR-TR-2012-128 | December 2012
  
  IACR Cryptology ePrint Archive 2012
  
  Publication Publication
- Probabilistic Relational Verification for Cryptographic Implementations
  
  Benjamin Gregoire, Pierre-Yves Strub, Nikhil Swamy, Santiago Zanella-Béguelin, Gilles Barthe, Cédric Fournet
  
  November 2012
  
  Publication
- Automation in Computer-Aided Cryptography: proofs, attacks and designs
  
  Gilles Barthe, Benjamin Grégoire, César Kunz, Yassine Lakhnech, Santiago Zanella-Béguelin
  
  2nd International Conference on Certified Programs and Proofs, CPP 2012 | April 2012
  
  Publication Publication
- Computer-Aided Cryptographic Proofs
  
  Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Santiago Zanella-Béguelin
  
  3rd International Conference on Interactive Theorem Proving, ITP 2012 | January 2012
  
  Publication Publication
- Computer-Aided Cryptographic Proofs
  
  Gilles Barthe, Benjamin Grégoire, Santiago Zanella-Béguelin
  
  19th International Symposium on Static Analysis, SAS 2012 | January 2012
  
  Publication Publication
- Full Proof Cryptography: Verifiable Compilation of Efficient Zero-Knowledge Protocols
  
  José Bacelar Almeida, Manuel Barbosa, Endre Bangerter, Gilles Barthe, Stephen Krenn, Santiago Zanella-Béguelin
  
  19th ACM Conference on Computer and Communications Security, CCS 2012 | January 2012
  
  19th ACM Conference on Computer and Communications Security, CCS 2012
  
  Publication Publication
- Probabilistic Reasoning for Differential Privacy
  
  Gilles Barthe, Boris Köpf, Federico Olmedo, Santiago Zanella-Béguelin
  
  39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012 | January 2012
  
  Publication Publication
- Probabilistic Relational Hoare Logics for Computer-Aided Security Proofs
  
  Gilles Barthe, Benjamin Grégoire, Santiago Zanella-Béguelin
  
  11th International Conference on Mathematics of Program Construction, MPC 2012 | January 2012
  
  Publication Publication
- Verified Security of Merkle-DamgÃ¥rd
  
  Michael Backes, Gilles Barthe, Matthias Berg, Benjamin Grégoire, César Kunz, Malte Skoruppa, Santiago Zanella-Béguelin
  
  25th IEEE Computer Security Foundations Symposium, CSF 2012 | January 2012
  
  Publication Publication
- Verified Security of Redundancy-Free Encryption from Rabin and RSA
  
  Gilles Barthe, David Pointcheval, Santiago Zanella-Béguelin
  
  19th ACM Conference on Computer and Communications Security, CCS 2012 | January 2012
  
  Publication Publication
- Beyond Provable Security. Verifiable IND-CCA Security of OAEP
  
  Gilles Barthe, Benjamin Grégoire, Yassine Lakhnech, Santiago Zanella-Béguelin
  
  Topics in Cryptology, CT-RSA 2011 | January 2011
  
  ISBN: 978-3-642-19073-5
  
  Publication Publication Publication
- Computer-Aided Security Proofs for the Working Cryptographer
  
  Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Santiago Zanella-Béguelin
  
  Advances in Cryptology, CRYPTO 2011 | January 2011
  
  ISBN: 978-3-642-22791-2
  
  Best Paper Award
  
  Publication Publication Publication
- Formal Certification of Code-Based Cryptographic Proofs
  
  Gilles Barthe, Benjamin Grégoire, Santiago Zanella-Béguelin
  
  January 2011
  
  Publication
- Verifiable Security of Boneh-Franklin Identity-Based Encryption
  
  Gilles Barthe, Federico Olmedo, Santiago Zanella-Béguelin
  
  5th International Conference on Provable Security, ProvSec 2011 | January 2011
  
  Publication Publication
- Formal Certification of Game-Based Cryptographic Proofs
  
  Santiago Zanella-Béguelin
  
  December 2010
  
  December 2010
  
  EAPLS Best PhD Dissertation Award
  
  Publication Publication
- A Machine-Checked Formalization of Sigma-Protocols
  
  Gilles Barthe, Daniel Hedin, Santiago Zanella-Béguelin, Benjamin Grégoire, Sylvain Heraud
  
  23rd IEEE Computer Security Foundations Symposium, CSF 2010 | January 2010
  
  23rd IEEE Computer Security Foundations Symposium, CSF 2010
  
  Publication Publication
- Programming Language Techniques for Cryptographic Proofs
  
  Gilles Barthe, Benjamin Grégoire, Santiago Zanella-Béguelin
  
  1st International Conference on Interactive Theorem Proving, ITP 2010 | January 2010
  
  Publication Publication
- Formal Certification of Code-Based Cryptographic Proofs
  
  Gilles Barthe, Benjamin Grégoire, Santiago Zanella-Béguelin
  
  36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009 | January 2009
  
  ISBN: 978-1-60558-379-2
  
  Publication Publication
- Formal certification of ElGamal encryption. A gentle introduction to CertiCrypt
  
  Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Santiago Zanella-Béguelin
  
  5th International Workshop on Formal Aspects in Security and Trust, FAST 2008 | January 2009
  
  5th International Workshop on Formal Aspects in Security and Trust, FAST 2008
  
  ISBN: 978-3-642-01464-2
  
  Publication Publication
- Formally Certifying the Security of Digital Signature Schemes
  
  Santiago Zanella-Béguelin, Benjamin Grégoire, Gilles Barthe, Federico Olmedo
  
  30th IEEE Symposium on Security and Privacy, S&P 2009 | January 2009
  
  Publication Publication
- A Formal Specification of the MIDP 2.0 Security Model
  
  Santiago Zanella-Béguelin, Gustavo Betarte, Carlos Luna
  
  4th International Workshop on Formal Aspects in Security and Trust, FAST 2006 | January 2006
  
  ISBN: 978-3-540-75226-4
  
  Publication Publication
- Formalisation and Verification of the GlobalPlatform Card Specification Using the B Method
  
  Santiago Zanella-Béguelin
  
  2nd International Workshop on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, CASSIS 2005 | January 2006
  
  2nd International Workshop on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, CASSIS 2005
  
  Publication Publication

- Project Everest: Perspectives from Developing Industrial-Grade High-Assurance Software
  
  D. Ahman, Karthik Bhargavan, Barry Bond, Jay Bosamiya, Chris Brzuska, Antoine Delignat-Lavaud, Cédric Fournet, Aymeric Fromherz, Sydney Gibson, Chris Hawblitzel, Cătălin Hrițcu, Markulf Kohlweiss, Guido Martínez, Haobin Ni, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Exequiel Rivas, Nikhil Swamy, Santiago Zanella-Béguelin
  
  ACM Transactions on Programming Languages and Systems | April 2026
  
  DOI
- HACL×N: Verified Generic SIMD Crypto (for all your favourite platforms)
  
  Marina Polubelova, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin Beurdouche, Aymeric Fromherz, Natalia Kulatova, Santiago Zanella-Béguelin
  
  ACM Conference on Computer and Communications Security (CCS) | November 2020
  
  Publication Access Project
- EverCrypt: A Fast, Veriﬁed, Cross-Platform Cryptographic Provider
  
  Jonathan Protzenko, Bryan Parno, Aymeric Fromherz, Chris Hawblitzel, Marina Polubelova, Karthikeyan Bhargavan, Benjamin Beurdouche, Joonwon Choi, Antoine Delignat-Lavaud, Cédric Fournet, Natalia Kulatova, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Christoph M. Wintersteiger, Santiago Zanella-Béguelin
  
  IEEE Symposium on Security and Privacy | May 2020
  
  Publication Video Access Github Project
- A monadic framework for relational verification: applied to information security, program equivalence, and optimizations
  
  Niklas Grimm, Kenji Maillard, Cédric Fournet, Catalin Hritcu, Matteo Maffei, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Santiago Zanella-Béguelin
  
  CPP 2018 | January 2018
  
  Publication Publication Publication Project
- Implementing and Proving the TLS 1.3 Record Layer
  
  Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy, Santiago Zanella-Béguelin, Karthikeyan Bhargavan , Jianyang Pan , Jean Karim Zinzindohoue
  
  SP '17 38th IEEE Symposium on Security and Privacy | May 2017
  
  Publication Publication Project
- Everest: Towards a Verified, Drop-In Replacement of HTTPS
  
  Karthikeyan Bhargavan, Barry Bond, Antoine Delignat-Lavaud, Cédric Fournet, Chris Hawblitzel, Catalin Hritcu, Samin Ishtiaq, Markulf Kohlweiss, Rustan Leino, Jay Lorch, Kenji Maillard, Jinyang Pang, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella-Béguelin, Jean-Karim Zinzindohoué
  
  SNAPL 2017 - 2nd Summit on Advances in Programming Languages | May 2017
  
  Publication Publication Publication Project
- Verified Low-Level Programming Embedded in F*
  
  Jonathan Protzenko, Jean Karim Zinzindohoue, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud, Cătălin Hriţcu, Karthikeyan Bhargavan, Cédric Fournet, Nikhil Swamy
  
  22nd International Conference on Functional Programming (ICFP 2017) | May 2017
  
  Publication Publication Publication Github Access Project Project
- Formal Verification of Smart Contracts: Short Paper
  
  Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Anitha Gollamudi, Georges Gonthier, Nadim Kobeissi, Natalia Kulatova, Aseem Rastogi, Thomas Sibut-Pinote, Nikhil Swamy, Santiago Zanella-Béguelin
  
  PLAS '16 Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security | October 2016
  
  ISBN: 978-1-4503-4574-3
  
  Publication Publication Publication
- Towards a Provably Secure Implementation of TLS 1.3
  
  Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Jonathan Protzenko, Nikhil Swamy, Santiago Zanella-Béguelin
  
  TRON Workshop | July 2016
  
  Publication Project
- Dependent Types and Multi-Monadic Effects in F*
  
  Nikhil Swamy, Cătălin Hriţcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoue, Santiago Zanella-Béguelin
  
  POPL '16 Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | January 2016
  
  ISBN: 978-1-4503-3549-2
  
  Publication Publication Publication
- Proving the TLS Handshake Secure (As It Is)
  
  Karthikeyan Bhargavan, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, Santiago Zanella-Béguelin, Cédric Fournet
  
  Advances in Cryptology -- CRYPTO 2014 | July 2014
  
  Publication Publication
- Probabilistic Relational Verification for Cryptographic Implementations
  
  Gilles Barthe, Cédric Fournet, Benjamin Grégoire, Pierre-Yves Strub, Santiago Zanella-Béguelin, Nikhil Swamy
  
  41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014 | January 2014
  
  To appear
  
  Publication Publication
- Probabilistic Relational Reasoning for Differential Privacy
  
  Gilles Barthe, Boris Koepf, Federico Olmedo, Santiago Zanella-Béguelin
  
  ACM Trans. Program. Lang. Syst. | November 2013, Vol 35
  
  Publication Publication
- Formalisation and Verification of the GlobalPlatform Card Specification Using the B Method
  
  Santiago Zanella-Béguelin
  
  2nd International Workshop on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, CASSIS 2005 | January 2006
  
  2nd International Workshop on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, CASSIS 2005
  
  Publication Publication
- Project Everest: Perspectives from Developing Industrial-Grade High-Assurance Software
  
  D. Ahman, Karthik Bhargavan, Barry Bond, Jay Bosamiya, Chris Brzuska, Antoine Delignat-Lavaud, Cédric Fournet, Aymeric Fromherz, Sydney Gibson, Chris Hawblitzel, Cătălin Hrițcu, Markulf Kohlweiss, Guido Martínez, Haobin Ni, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Exequiel Rivas, Nikhil Swamy, Santiago Zanella-Béguelin
  
  ACM Transactions on Programming Languages and Systems | April 2026
  
  DOI
- Permissive Information-Flow Analysis for Large Language Models
  
  Shoaib Ahmed Siddiqui, Radhika Gaonkar, Boris Köpf, David Krueger, Andrew Paverd, Ahmed Salem, Shruti Tople, Lukas Wutschitz, Menglin Xia, Santiago Zanella-Béguelin
  
  Transactions on Machine Learning Research (TMLR) | October 2025
  
  Publication Publication Project
- Securing AI Agents with Information-Flow Control
  
  Manuel Costa, Boris Köpf, Aashish Kolluri, Andrew Paverd, Mark Russinovich, Ahmed Salem, Shruti Tople, Lukas Wutschitz, Santiago Zanella-Béguelin
  
  May 2025
  
  DOI Publication Publication Project Project
- The Canary’s Echo: Auditing Privacy Risks of LLM-Generated Synthetic Text
  
  Matthieu Meeus, Lukas Wutschitz, Santiago Zanella-Béguelin, Reza Shokri, Shruti Tople
  
  February 2025
  
  DOI Preprint Project
- Closed-Form Bounds for DP-SGD against Record-level Inference
  
  Giovanni Cherubin, Boris Köpf, Andrew Paverd, Shruti Tople, Lukas Wutschitz, Santiago Zanella-Béguelin
  
  USENIX Security Symposium | August 2024
  
  Publication Project
- Dataset and Lessons Learned from the 2024 SaTML LLM Capture-the-Flag Competition
  
  Edoardo Debenedetti, Javier Rando, Daniel Paleka, Fineas Silaghi, Dragos Albastroiu, Niv Cohen, Yuval Lemberg, Reshmi Ghosh, Ahmed Salem, Rui Wen, Giovanni Cherubin, Santiago Zanella-Béguelin, Robin Schmid, Victor Klemm, Takahiro Miki, Chenhao Li, Stefan Kraft, Mario Fritz, Florian Tramer, Sahar Abdelnabi, Lea Schönherr
  
  NeurIPS 2024 | June 2024
  
  Preprint Project
- On the Efficacy of Differentially Private Few-shot Image Classification
  
  Marlon Tobaben, Aliaksandra Shysheya, John Bronskill, Andrew Paverd, Shruti Tople, Santiago Zanella-Béguelin, Richard Turner, Antti Honkela
  
  Transactions on Machine Learning Research | December 2023, Vol 2023
  
  DOI Preprint Preprint Publication Project
- Bayesian Estimation of Differential Privacy
  
  Santiago Zanella-Béguelin, Lukas Wutschitz, Shruti Tople, Ahmed Salem, Victor Ruehle, Andrew Paverd, Mohammad Naseri, Boris Köpf, Daniel Jones
  
  2023 International Conference on Machine Learning | July 2023
  
  Editor(s): Barbara Engelhardt, Emma Brunskill, Kyunghyun Cho
  
  Publication Project
- Analyzing Leakage of Personally Identifiable Information in Language Models
  
  Nils Lukas, Ahmed Salem, Robert Sim, Shruti Tople, Lukas Wutschitz, Santiago Zanella-Béguelin
  
  2023 IEEE Symposium on Security and Privacy | May 2023
  
  Publication PDF DOI Project
- SoK: Let the Privacy Games Begin! A Unified Treatment of Data Inference Privacy in Machine Learning
  
  Ahmed Salem, Giovanni Cherubin, David Evans, Boris Köpf, Andrew Paverd, Anshuman Suri, Shruti Tople, Santiago Zanella-Béguelin
  
  2023 IEEE Symposium on Security and Privacy | May 2023
  
  Publication PDF DOI Project
- Grey-box Extraction of Natural Language Models
  
  Santiago Zanella-Béguelin, Shruti Tople, Andrew Paverd, Boris Köpf
  
  International Conference on Machine Learning | July 2021
  
  Editor(s): Marina Meila and Tong Zhang
  
  PDF Project
- HACL×N: Verified Generic SIMD Crypto (for all your favourite platforms)
  
  Marina Polubelova, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin Beurdouche, Aymeric Fromherz, Natalia Kulatova, Santiago Zanella-Béguelin
  
  ACM Conference on Computer and Communications Security (CCS) | November 2020
  
  Publication Access Project
- Analyzing Information Leakage of Updates to Natural Language Models
  
  Santiago Zanella-Béguelin, Lukas Wutschitz, Shruti Tople, Victor Ruehle, Andrew Paverd, Olga Ohrimenko, Boris Köpf, Marc Brockschmidt
  
  ACM Conference on Computer and Communication Security (CCS) | November 2020
  
  Author's Version Project
- EverCrypt: A Fast, Veriﬁed, Cross-Platform Cryptographic Provider
  
  Jonathan Protzenko, Bryan Parno, Aymeric Fromherz, Chris Hawblitzel, Marina Polubelova, Karthikeyan Bhargavan, Benjamin Beurdouche, Joonwon Choi, Antoine Delignat-Lavaud, Cédric Fournet, Natalia Kulatova, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Christoph M. Wintersteiger, Santiago Zanella-Béguelin
  
  IEEE Symposium on Security and Privacy | May 2020
  
  Publication Video Access Github Project
- Imperfect forward secrecy: how Diffie-Hellman fails in practice
  
  David Adrian, Karthik Bhargavan, Zakir Durumeric, Pierrick Gaudry, Matthew Green, J. Alex Halderman, Nadia Heninger, Drew Springall, Emmanuel Thomé, Luke Valenta, Benjamin VanderSloot, Eric Wustrow, Santiago Zanella-Béguelin, Paul Zimmermann
  
  Communications of The ACM | December 2018, Vol 62(1): pp. 106-114
  
  PDF DOI
- Implementing and Proving the TLS 1.3 Record Layer
  
  Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy, Santiago Zanella-Béguelin, Karthikeyan Bhargavan , Jianyang Pan , Jean Karim Zinzindohoue
  
  SP '17 38th IEEE Symposium on Security and Privacy | May 2017
  
  Publication Publication Project
- Everest: Towards a Verified, Drop-In Replacement of HTTPS
  
  Karthikeyan Bhargavan, Barry Bond, Antoine Delignat-Lavaud, Cédric Fournet, Chris Hawblitzel, Catalin Hritcu, Samin Ishtiaq, Markulf Kohlweiss, Rustan Leino, Jay Lorch, Kenji Maillard, Jinyang Pang, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella-Béguelin, Jean-Karim Zinzindohoué
  
  SNAPL 2017 - 2nd Summit on Advances in Programming Languages | May 2017
  
  Publication Publication Publication Project
- Verified Low-Level Programming Embedded in F*
  
  Jonathan Protzenko, Jean Karim Zinzindohoue, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud, Cătălin Hriţcu, Karthikeyan Bhargavan, Cédric Fournet, Nikhil Swamy
  
  22nd International Conference on Functional Programming (ICFP 2017) | May 2017
  
  Publication Publication Publication Github Access Project Project
- Downgrade Resilience in Key-Exchange Protocols
  
  Karthikeyan Bhargavan, Christina Brzuska, Cédric Fournet, Matthew Green, Markulf Kohlweiss, Santiago Zanella-Béguelin
  
  2016 IEEE Symposium on Security and Privacy | May 2016
  
  Publication Publication Publication
- Proving the TLS Handshake Secure (As It Is)
  
  Karthikeyan Bhargavan, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, Santiago Zanella-Béguelin, Cédric Fournet
  
  Advances in Cryptology -- CRYPTO 2014 | July 2014
  
  Publication Publication
- Smart Meter Aggregation via Secret-Sharing
  
  George Danezis, Cédric Fournet, Markulf Kohlweiss, Santiago Zanella-Béguelin
  
  2013 Smart Energy Grid Security Workshop, SEGS 2013 | January 2013
  
  To appear
  
  Publication
- Fully Automated Analysis of Padding-Based Encryption in the Computational Model
  
  Gilles Barthe, Juan Manuel Crespo, César Kunz, Benedikt Schmidt, Benjamin Grégoire, Yassine Lakhnech, Santiago Zanella-Béguelin
  
  20th ACM Conference on Computer and Communications Security, CCS 2013 | January 2013
  
  Publication Publication
- Automated Analysis and Synthesis of Padding-Based Encryption Schemes
  
  Gilles Barthe, Santiago Zanella-Béguelin, Juan Manuel Crespo, César Kunz, Yassine Lakhnech, Benjamin Grégoire
  
  December 2012
  
  IACR Cryptology ePrint Archive 2012
  
  Publication Publication
- Fully Automated Analysis of Padding-Based Encryption in the Computational Model
  
  Gilles Barthe, Juan Manuel Crespo, César Kunz, Benjamin Grégoire, Yassine Lakhnech, Santiago Zanella-Béguelin
  
  MSR-TR-2012-128 | December 2012
  
  IACR Cryptology ePrint Archive 2012
  
  Publication Publication
- Probabilistic Relational Verification for Cryptographic Implementations
  
  Benjamin Gregoire, Pierre-Yves Strub, Nikhil Swamy, Santiago Zanella-Béguelin, Gilles Barthe, Cédric Fournet
  
  November 2012
  
  Publication
- Automation in Computer-Aided Cryptography: proofs, attacks and designs
  
  Gilles Barthe, Benjamin Grégoire, César Kunz, Yassine Lakhnech, Santiago Zanella-Béguelin
  
  2nd International Conference on Certified Programs and Proofs, CPP 2012 | April 2012
  
  Publication Publication
- Full Proof Cryptography: Verifiable Compilation of Efficient Zero-Knowledge Protocols
  
  José Bacelar Almeida, Manuel Barbosa, Endre Bangerter, Gilles Barthe, Stephen Krenn, Santiago Zanella-Béguelin
  
  19th ACM Conference on Computer and Communications Security, CCS 2012 | January 2012
  
  19th ACM Conference on Computer and Communications Security, CCS 2012
  
  Publication Publication
- Probabilistic Relational Hoare Logics for Computer-Aided Security Proofs
  
  Gilles Barthe, Benjamin Grégoire, Santiago Zanella-Béguelin
  
  11th International Conference on Mathematics of Program Construction, MPC 2012 | January 2012
  
  Publication Publication
- Probabilistic Reasoning for Differential Privacy
  
  Gilles Barthe, Boris Köpf, Federico Olmedo, Santiago Zanella-Béguelin
  
  39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012 | January 2012
  
  Publication Publication
- Beyond Provable Security. Verifiable IND-CCA Security of OAEP
  
  Gilles Barthe, Benjamin Grégoire, Yassine Lakhnech, Santiago Zanella-Béguelin
  
  Topics in Cryptology, CT-RSA 2011 | January 2011
  
  ISBN: 978-3-642-19073-5
  
  Publication Publication Publication
- Computer-Aided Security Proofs for the Working Cryptographer
  
  Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Santiago Zanella-Béguelin
  
  Advances in Cryptology, CRYPTO 2011 | January 2011
  
  ISBN: 978-3-642-22791-2
  
  Best Paper Award
  
  Publication Publication Publication
- Formal Certification of Code-Based Cryptographic Proofs
  
  Gilles Barthe, Benjamin Grégoire, Santiago Zanella-Béguelin
  
  January 2011
  
  Publication
- Formal Certification of Game-Based Cryptographic Proofs
  
  Santiago Zanella-Béguelin
  
  December 2010
  
  December 2010
  
  EAPLS Best PhD Dissertation Award
  
  Publication Publication
- Programming Language Techniques for Cryptographic Proofs
  
  Gilles Barthe, Benjamin Grégoire, Santiago Zanella-Béguelin
  
  1st International Conference on Interactive Theorem Proving, ITP 2010 | January 2010
  
  Publication Publication
- Formal Certification of Code-Based Cryptographic Proofs
  
  Gilles Barthe, Benjamin Grégoire, Santiago Zanella-Béguelin
  
  36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009 | January 2009
  
  ISBN: 978-1-60558-379-2
  
  Publication Publication
- Formal certification of ElGamal encryption. A gentle introduction to CertiCrypt
  
  Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Santiago Zanella-Béguelin
  
  5th International Workshop on Formal Aspects in Security and Trust, FAST 2008 | January 2009
  
  5th International Workshop on Formal Aspects in Security and Trust, FAST 2008
  
  ISBN: 978-3-642-01464-2
  
  Publication Publication
- Formally Certifying the Security of Digital Signature Schemes
  
  Santiago Zanella-Béguelin, Benjamin Grégoire, Gilles Barthe, Federico Olmedo
  
  30th IEEE Symposium on Security and Privacy, S&P 2009 | January 2009
  
  Publication Publication
- A Formal Specification of the MIDP 2.0 Security Model
  
  Santiago Zanella-Béguelin, Gustavo Betarte, Carlos Luna
  
  4th International Workshop on Formal Aspects in Security and Trust, FAST 2006 | January 2006
  
  ISBN: 978-3-540-75226-4
  
  Publication Publication
- Optimizing Agent Planning for Security and Autonomy
  
  Aashish Kolluri, Rishi Sharma, Manuel Costa, Boris Köpf, Tobias Niessen, Mark Russinovich, Shruti Tople, Santiago Zanella-Béguelin
  
  ICLR 2026 | February 2026
  
  Publication Preprint Project
- Beyond Membership: Limitations of Add/Remove Adjacency in Differential Privacy
  
  Gauri Pradhan, Joonas Jälkö, Santiago Zanella-Béguelin, Antti Honkela
  
  ICLR 2026 | November 2025
  
  DOI Publication
- Permissive Information-Flow Analysis for Large Language Models
  
  Shoaib Ahmed Siddiqui, Radhika Gaonkar, Boris Köpf, David Krueger, Andrew Paverd, Ahmed Salem, Shruti Tople, Lukas Wutschitz, Menglin Xia, Santiago Zanella-Béguelin
  
  Transactions on Machine Learning Research (TMLR) | October 2025
  
  Publication Publication Project
- Securing AI Agents with Information-Flow Control
  
  Manuel Costa, Boris Köpf, Aashish Kolluri, Andrew Paverd, Mark Russinovich, Ahmed Salem, Shruti Tople, Lukas Wutschitz, Santiago Zanella-Béguelin
  
  May 2025
  
  DOI Publication Publication Project Project
- The Canary’s Echo: Auditing Privacy Risks of LLM-Generated Synthetic Text
  
  Matthieu Meeus, Lukas Wutschitz, Santiago Zanella-Béguelin, Reza Shokri, Shruti Tople
  
  February 2025
  
  DOI Preprint Project
- The Canary’s Echo: Auditing Privacy Risks of LLM-Generated Synthetic Text
  
  Matthieu Meeus, Lukas Wutschitz, Santiago Zanella-Béguelin, Shruti Tople, Reza Shokri
  
  ICML 2025 | February 2025
  
  DOI Publication Publication
- Closed-Form Bounds for DP-SGD against Record-level Inference
  
  Giovanni Cherubin, Boris Köpf, Andrew Paverd, Shruti Tople, Lukas Wutschitz, Santiago Zanella-Béguelin
  
  USENIX Security Symposium | August 2024
  
  Publication Project
- Dataset and Lessons Learned from the 2024 SaTML LLM Capture-the-Flag Competition
  
  Edoardo Debenedetti, Javier Rando, Daniel Paleka, Fineas Silaghi, Dragos Albastroiu, Niv Cohen, Yuval Lemberg, Reshmi Ghosh, Ahmed Salem, Rui Wen, Giovanni Cherubin, Santiago Zanella-Béguelin, Robin Schmid, Victor Klemm, Takahiro Miki, Chenhao Li, Stefan Kraft, Mario Fritz, Florian Tramer, Sahar Abdelnabi, Lea Schönherr
  
  NeurIPS 2024 | June 2024
  
  Preprint Project
- On the Efficacy of Differentially Private Few-shot Image Classification
  
  Marlon Tobaben, Aliaksandra Shysheya, John Bronskill, Andrew Paverd, Shruti Tople, Santiago Zanella-Béguelin, Richard Turner, Antti Honkela
  
  Transactions on Machine Learning Research | December 2023, Vol 2023
  
  DOI Preprint Preprint Publication Project
- Bayesian Estimation of Differential Privacy
  
  Santiago Zanella-Béguelin, Lukas Wutschitz, Shruti Tople, Ahmed Salem, Victor Ruehle, Andrew Paverd, Mohammad Naseri, Boris Köpf, Daniel Jones
  
  2023 International Conference on Machine Learning | July 2023
  
  Editor(s): Barbara Engelhardt, Emma Brunskill, Kyunghyun Cho
  
  Publication Project
- Analyzing Leakage of Personally Identifiable Information in Language Models
  
  Nils Lukas, Ahmed Salem, Robert Sim, Shruti Tople, Lukas Wutschitz, Santiago Zanella-Béguelin
  
  2023 IEEE Symposium on Security and Privacy | May 2023
  
  Publication PDF DOI Project
- SoK: Let the Privacy Games Begin! A Unified Treatment of Data Inference Privacy in Machine Learning
  
  Ahmed Salem, Giovanni Cherubin, David Evans, Boris Köpf, Andrew Paverd, Anshuman Suri, Shruti Tople, Santiago Zanella-Béguelin
  
  2023 IEEE Symposium on Security and Privacy | May 2023
  
  Publication PDF DOI Project
- Grey-box Extraction of Natural Language Models
  
  Santiago Zanella-Béguelin, Shruti Tople, Andrew Paverd, Boris Köpf
  
  International Conference on Machine Learning | July 2021
  
  Editor(s): Marina Meila and Tong Zhang
  
  PDF Project
- Analyzing Information Leakage of Updates to Natural Language Models
  
  Santiago Zanella-Béguelin, Lukas Wutschitz, Shruti Tople, Victor Ruehle, Andrew Paverd, Olga Ohrimenko, Boris Köpf, Marc Brockschmidt
  
  ACM Conference on Computer and Communication Security (CCS) | November 2020
  
  Author's Version Project
- EverCrypt: A Fast, Veriﬁed, Cross-Platform Cryptographic Provider
  
  Jonathan Protzenko, Bryan Parno, Aymeric Fromherz, Chris Hawblitzel, Marina Polubelova, Karthikeyan Bhargavan, Benjamin Beurdouche, Joonwon Choi, Antoine Delignat-Lavaud, Cédric Fournet, Natalia Kulatova, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Christoph M. Wintersteiger, Santiago Zanella-Béguelin
  
  IEEE Symposium on Security and Privacy | May 2020
  
  Publication Video Access Github Project
- Verified Indifferentiable Hashing into Elliptic Curves
  
  Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Federico Olmedo, Santiago Zanella-Béguelin
  
  Journal of Computer Security | December 2013, Vol 21(6): pp. 881-917
  
  Accepted pending minor revisions
  
  Publication Publication
- Verified Computational Differential Privacy with Applications to Smart Metering
  
  Benjamin Grégoire, César Kunz, Santiago Zanella-Béguelin, Gilles Barthe, George Danezis,
  
  26th IEEE Computer Security Foundations Symposium, CSF 2013 | January 2013
  
  Publication
- Verified Security of Redundancy-Free Encryption from Rabin and RSA
  
  Gilles Barthe, David Pointcheval, Santiago Zanella-Béguelin
  
  19th ACM Conference on Computer and Communications Security, CCS 2012 | January 2012
  
  Publication Publication
- Verified Security of Merkle-DamgÃ¥rd
  
  Michael Backes, Gilles Barthe, Matthias Berg, Benjamin Grégoire, César Kunz, Malte Skoruppa, Santiago Zanella-Béguelin
  
  25th IEEE Computer Security Foundations Symposium, CSF 2012 | January 2012
  
  Publication Publication
- Verifiable Security of Boneh-Franklin Identity-Based Encryption
  
  Gilles Barthe, Federico Olmedo, Santiago Zanella-Béguelin
  
  5th International Conference on Provable Security, ProvSec 2011 | January 2011
  
  Publication Publication
- Computer-Aided Cryptographic Proofs
  
  Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Santiago Zanella-Béguelin
  
  3rd International Conference on Interactive Theorem Proving, ITP 2012 | January 2012
  
  Publication Publication
- Computer-Aided Cryptographic Proofs
  
  Gilles Barthe, Benjamin Grégoire, Santiago Zanella-Béguelin
  
  19th International Symposium on Static Analysis, SAS 2012 | January 2012
  
  Publication Publication
- A Machine-Checked Formalization of Sigma-Protocols
  
  Gilles Barthe, Daniel Hedin, Santiago Zanella-Béguelin, Benjamin Grégoire, Sylvain Heraud
  
  23rd IEEE Computer Security Foundations Symposium, CSF 2010 | January 2010
  
  23rd IEEE Computer Security Foundations Symposium, CSF 2010
  
  Publication Publication

- Project Everest: Perspectives from Developing Industrial-Grade High-Assurance Software
  
  D. Ahman, Karthik Bhargavan, Barry Bond, Jay Bosamiya, Chris Brzuska, Antoine Delignat-Lavaud, Cédric Fournet, Aymeric Fromherz, Sydney Gibson, Chris Hawblitzel, Cătălin Hrițcu, Markulf Kohlweiss, Guido Martínez, Haobin Ni, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Exequiel Rivas, Nikhil Swamy, Santiago Zanella-Béguelin
  
  ACM Transactions on Programming Languages and Systems | April 2026
  
  DOI
- Permissive Information-Flow Analysis for Large Language Models
  
  Shoaib Ahmed Siddiqui, Radhika Gaonkar, Boris Köpf, David Krueger, Andrew Paverd, Ahmed Salem, Shruti Tople, Lukas Wutschitz, Menglin Xia, Santiago Zanella-Béguelin
  
  Transactions on Machine Learning Research (TMLR) | October 2025
  
  Publication Publication Project
- On the Efficacy of Differentially Private Few-shot Image Classification
  
  Marlon Tobaben, Aliaksandra Shysheya, John Bronskill, Andrew Paverd, Shruti Tople, Santiago Zanella-Béguelin, Richard Turner, Antti Honkela
  
  Transactions on Machine Learning Research | December 2023, Vol 2023
  
  DOI Preprint Preprint Publication Project
- Imperfect forward secrecy: how Diffie-Hellman fails in practice
  
  David Adrian, Karthik Bhargavan, Zakir Durumeric, Pierrick Gaudry, Matthew Green, J. Alex Halderman, Nadia Heninger, Drew Springall, Emmanuel Thomé, Luke Valenta, Benjamin VanderSloot, Eric Wustrow, Santiago Zanella-Béguelin, Paul Zimmermann
  
  Communications of The ACM | December 2018, Vol 62(1): pp. 106-114
  
  PDF DOI
- Verified Indifferentiable Hashing into Elliptic Curves
  
  Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Federico Olmedo, Santiago Zanella-Béguelin
  
  Journal of Computer Security | December 2013, Vol 21(6): pp. 881-917
  
  Accepted pending minor revisions
  
  Publication Publication
- Probabilistic Relational Reasoning for Differential Privacy
  
  Gilles Barthe, Boris Koepf, Federico Olmedo, Santiago Zanella-Béguelin
  
  ACM Trans. Program. Lang. Syst. | November 2013, Vol 35
  
  Publication Publication
- Optimizing Agent Planning for Security and Autonomy
  
  Aashish Kolluri, Rishi Sharma, Manuel Costa, Boris Köpf, Tobias Niessen, Mark Russinovich, Shruti Tople, Santiago Zanella-Béguelin
  
  ICLR 2026 | February 2026
  
  Publication Preprint Project
- Beyond Membership: Limitations of Add/Remove Adjacency in Differential Privacy
  
  Gauri Pradhan, Joonas Jälkö, Santiago Zanella-Béguelin, Antti Honkela
  
  ICLR 2026 | November 2025
  
  DOI Publication
- The Canary’s Echo: Auditing Privacy Risks of LLM-Generated Synthetic Text
  
  Matthieu Meeus, Lukas Wutschitz, Santiago Zanella-Béguelin, Shruti Tople, Reza Shokri
  
  ICML 2025 | February 2025
  
  DOI Publication Publication
- Closed-Form Bounds for DP-SGD against Record-level Inference
  
  Giovanni Cherubin, Boris Köpf, Andrew Paverd, Shruti Tople, Lukas Wutschitz, Santiago Zanella-Béguelin
  
  USENIX Security Symposium | August 2024
  
  Publication Project
- Dataset and Lessons Learned from the 2024 SaTML LLM Capture-the-Flag Competition
  
  Edoardo Debenedetti, Javier Rando, Daniel Paleka, Fineas Silaghi, Dragos Albastroiu, Niv Cohen, Yuval Lemberg, Reshmi Ghosh, Ahmed Salem, Rui Wen, Giovanni Cherubin, Santiago Zanella-Béguelin, Robin Schmid, Victor Klemm, Takahiro Miki, Chenhao Li, Stefan Kraft, Mario Fritz, Florian Tramer, Sahar Abdelnabi, Lea Schönherr
  
  NeurIPS 2024 | June 2024
  
  Preprint Project
- Bayesian Estimation of Differential Privacy
  
  Santiago Zanella-Béguelin, Lukas Wutschitz, Shruti Tople, Ahmed Salem, Victor Ruehle, Andrew Paverd, Mohammad Naseri, Boris Köpf, Daniel Jones
  
  2023 International Conference on Machine Learning | July 2023
  
  Editor(s): Barbara Engelhardt, Emma Brunskill, Kyunghyun Cho
  
  Publication Project
- Analyzing Leakage of Personally Identifiable Information in Language Models
  
  Nils Lukas, Ahmed Salem, Robert Sim, Shruti Tople, Lukas Wutschitz, Santiago Zanella-Béguelin
  
  2023 IEEE Symposium on Security and Privacy | May 2023
  
  Publication PDF DOI Project
- SoK: Let the Privacy Games Begin! A Unified Treatment of Data Inference Privacy in Machine Learning
  
  Ahmed Salem, Giovanni Cherubin, David Evans, Boris Köpf, Andrew Paverd, Anshuman Suri, Shruti Tople, Santiago Zanella-Béguelin
  
  2023 IEEE Symposium on Security and Privacy | May 2023
  
  Publication PDF DOI Project
- Grey-box Extraction of Natural Language Models
  
  Santiago Zanella-Béguelin, Shruti Tople, Andrew Paverd, Boris Köpf
  
  International Conference on Machine Learning | July 2021
  
  Editor(s): Marina Meila and Tong Zhang
  
  PDF Project
- HACL×N: Verified Generic SIMD Crypto (for all your favourite platforms)
  
  Marina Polubelova, Karthikeyan Bhargavan, Jonathan Protzenko, Benjamin Beurdouche, Aymeric Fromherz, Natalia Kulatova, Santiago Zanella-Béguelin
  
  ACM Conference on Computer and Communications Security (CCS) | November 2020
  
  Publication Access Project
- Analyzing Information Leakage of Updates to Natural Language Models
  
  Santiago Zanella-Béguelin, Lukas Wutschitz, Shruti Tople, Victor Ruehle, Andrew Paverd, Olga Ohrimenko, Boris Köpf, Marc Brockschmidt
  
  ACM Conference on Computer and Communication Security (CCS) | November 2020
  
  Author's Version Project
- EverCrypt: A Fast, Veriﬁed, Cross-Platform Cryptographic Provider
  
  Jonathan Protzenko, Bryan Parno, Aymeric Fromherz, Chris Hawblitzel, Marina Polubelova, Karthikeyan Bhargavan, Benjamin Beurdouche, Joonwon Choi, Antoine Delignat-Lavaud, Cédric Fournet, Natalia Kulatova, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Christoph M. Wintersteiger, Santiago Zanella-Béguelin
  
  IEEE Symposium on Security and Privacy | May 2020
  
  Publication Video Access Github Project
- A monadic framework for relational verification: applied to information security, program equivalence, and optimizations
  
  Niklas Grimm, Kenji Maillard, Cédric Fournet, Catalin Hritcu, Matteo Maffei, Jonathan Protzenko, Tahina Ramananandro, Aseem Rastogi, Nikhil Swamy, Santiago Zanella-Béguelin
  
  CPP 2018 | January 2018
  
  Publication Publication Publication Project
- Implementing and Proving the TLS 1.3 Record Layer
  
  Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Jonathan Protzenko, Aseem Rastogi, Nikhil Swamy, Santiago Zanella-Béguelin, Karthikeyan Bhargavan , Jianyang Pan , Jean Karim Zinzindohoue
  
  SP '17 38th IEEE Symposium on Security and Privacy | May 2017
  
  Publication Publication Project
- Everest: Towards a Verified, Drop-In Replacement of HTTPS
  
  Karthikeyan Bhargavan, Barry Bond, Antoine Delignat-Lavaud, Cédric Fournet, Chris Hawblitzel, Catalin Hritcu, Samin Ishtiaq, Markulf Kohlweiss, Rustan Leino, Jay Lorch, Kenji Maillard, Jinyang Pang, Bryan Parno, Jonathan Protzenko, Tahina Ramananandro, Ashay Rane, Aseem Rastogi, Nikhil Swamy, Laure Thompson, Peng Wang, Santiago Zanella-Béguelin, Jean-Karim Zinzindohoué
  
  SNAPL 2017 - 2nd Summit on Advances in Programming Languages | May 2017
  
  Publication Publication Publication Project
- Verified Low-Level Programming Embedded in F*
  
  Jonathan Protzenko, Jean Karim Zinzindohoue, Aseem Rastogi, Tahina Ramananandro, Peng Wang, Santiago Zanella-Béguelin, Antoine Delignat-Lavaud, Cătălin Hriţcu, Karthikeyan Bhargavan, Cédric Fournet, Nikhil Swamy
  
  22nd International Conference on Functional Programming (ICFP 2017) | May 2017
  
  Publication Publication Publication Github Access Project Project
- Formal Verification of Smart Contracts: Short Paper
  
  Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Anitha Gollamudi, Georges Gonthier, Nadim Kobeissi, Natalia Kulatova, Aseem Rastogi, Thomas Sibut-Pinote, Nikhil Swamy, Santiago Zanella-Béguelin
  
  PLAS '16 Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security | October 2016
  
  ISBN: 978-1-4503-4574-3
  
  Publication Publication Publication
- Towards a Provably Secure Implementation of TLS 1.3
  
  Antoine Delignat-Lavaud, Cédric Fournet, Markulf Kohlweiss, Jonathan Protzenko, Nikhil Swamy, Santiago Zanella-Béguelin
  
  TRON Workshop | July 2016
  
  Publication Project
- Downgrade Resilience in Key-Exchange Protocols
  
  Karthikeyan Bhargavan, Christina Brzuska, Cédric Fournet, Matthew Green, Markulf Kohlweiss, Santiago Zanella-Béguelin
  
  2016 IEEE Symposium on Security and Privacy | May 2016
  
  Publication Publication Publication
- Dependent Types and Multi-Monadic Effects in F*
  
  Nikhil Swamy, Cătălin Hriţcu, Chantal Keller, Aseem Rastogi, Antoine Delignat-Lavaud, Simon Forest, Karthikeyan Bhargavan, Cédric Fournet, Pierre-Yves Strub, Markulf Kohlweiss, Jean-Karim Zinzindohoue, Santiago Zanella-Béguelin
  
  POPL '16 Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages | January 2016
  
  ISBN: 978-1-4503-3549-2
  
  Publication Publication Publication
- Proving the TLS Handshake Secure (As It Is)
  
  Karthikeyan Bhargavan, Markulf Kohlweiss, Alfredo Pironti, Pierre-Yves Strub, Santiago Zanella-Béguelin, Cédric Fournet
  
  Advances in Cryptology -- CRYPTO 2014 | July 2014
  
  Publication Publication
- Probabilistic Relational Verification for Cryptographic Implementations
  
  Gilles Barthe, Cédric Fournet, Benjamin Grégoire, Pierre-Yves Strub, Santiago Zanella-Béguelin, Nikhil Swamy
  
  41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014 | January 2014
  
  To appear
  
  Publication Publication
- Smart Meter Aggregation via Secret-Sharing
  
  George Danezis, Cédric Fournet, Markulf Kohlweiss, Santiago Zanella-Béguelin
  
  2013 Smart Energy Grid Security Workshop, SEGS 2013 | January 2013
  
  To appear
  
  Publication
- Fully Automated Analysis of Padding-Based Encryption in the Computational Model
  
  Gilles Barthe, Juan Manuel Crespo, César Kunz, Benedikt Schmidt, Benjamin Grégoire, Yassine Lakhnech, Santiago Zanella-Béguelin
  
  20th ACM Conference on Computer and Communications Security, CCS 2013 | January 2013
  
  Publication Publication
- Verified Computational Differential Privacy with Applications to Smart Metering
  
  Benjamin Grégoire, César Kunz, Santiago Zanella-Béguelin, Gilles Barthe, George Danezis,
  
  26th IEEE Computer Security Foundations Symposium, CSF 2013 | January 2013
  
  Publication
- Probabilistic Relational Verification for Cryptographic Implementations
  
  Benjamin Gregoire, Pierre-Yves Strub, Nikhil Swamy, Santiago Zanella-Béguelin, Gilles Barthe, Cédric Fournet
  
  November 2012
  
  Publication
- Automation in Computer-Aided Cryptography: proofs, attacks and designs
  
  Gilles Barthe, Benjamin Grégoire, César Kunz, Yassine Lakhnech, Santiago Zanella-Béguelin
  
  2nd International Conference on Certified Programs and Proofs, CPP 2012 | April 2012
  
  Publication Publication
- Full Proof Cryptography: Verifiable Compilation of Efficient Zero-Knowledge Protocols
  
  José Bacelar Almeida, Manuel Barbosa, Endre Bangerter, Gilles Barthe, Stephen Krenn, Santiago Zanella-Béguelin
  
  19th ACM Conference on Computer and Communications Security, CCS 2012 | January 2012
  
  19th ACM Conference on Computer and Communications Security, CCS 2012
  
  Publication Publication
- Verified Security of Redundancy-Free Encryption from Rabin and RSA
  
  Gilles Barthe, David Pointcheval, Santiago Zanella-Béguelin
  
  19th ACM Conference on Computer and Communications Security, CCS 2012 | January 2012
  
  Publication Publication
- Computer-Aided Cryptographic Proofs
  
  Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, Santiago Zanella-Béguelin
  
  3rd International Conference on Interactive Theorem Proving, ITP 2012 | January 2012
  
  Publication Publication
- Probabilistic Relational Hoare Logics for Computer-Aided Security Proofs
  
  Gilles Barthe, Benjamin Grégoire, Santiago Zanella-Béguelin
  
  11th International Conference on Mathematics of Program Construction, MPC 2012 | January 2012
  
  Publication Publication
- Verified Security of Merkle-DamgÃ¥rd
  
  Michael Backes, Gilles Barthe, Matthias Berg, Benjamin Grégoire, César Kunz, Malte Skoruppa, Santiago Zanella-Béguelin
  
  25th IEEE Computer Security Foundations Symposium, CSF 2012 | January 2012
  
  Publication Publication
- Probabilistic Reasoning for Differential Privacy
  
  Gilles Barthe, Boris Köpf, Federico Olmedo, Santiago Zanella-Béguelin
  
  39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012 | January 2012
  
  Publication Publication
- Computer-Aided Cryptographic Proofs
  
  Gilles Barthe, Benjamin Grégoire, Santiago Zanella-Béguelin
  
  19th International Symposium on Static Analysis, SAS 2012 | January 2012
  
  Publication Publication
- Beyond Provable Security. Verifiable IND-CCA Security of OAEP
  
  Gilles Barthe, Benjamin Grégoire, Yassine Lakhnech, Santiago Zanella-Béguelin
  
  Topics in Cryptology, CT-RSA 2011 | January 2011
  
  ISBN: 978-3-642-19073-5
  
  Publication Publication Publication
- Computer-Aided Security Proofs for the Working Cryptographer
  
  Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Santiago Zanella-Béguelin
  
  Advances in Cryptology, CRYPTO 2011 | January 2011
  
  ISBN: 978-3-642-22791-2
  
  Best Paper Award
  
  Publication Publication Publication
- Verifiable Security of Boneh-Franklin Identity-Based Encryption
  
  Gilles Barthe, Federico Olmedo, Santiago Zanella-Béguelin
  
  5th International Conference on Provable Security, ProvSec 2011 | January 2011
  
  Publication Publication
- Formal Certification of Code-Based Cryptographic Proofs
  
  Gilles Barthe, Benjamin Grégoire, Santiago Zanella-Béguelin
  
  January 2011
  
  Publication
- A Machine-Checked Formalization of Sigma-Protocols
  
  Gilles Barthe, Daniel Hedin, Santiago Zanella-Béguelin, Benjamin Grégoire, Sylvain Heraud
  
  23rd IEEE Computer Security Foundations Symposium, CSF 2010 | January 2010
  
  23rd IEEE Computer Security Foundations Symposium, CSF 2010
  
  Publication Publication
- Programming Language Techniques for Cryptographic Proofs
  
  Gilles Barthe, Benjamin Grégoire, Santiago Zanella-Béguelin
  
  1st International Conference on Interactive Theorem Proving, ITP 2010 | January 2010
  
  Publication Publication
- Formal Certification of Code-Based Cryptographic Proofs
  
  Gilles Barthe, Benjamin Grégoire, Santiago Zanella-Béguelin
  
  36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009 | January 2009
  
  ISBN: 978-1-60558-379-2
  
  Publication Publication
- Formal certification of ElGamal encryption. A gentle introduction to CertiCrypt
  
  Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Santiago Zanella-Béguelin
  
  5th International Workshop on Formal Aspects in Security and Trust, FAST 2008 | January 2009
  
  5th International Workshop on Formal Aspects in Security and Trust, FAST 2008
  
  ISBN: 978-3-642-01464-2
  
  Publication Publication
- Formally Certifying the Security of Digital Signature Schemes
  
  Santiago Zanella-Béguelin, Benjamin Grégoire, Gilles Barthe, Federico Olmedo
  
  30th IEEE Symposium on Security and Privacy, S&P 2009 | January 2009
  
  Publication Publication
- Formalisation and Verification of the GlobalPlatform Card Specification Using the B Method
  
  Santiago Zanella-Béguelin
  
  2nd International Workshop on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, CASSIS 2005 | January 2006
  
  2nd International Workshop on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, CASSIS 2005
  
  Publication Publication
- A Formal Specification of the MIDP 2.0 Security Model
  
  Santiago Zanella-Béguelin, Gustavo Betarte, Carlos Luna
  
  4th International Workshop on Formal Aspects in Security and Trust, FAST 2006 | January 2006
  
  ISBN: 978-3-540-75226-4
  
  Publication Publication
- Securing AI Agents with Information-Flow Control
  
  Manuel Costa, Boris Köpf, Aashish Kolluri, Andrew Paverd, Mark Russinovich, Ahmed Salem, Shruti Tople, Lukas Wutschitz, Santiago Zanella-Béguelin
  
  May 2025
  
  DOI Publication Publication Project Project
- Automated Analysis and Synthesis of Padding-Based Encryption Schemes
  
  Gilles Barthe, Santiago Zanella-Béguelin, Juan Manuel Crespo, César Kunz, Yassine Lakhnech, Benjamin Grégoire
  
  December 2012
  
  IACR Cryptology ePrint Archive 2012
  
  Publication Publication
- The Canary’s Echo: Auditing Privacy Risks of LLM-Generated Synthetic Text
  
  Matthieu Meeus, Lukas Wutschitz, Santiago Zanella-Béguelin, Reza Shokri, Shruti Tople
  
  February 2025
  
  DOI Preprint Project
- Fully Automated Analysis of Padding-Based Encryption in the Computational Model
  
  Gilles Barthe, Juan Manuel Crespo, César Kunz, Benjamin Grégoire, Yassine Lakhnech, Santiago Zanella-Béguelin
  
  MSR-TR-2012-128 | December 2012
  
  IACR Cryptology ePrint Archive 2012
  
  Publication Publication
- Formal Certification of Game-Based Cryptographic Proofs
  
  Santiago Zanella-Béguelin
  
  December 2010
  
  December 2010
  
  EAPLS Best PhD Dissertation Award
  
  Publication Publication

Santiago Zanella-Béguelin

Publications

Project Everest: Perspectives from Developing Industrial-Grade High-Assurance Software

Optimizing Agent Planning for Security and Autonomy

Beyond Membership: Limitations of Add/Remove Adjacency in Differential Privacy

Permissive Information-Flow Analysis for Large Language Models

Securing AI Agents with Information-Flow Control

The Canary’s Echo: Auditing Privacy Risks of LLM-Generated Synthetic Text

The Canary’s Echo: Auditing Privacy Risks of LLM-Generated Synthetic Text

Closed-Form Bounds for DP-SGD against Record-level Inference

Dataset and Lessons Learned from the 2024 SaTML LLM Capture-the-Flag Competition

On the Efficacy of Differentially Private Few-shot Image Classification

Bayesian Estimation of Differential Privacy

Analyzing Leakage of Personally Identifiable Information in Language Models

SoK: Let the Privacy Games Begin! A Unified Treatment of Data Inference Privacy in Machine Learning

Grey-box Extraction of Natural Language Models

HACL×N: Verified Generic SIMD Crypto (for all your favourite platforms)

Analyzing Information Leakage of Updates to Natural Language Models

EverCrypt: A Fast, Veriﬁed, Cross-Platform Cryptographic Provider

Imperfect forward secrecy: how Diffie-Hellman fails in practice

A monadic framework for relational verification: applied to information security, program equivalence, and optimizations

Implementing and Proving the TLS 1.3 Record Layer

Everest: Towards a Verified, Drop-In Replacement of HTTPS

Verified Low-Level Programming Embedded in F*

Formal Verification of Smart Contracts: Short Paper

Towards a Provably Secure Implementation of TLS 1.3

Downgrade Resilience in Key-Exchange Protocols

Dependent Types and Multi-Monadic Effects in F*

Proving the TLS Handshake Secure (As It Is)

Probabilistic Relational Verification for Cryptographic Implementations

Verified Indifferentiable Hashing into Elliptic Curves

Probabilistic Relational Reasoning for Differential Privacy

Fully Automated Analysis of Padding-Based Encryption in the Computational Model

Smart Meter Aggregation via Secret-Sharing

Verified Computational Differential Privacy with Applications to Smart Metering

Automated Analysis and Synthesis of Padding-Based Encryption Schemes

Fully Automated Analysis of Padding-Based Encryption in the Computational Model

Probabilistic Relational Verification for Cryptographic Implementations

Automation in Computer-Aided Cryptography: proofs, attacks and designs

Computer-Aided Cryptographic Proofs

Computer-Aided Cryptographic Proofs

Full Proof Cryptography: Verifiable Compilation of Efficient Zero-Knowledge Protocols

Probabilistic Reasoning for Differential Privacy

Probabilistic Relational Hoare Logics for Computer-Aided Security Proofs

Verified Security of Merkle-DamgÃ¥rd

Verified Security of Redundancy-Free Encryption from Rabin and RSA

Beyond Provable Security. Verifiable IND-CCA Security of OAEP

Computer-Aided Security Proofs for the Working Cryptographer

Formal Certification of Code-Based Cryptographic Proofs

Verifiable Security of Boneh-Franklin Identity-Based Encryption

Formal Certification of Game-Based Cryptographic Proofs

A Machine-Checked Formalization of Sigma-Protocols

Programming Language Techniques for Cryptographic Proofs

Formal Certification of Code-Based Cryptographic Proofs

Formal certification of ElGamal encryption. A gentle introduction to CertiCrypt

Formally Certifying the Security of Digital Signature Schemes

A Formal Specification of the MIDP 2.0 Security Model

Formalisation and Verification of the GlobalPlatform Card Specification Using the B Method

Project Everest: Perspectives from Developing Industrial-Grade High-Assurance Software

HACL×N: Verified Generic SIMD Crypto (for all your favourite platforms)

EverCrypt: A Fast, Veriﬁed, Cross-Platform Cryptographic Provider

A monadic framework for relational verification: applied to information security, program equivalence, and optimizations

Implementing and Proving the TLS 1.3 Record Layer

Everest: Towards a Verified, Drop-In Replacement of HTTPS

Verified Low-Level Programming Embedded in F*

Formal Verification of Smart Contracts: Short Paper

Towards a Provably Secure Implementation of TLS 1.3

Dependent Types and Multi-Monadic Effects in F*

Proving the TLS Handshake Secure (As It Is)

Probabilistic Relational Verification for Cryptographic Implementations

Probabilistic Relational Reasoning for Differential Privacy

Formalisation and Verification of the GlobalPlatform Card Specification Using the B Method

Project Everest: Perspectives from Developing Industrial-Grade High-Assurance Software

Permissive Information-Flow Analysis for Large Language Models

Securing AI Agents with Information-Flow Control

The Canary’s Echo: Auditing Privacy Risks of LLM-Generated Synthetic Text

Closed-Form Bounds for DP-SGD against Record-level Inference

Dataset and Lessons Learned from the 2024 SaTML LLM Capture-the-Flag Competition

On the Efficacy of Differentially Private Few-shot Image Classification

Bayesian Estimation of Differential Privacy