Formalisation and Verification of the GlobalPlatform Card Specification Using the B Method. - Santiago Zanella-Béguelin (CASSIS, 2005)

A Formal Specification of the MIDP 2.0 Security Model. - Santiago Zanella-Béguelin; Gustavo Betarte; Carlos Luna 001 (Formal Aspects in Security and Trust, 2006)

Formal Certification of ElGamal Encryption. - Gilles Barthe; Benjamin Grégoire; Sylvain Heraud; Santiago Zanella-Béguelin (Formal Aspects in Security and Trust, 2008)

Formal certification of code-based cryptographic proofs. - Gilles Barthe; Benjamin Grégoire; Santiago Zanella-Béguelin (POPL, 2009)

Formally Certifying the Security of Digital Signature Schemes. - Santiago Zanella-Béguelin; Gilles Barthe; Benjamin Grégoire; Federico Olmedo (SP, 2009)

A Machine-Checked Formalization of Sigma-Protocols. - Gilles Barthe; Daniel Hedin; Santiago Zanella-Béguelin; Benjamin Grégoire; Sylvain Heraud (CSF, 2010)

Programming Language Techniques for Cryptographic Proofs. - Gilles Barthe; Benjamin Grégoire; Santiago Zanella-Béguelin (ITP, 2010)

Formal certification of game-based cryptographic proofs. (Certification formelle de preuves cryptographiques basées sur les séquences de jeux). - Santiago Zanella-Béguelin (2010)

Computer-Aided Security Proofs for the Working Cryptographer. - Gilles Barthe; Benjamin Grégoire; Sylvain Heraud; Santiago Zanella-Béguelin (CRYPTO, 2011)

Beyond Provable Security Verifiable IND-CCA Security of OAEP. - Gilles Barthe; Benjamin Grégoire; Yassine Lakhnech; Santiago Zanella-Béguelin (CT-RSA, 2011)

Verifiable Security of Boneh-Franklin Identity-Based Encryption. - Gilles Barthe; Federico Olmedo; Santiago Zanella-Béguelin (ProvSec, 2011)

Automation in Computer-Aided Cryptography: Proofs, Attacks and Designs. - Gilles Barthe; Benjamin Grégoire; César Kunz; Yassine Lakhnech; Santiago Zanella-Béguelin (CPP, 2012)

Verified Security of Merkle-Damgård. - Michael Backes 001; Gilles Barthe; Matthias Berg; Benjamin Grégoire; César Kunz; Malte Skoruppa; Santiago Zanella-Béguelin (CSF, 2012)

Computer-Aided Cryptographic Proofs. - Gilles Barthe; Juan Manuel Crespo; Benjamin Grégoire; César Kunz; Santiago Zanella-Béguelin (ITP, 2012)

Probabilistic Relational Hoare Logics for Computer-Aided Security Proofs. - Gilles Barthe; Benjamin Grégoire; Santiago Zanella-Béguelin (MPC, 2012)

Computer-Aided Cryptographic Proofs. - Gilles Barthe; Benjamin Grégoire; Santiago Zanella-Béguelin (SAS, 2012)

Full Proof Cryptography: Verifiable Compilation of Efficient Zero-Knowledge Protocols. - José Bacelar Almeida; Manuel Barbosa; Endre Bangerter; Gilles Barthe; Stephan Krenn; Santiago Zanella-Béguelin (IACR Cryptol. ePrint Arch., 2012)

Automated Analysis and Synthesis of Padding-Based Encryption Schemes. - Gilles Barthe; Juan Manuel Crespo; Benjamin Grégoire; César Kunz; Yassine Lakhnech; Santiago Zanella-Béguelin (IACR Cryptol. ePrint Arch., 2012)

Verified Security of Redundancy-Free Encryption from Rabin and RSA. - Gilles Barthe; David Pointcheval; Santiago Zanella-Béguelin (IACR Cryptol. ePrint Arch., 2012)

Fully automated analysis of padding-based encryption in the computational model. - Gilles Barthe; Juan Manuel Crespo; Benjamin Grégoire; César Kunz; Yassine Lakhnech; Benedikt Schmidt; Santiago Zanella-Béguelin (CCS, 2013)

Smart meter aggregation via secret-sharing. - George Danezis; Cédric Fournet; Markulf Kohlweiss; Santiago Zanella-Béguelin (SEGS@CCS, 2013)

