Santiago Zanella-Béguelin
POST DOC RESEARCHER
Santiago Zanella-Béguelin
Microsoft Research Cambridge
21 Station Road
CB1 2FB
Cambridge, UK
Phone: +44 (0) 1223 479 733
Email: santiago at microsoft dot com
I am a Post-Doctoral Researcher at Microsoft Research Cambridge, UK. I am a member of the Programming Principles and Tools and Constructive Security groups. I also collaborate with the Secure Distributed Computations and their Proofs team of the INRIA-Microsoft Research Joint Centre.
Previously, I held a Post-Doctoral position at the Madrid Institute for Advanced Studies in Software Development Technologies (IMDEA Software Institute), Spain. Once upon a time I got my PhD from École Nationale Supérieure des Mines de Paris, working in the Everest and Marelle teams at INRIA Sophia Antipolis-Méditerranée, France, under the supervision of Gilles Barthe.
I contribute to the following projects:
- CertiCrypt is a fully machine-checked framework built on top of the Coq proof assistant. It is based on a deep embedding of an extensible probabilistic imperative language and a formalization of probabilistic polynomial-time programs. Verification methods are implemented in Coq, and proved correct w.r.t. program semantics. This framework is presented in my PhD thesis and in this POPL 2009 paper.
- EasyCrypt is an automated tool for elaborating security proofs of cryptographic systems from proof sketches. The latter are compact, formal representations of the essence of a proof as a sequence of games and hints. Proof sketches are checked automatically using off-the-shelf SMT solvers and automated theorem provers. This tool is presented in this CRYPTO 2011 paper.
- ZooCrypt is an automated tool for analyzing the security of padding-based public-key encryption schemes (i.e. schemes built from trapdoor permutations and hash functions). ZooCrypt includes an experimental mechanism to generate EasyCrypt proofs of security of analyzed schemes.
Upcoming events
-
FCS 2013. June 29, 2013. New Orleans LA, USA
-
SAC 2014 (Computer Security Track). March 24 - 28, 2014. Gyeongju, South Korea
-
LATIN 2014. March 31 - April 4, 2014. Montevideo, Uruguay
Past Events
- CPP 2012. December 13-15, 2012. Kyoto, Japan
- LatinCrypt 2012. October 7-10, 2012. Santiago, Chile
- FCC 2012. June 27-28, 2012. Cambridge MA, USA
Journal Articles
- Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Federico Olmedo, and Santiago Zanella-Béguelin, Verified Indifferentiable Hashing into Elliptic Curves, in Journal of Computer Security, IOS Press, 2013
- Gilles Barthe, Boris Koepf, Federico Olmedo, and Santiago Zanella-Béguelin, Probabilistic Relational Reasoning for Differential Privacy, in ACM Trans. Program. Lang. Syst., ACM, 2013
- Gilles Barthe, Benjamin Grégoire, and Santiago Zanella-Béguelin, Formal Certification of Code-Based Cryptographic Proofs, in Submitted manuscript under review, ACM, 2010
Peer-Reviewed Papers
- Gilles Barthe, George Danezis, Benjamin Grégoire, César Kunz, and Santiago Zanella-Béguelin, Verified Computational Differential Privacy with Applications to Smart Metering, in 26th IEEE Computer Security Foundations Symposium, IEEE, 2013
- Gilles Barthe, Boris Köpf, Federico Olmedo, and Santiago Zanella-Béguelin, Probabilistic Reasoning for Differential Privacy, in 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, ACM, New York, 2012
- José Bacelar Almeida, Manuel Barbosa, Endre Bangerter, Gilles Barthe, Stephen Krenn, and Santiago Zanella-Béguelin, Full Proof Cryptography: Verifiable Compilation of Efficient Zero-Knowledge Protocols, in 19th ACM Conference on Computer and Communications Security, CCS 2012, ACM Press, 2012
- Gilles Barthe, David Pointcheval, and Santiago Zanella-Béguelin, Verified Security of Redundancy-Free Encryption from Rabin and RSA, in 19th ACM Conference on Computer and Communications Security, CCS 2012, ACM, New York, 2012
- Michael Backes, Gilles Barthe, Matthias Berg, Benjamin Grégoire, César Kunz, Malte Skoruppa, and Santiago Zanella-Béguelin, Verified security of Merkle-Damgård, in 25th IEEE Computer Security Foundations Symposium, CSF 2012, IEEE Computer Society, Los Alamitos, 2012
- Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, Federico Olmedo, and Santiago Zanella-Béguelin, Verified Indifferentiable Hashing into Elliptic Curves, in 1st International Conference on Principles of Security and Trust, POST 2012, Springer, Heidelberg, 2012
- Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, and Santiago Zanella-Béguelin, Computer-Aided Security Proofs for the Working Cryptographer, in Advances in Cryptology, CRYPTO 2011, Springer, Heidelberg, 2011
- Gilles Barthe, Benjamin Grégoire, Yassine Lakhnech, and Santiago Zanella-Béguelin, Beyond Provable Security. Verifiable IND-CCA Security of OAEP, in Topics in Cryptology, CT-RSA 2011, Springer, Heidelberg, 2011
- Gilles Barthe, Federico Olmedo, and Santiago Zanella-Béguelin, Verifiable Security of Boneh-Franklin Identity-Based Encryption, in 5th International Conference on Provable Security, ProvSec 2011, Springer, Heidelberg, 2011
- Gilles Barthe, Benjamin Grégoire, and Santiago Zanella-Béguelin, Programming Language Techniques for Cryptographic Proofs, in 1st International Conference on Interactive Theorem Proving, ITP 2010, Springer, Heidelberg, 2010
- Gilles Barthe, Daniel Hedin, Santiago Zanella-Béguelin, Benjamin Grégoire, and Sylvain Heraud, A Machine-Checked Formalization of Sigma-Protocols, in 23rd IEEE Computer Security Foundations Symposium, CSF 2010, IEEE Computer Society, Los Alamitos, 2010
- Gilles Barthe, Benjamin Grégoire, and Santiago Zanella-Béguelin, Formal Certification of Code-Based Cryptographic Proofs, in 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, ACM, New York, 2009
- Santiago Zanella-Béguelin, Benjamin Grégoire, Gilles Barthe, and Federico Olmedo, Formally Certifying the Security of Digital Signature Schemes, in 30th IEEE Symposium on Security and Privacy, S&P 2009, IEEE Computer Society, Los Alamitos, 2009
- Santiago Zanella-Béguelin, Gustavo Betarte, and Carlos Luna, A Formal Specification of the MIDP 2.0 Security Model, in 4th International Workshop on Formal Aspects in Security and Trust, FAST 2006, Springer, Heidelberg, 2006
- Santiago Zanella-Béguelin, Formalisation and Verification of the GlobalPlatform Card Specification Using the B Method, in 2nd International Workshop on Construction and Analysis of Safe, Secure, and Interoperable Smart Devices, CASSIS 2005, Springer, Heidelberg, 2006
Invited Papers
- Gilles Barthe, Benjamin Grégoire, and Santiago Zanella-Béguelin, Computer-Aided Cryptographic Proofs, in 19th International Symposium on Static Analysis, SAS 2012, Springer, Heidelberg, 2012
- Gilles Barthe, Benjamin Grégoire, and Santiago Zanella-Béguelin, Probabilistic Relational Hoare Logics for Computer-Aided Security Proofs, in 11th International Conference on Mathematics of Program Construction, MPC 2012, Springer, Heidelberg, 2012
- Gilles Barthe, Benjamin Grégoire, César Kunz, Yassine Lakhnech, and Santiago Zanella-Béguelin, Automation in Computer-Aided Cryptography: proofs, attacks and designs, in 2nd International Conference on Certified Programs and Proofs, CPP 2012, Springer, Heidelberg, 2012
- Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, and Santiago Zanella-Béguelin, Computer-Aided Cryptographic Proofs, in 3rd International Conference on Interactive Theorem Proving, ITP 2012, Springer, Heidelberg, 2012
- Gilles Barthe, Benjamin Grégoire, Sylvain Heraud, and Santiago Zanella-Béguelin, Formal certification of ElGamal encryption. A gentle introduction to CertiCrypt, in 5th International Workshop on Formal Aspects in Security and Trust, FAST 2008, Springer, Heidelberg, 2009
Tech Reports
- Santiago Zanella-Béguelin, Gilles Barthe, Juan Manuel Crespo, Benjamin Grégoire, César Kunz, and Yassine Lakhnech, Automated Analysis and Synthesis of Padding-Based Encryption Schemes, no. 2012/695, International Association for Cryptologic Research, December 2012
- Gilles Barthe, Cedric Fournet, Benjamin Gregoire, Pierre-Yves Strub, Nikhil Swamy, and Santiago Zanella Beguelin, Probabilistic Relational Verification for Cryptographic Implementations, November 2012
Theses
- Santiago Zanella-Béguelin, Formal Certification of Game-Based Cryptographic Proofs, École des Mines de Paris, EAPLS Best PhD Dissertation Award, December 2010