Santiago ZanellaBéguelin
Researcher
I now work at Microsoft Research. This website is no longer maintained.
About
I'm a Postdoctoral Research Fellow at the Madrid Institute for Advanced Studies in Software Development Technologies (IMDEA Software Institute), Spain. I previously held a PhD position in the Everest and Marelle teams at INRIA Sophia AntipolisMéditerranée, France, under the supervision of Gilles Barthe. I also collaborate with the Secure Distributed Computations and their Proofs team in the INRIAMicrosoft Research Joint Centre.
Research Interests
I'm interested in Formal Methods in general, and in particular in
 Program Specification and Verification
 Verification of Cryptographic Systems and Implementations
 Languagebased Security
 Semantics of Programming Languages
 Theorem Provers
Software
I contribute in the development of the following tools: CertiCrypt is a framework built on top of the Coq proof assistant that enables the machinechecked construction and verification of languagebased cryptographic proofs. Certicrypt provides certified tools to reason about the equivalence of probabilistic programs, including a relational Hoare logic, a theory of observational equivalence, verified program transformations, and gamebased techniques such as reasoning about failure events.
 EasyCrypt is an automated tool for elaborating security proofs of cryptographic systems from proof sketchescompact, formal representations of the essence of a proof as a sequence of games and hints. Proof sketches are checked automatically using offtheshelf SMT solvers and automated theorem provers, and can then be compiled into verifiable proofs in the CertiCrypt framework. The tool supports most common reasoning patterns and is significantly easier to use than its predecessors.
Publications
PeerReviewed Conferences

G. Barthe, B. Grégoire, S. Heraud, F. Olmedo, S. Zanella Béguelin.
Verifiable Indifferentiable Hashing into Elliptic Curves.
In 1st Conference on Principles of Security and Trust  POST 2012.
Springer, 2012. To appear.
[ BibTeX  PDF ] 
G. Barthe, B. Köpf, F. Olmedo, S. Zanella Béguelin.
Probabilistic Reasoning for Differential Privacy.
In 39th ACM SIGPLANSIGACT Symposium on Principles of Programming Languages  POPL 2012.
ACM, 2012. To appear.
[ BibTeX  PDF ] 
G. Barthe, F. Olmedo, S. Zanella Béguelin.
Verifiable Security of BonehFranklin IdentityBased Encryption.
In 5th International Conference on Provable Security  ProvSec 2011.
volume 6980 of
Lecture Notes in Computer Science, pages 6883, Springer, 2011.
[ BibTeX  PDF  URL ] 
G. Barthe, B. Grégoire, S. Heraud, S. Zanella Béguelin.
ComputerAided Security Proofs for the Working Cryptographer.
In Advances in Cryptology  CRYPTO 2011, volume 6841 of
Lecture Notes in Computer Science, pages 7190, Springer, 2011.
Best Paper Award
[ BibTeX  PDF  URL  Slides ] 
G. Barthe, B. Grégoire, S. Zanella Béguelin, Y. Lakhnech.
Beyond Provable Security. Verifiable INDCCA Security of OAEP.
In Topics in Cryptology  CTRSA 2011, volume 6558
of Lecture Notes in Computer Science, pages 180196,
Springer, 2011.
[ BibTeX  PDF  URL ] 
G. Barthe, D. Hedin, S. Zanella Béguelin, B. Grégoire, S. Heraud.
A MachineChecked Formalization of SigmaProtocols.
In Proceedings of the 23rd IEEE Computer Security Foundations Symposium, CSF 2010, pages 246260, IEEE Computer Society, 2010.
[ BibTeX  PDF  URL  Slides ] 
G. Barthe, B. Grégoire, S. Zanella Béguelin.
Programming language techniques for cryptographic proofs.
In Proceedings of the 1st International Conference on Interactive Theorem Proving, ITP 2010, volume 5491 of Lecture Notes in Computer Science, pages 115130, Springer, 2010.
[ BibTeX  PDF  URL  Slides ] 
S. Zanella Béguelin, G. Barthe, B. Grégoire, F. Olmedo.
Formally certifying the security of digital signature schemes.
In Proceedings of the 30th IEEE Symposium on Security and Privacy, S&P 2009,
pages 237250, IEEE Computer Society, 2009.
[ BibTeX  PDF  URL  Slides ] 
G. Barthe, B. Grégoire, S. Zanella Béguelin.
Formal certification of codebased cryptographic
proofs. In Proceedings of the 36th ACM SIGPLANSIGACT Symposium on
Principles of Programming Languages, POPL 2009,
pages 90101, ACM, 2009.
[ BibTeX  PDF  URL  Slides ]
PeerReviewed Workshops

S. Zanella Béguelin, G. Betarte, C. Luna. A formal specification of the MIDP 2.0
security model. In Proceedings of the
4th International Workshop on Formal Aspects in Security
and Trust, FAST 2006,
volume 4691 of Lecture Notes in Computer Science,
pages 220234, Springer, 2006.
[ BibTeX  PDF  URL  Slides ] 
S. Zanella Béguelin. Formalisation and verification of the GlobalPlatform Card
Specification using the B method. In Proceedings of the 2nd International Workshop on
Construction and Analysis of Safe, Secure, and Interoperable Smart Devices,
CASSIS 2005, volume 3956 of Lectures Notes in Computer Science,
pages 155273. Springer, 2006.
[ BibTex  PDF  URL ]
Invited Papers

G. Barthe, B. Grégoire, S. Heraud, S. Zanella Béguelin.
Formal certification of ElGamal encryption. A gentle introduction to CertiCrypt.
In Proceedings of the 5th International Workshop on Formal Aspects in Security
and Trust, FAST 2008, volume 5491 of Lecture Notes in Computer Science,
pages 119, Springer, 2009.
[ BibTeX  PDF  URL ]
PhD Thesis
Contact Information
Santiago Zanella Béguelin
Microsoft Research