Verified Computational Differential Privacy with Applications to Smart Metering. - Gilles Barthe; George Danezis; Benjamin Grégoire; César Kunz; Santiago Zanella-Béguelin (CSF, 2013)

Verified indifferentiable hashing into elliptic curves. - Gilles Barthe; Benjamin Grégoire; Sylvain Heraud; Federico Olmedo; Santiago Zanella-Béguelin (J. Comput. Secur., 2013)

Probabilistic Relational Reasoning for Differential Privacy. - Gilles Barthe; Boris Köpf; Federico Olmedo; Santiago Zanella-Béguelin (ACM Trans. Program. Lang. Syst., 2013)

Towards Automated Proving of Relational Properties of Probabilistic Programs (Invited Talk). - Klaus von Gleissenthall; Andrey Rybalchenko; Santiago Zanella-Béguelin (VPT@CAV, 2014)

Probabilistic relational verification for cryptographic implementations. - Gilles Barthe; Cédric Fournet; Benjamin Grégoire; Pierre-Yves Strub; Nikhil Swamy; Santiago Zanella-Béguelin (POPL, 2014)

Proving the TLS Handshake Secure (as it is). - Karthikeyan Bhargavan; Cédric Fournet; Markulf Kohlweiss; Alfredo Pironti 001; Pierre-Yves Strub; Santiago Zanella-Béguelin (IACR Cryptol. ePrint Arch., 2014)

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@CCS, 2016)

Dependent types and multi-monadic effects in F. - Nikhil Swamy; Catalin Hritcu; 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, 2016)

Downgrade Resilience in Key-Exchange Protocols. - Karthikeyan Bhargavan; Christina Brzuska; Cédric Fournet; Matthew Green 001; Markulf Kohlweiss; Santiago Zanella-Béguelin (IACR Cryptol. ePrint Arch., 2016)

Implementing and Proving the TLS 1.3 Record Layer. - Karthikeyan Bhargavan; Antoine Delignat-Lavaud; Cédric Fournet; Markulf Kohlweiss; Jianyang Pan; Jonathan Protzenko; Aseem Rastogi; Nikhil Swamy; Santiago Zanella-Béguelin; Jean Karim Zinzindohoue (IACR Cryptol. ePrint Arch., 2016)

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; K. Rustan M. Leino; Jay R. Lorch; Kenji Maillard; Jianyang Pan; et al. (SNAPL, 2017)

Verified Low-Level Programming Embedded in F*. - Jonathan Protzenko; Jean Karim Zinzindohoué; Aseem Rastogi; Tahina Ramananandro; Peng Wang 048; Santiago Zanella-Béguelin; Antoine Delignat-Lavaud; Catalin Hritcu; Karthikeyan Bhargavan; Cédric Fournet; Nikhil Swamy (CoRR, 2017)

A Monadic Framework for Relational Verification (Functional Pearl). - Niklas Grimm; Kenji Maillard; Cédric Fournet; Catalin Hritcu; Matteo Maffei; Jonathan Protzenko; Aseem Rastogi; Nikhil Swamy; Santiago Zanella-Béguelin (CoRR, 2017)

Verified low-level programming embedded in F. - Jonathan Protzenko; Jean Karim Zinzindohoué; Aseem Rastogi; Tahina Ramananandro; Peng Wang 048; Santiago Zanella-Béguelin; Antoine Delignat-Lavaud; Catalin Hritcu; Karthikeyan Bhargavan; Cédric Fournet; Nikhil Swamy (Proc. ACM Program. Lang., 2017)

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)

Imperfect forward secrecy: how Diffie-Hellman fails in practice. - David Adrian; Karthikeyan Bhargavan; Zakir Durumeric; Pierrick Gaudry; Matthew Green 001; J. Alex Halderman; Nadia Heninger; Drew Springall; Emmanuel Thomé; Luke Valenta; Benjamin VanderSloot; Eric Wustrow; et al. (Commun. ACM, 2019)

Analyzing Privacy Loss in Updates of Natural Language Models. - Shruti Tople; Marc Brockschmidt; Boris Köpf; Olga Ohrimenko; Santiago Zanella-Béguelin (CoRR, 2019)

EverCrypt: A Fast, Verified, 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; Tahina Ramananandro; Aseem Rastogi; et al. (IACR Cryptol. ePrint Arch., 2019)

