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
Publications
Publications by Year
-
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
-
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
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
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
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
-
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
-
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
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
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, Aseem Rastogi, Nikhil Swamy, Christoph M. Wintersteiger, Santiago Zanella-Béguelin
IEEE Symposium on Security and Privacy | May 2020
-
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
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
-
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
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
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 Download 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
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
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
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
-
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
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
-
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
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
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
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
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
-
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
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
Probabilistic Relational Verification for Cryptographic Implementations
Benjamin Gregoire, Pierre-Yves Strub, Nikhil Swamy, Santiago Zanella-Béguelin, Gilles Barthe, Cédric Fournet
November 2012
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
Computer-Aided Cryptographic Proofs
Gilles Barthe, Benjamin Grégoire, Santiago Zanella-Béguelin
19th International Symposium on Static Analysis, SAS 2012 | January 2012
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
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
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
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
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
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
-
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
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
Formal Certification of Code-Based Cryptographic Proofs
Gilles Barthe, Benjamin Grégoire, Santiago Zanella-Béguelin
January 2011
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
-
Formal Certification of Game-Based Cryptographic Proofs
December 2010
December 2010
EAPLS Best PhD Dissertation Award
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
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
-
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
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
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
-
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
Formalisation and Verification of the GlobalPlatform Card Specification Using the B Method
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
Publications by Research Area
-
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
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
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
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
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
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
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
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
-
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
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
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
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
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
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
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
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
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
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, Aseem Rastogi, Nikhil Swamy, Christoph M. Wintersteiger, Santiago Zanella-Béguelin
IEEE Symposium on Security and Privacy | May 2020
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
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
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
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 Download 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
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
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
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
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
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
Probabilistic Relational Verification for Cryptographic Implementations
Benjamin Gregoire, Pierre-Yves Strub, Nikhil Swamy, Santiago Zanella-Béguelin, Gilles Barthe, Cédric Fournet
November 2012
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
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
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
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
Formal Certification of Code-Based Cryptographic Proofs
Gilles Barthe, Benjamin Grégoire, Santiago Zanella-Béguelin
January 2011
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
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
Formal Certification of Game-Based Cryptographic Proofs
December 2010
December 2010
EAPLS Best PhD Dissertation Award
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
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
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
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
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
-
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
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, Aseem Rastogi, Nikhil Swamy, Christoph M. Wintersteiger, Santiago Zanella-Béguelin
IEEE Symposium on Security and Privacy | May 2020
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
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
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
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 Download 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
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
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
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
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
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
Formalisation and Verification of the GlobalPlatform Card Specification Using the B Method
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
-
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, Aseem Rastogi, Nikhil Swamy, Christoph M. Wintersteiger, Santiago Zanella-Béguelin
IEEE Symposium on Security and Privacy | May 2020
-
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
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
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
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
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
-
Computer-Aided Cryptographic Proofs
Gilles Barthe, Benjamin Grégoire, Santiago Zanella-Béguelin
19th International Symposium on Static Analysis, SAS 2012 | January 2012
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
-
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
Publications by Type
-
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
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
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
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
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
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
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
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
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, Aseem Rastogi, Nikhil Swamy, Christoph M. Wintersteiger, Santiago Zanella-Béguelin
IEEE Symposium on Security and Privacy | May 2020
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
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
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
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 Download 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
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
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
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
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
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
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
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
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
Probabilistic Relational Verification for Cryptographic Implementations
Benjamin Gregoire, Pierre-Yves Strub, Nikhil Swamy, Santiago Zanella-Béguelin, Gilles Barthe, Cédric Fournet
November 2012
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
Computer-Aided Cryptographic Proofs
Gilles Barthe, Benjamin Grégoire, Santiago Zanella-Béguelin
19th International Symposium on Static Analysis, SAS 2012 | January 2012
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
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
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
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
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
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
Formal Certification of Code-Based Cryptographic Proofs
Gilles Barthe, Benjamin Grégoire, Santiago Zanella-Béguelin
January 2011
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
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
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
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
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
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
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
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
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
Formalisation and Verification of the GlobalPlatform Card Specification Using the B Method
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
-
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
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
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
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
-
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
-
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
-
Formal Certification of Game-Based Cryptographic Proofs
December 2010
December 2010
EAPLS Best PhD Dissertation Award