Analyzing Information Leakage of Updates to Natural Language Models. - Santiago Zanella-Béguelin; Lukas Wutschitz; Shruti Tople; Victor Rühle; Andrew Paverd; Olga Ohrimenko; Boris Köpf; Marc Brockschmidt (CCS, 2020)

HACLxN: 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 (CCS, 2020)

EverCrypt: A Fast, Verified, 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; et al. (SP, 2020)

HACL×N: Verified Generic SIMD Crypto (for all your favorite platforms). - Marina Polubelova; Karthikeyan Bhargavan; Jonathan Protzenko; Benjamin Beurdouche; Aymeric Fromherz; Natalia Kulatova; Santiago Zanella-Béguelin (IACR Cryptol. ePrint Arch., 2020)

Grey-box Extraction of Natural Language Models. - Santiago Zanella-Béguelin; Shruti Tople; Andrew Paverd; Boris Köpf (ICML, 2021)

Bayesian Estimation of Differential Privacy. - Santiago Zanella-Béguelin; Lukas Wutschitz; Shruti Tople; Ahmed Salem 001; Victor Rühle; Andrew Paverd; Mohammad Naseri; Boris Köpf; Daniel Jones (ICML, 2023)

Analyzing Leakage of Personally Identifiable Information in Language Models. - Nils Lukas; Ahmed Salem 001; Robert Sim; Shruti Tople; Lukas Wutschitz; Santiago Zanella-Béguelin (SP, 2023)

SoK: Let the Privacy Games Begin! A Unified Treatment of Data Inference Privacy in Machine Learning. - Ahmed Salem 001; Giovanni Cherubin; David Evans 001; Boris Köpf; Andrew Paverd; Anshuman Suri; Shruti Tople; Santiago Zanella-Béguelin (SP, 2023)

Rethinking Privacy in Machine Learning Pipelines from an Information Flow Control Perspective. - Lukas Wutschitz; Boris Köpf; Andrew Paverd; Saravan Rajmohan; Ahmed Salem 001; Shruti Tople; Santiago Zanella-Béguelin; Menglin Xia; Victor Rühle (CoRR, 2023)

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 E. Turner; Antti Honkela (Trans. Mach. Learn. Res., 2023)

Dataset and Lessons Learned from the 2024 SaTML LLM Capture-the-Flag Competition. - Edoardo Debenedetti; Javier Rando; Daniel Paleka; Silaghi Fineas Florin; Dragos Albastroiu; Niv Cohen; Yuval Lemberg; Reshmi Ghosh; Rui Wen 002; Ahmed Salem 001; Giovanni Cherubin; Santiago Zanella-Béguelin; et al. (NeurIPS, 2024)

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, 2024)

Permissive Information-Flow Analysis for Large Language Models. - Shoaib Ahmed Siddiqui; Radhika Gaonkar; Boris Köpf; David Krueger 001; Andrew Paverd; Ahmed Salem 001; Shruti Tople; Lukas Wutschitz; Menglin Xia; Santiago Zanella-Béguelin (CoRR, 2024)

The Price of Intelligence: Three risks inherent in LLMs. - Mark Russinovich; Ahmed Salem 001; Santiago Zanella-Béguelin; Yonatan Zunger (ACM Queue, 2024)

The Canary's Echo: Auditing Privacy Risks of LLM-Generated Synthetic Text. - Matthieu Meeus; Lukas Wutschitz; Santiago Zanella-Béguelin; Shruti Tople; Reza Shokri (CoRR, 2025)

Securing AI Agents with Information-Flow Control. - Manuel Costa; Boris Köpf; Aashish Kolluri; Andrew Paverd; Mark Russinovich; Ahmed Salem 001; Shruti Tople; Lukas Wutschitz; Santiago Zanella-Béguelin (CoRR, 2025)

A Representation Engineering Perspective on the Effectiveness of Multi-Turn Jailbreaks. - Blake Bullwinkel; Mark Russinovich; Ahmed Salem 001; Santiago Zanella-Béguelin; Daniel Jones; Giorgio Severi; Eugenia Kim; Keegan Hines; Amanda J. Minnich; Yonatan Zunger; Ram Shankar Siva Kumar (CoRR, 2025)

A Systematization of Security Vulnerabilities in Computer Use Agents. - Daniel Jones; Giorgio Severi; Martin Pouliot; Gary Lopez; Joris de Gruyter; Santiago Zanella-Béguelin; Justin Song; Blake Bullwinkel; Pamela Cortez; Amanda J. Minnich (CoRR, 2025)