Santiago Zanella-Béguelin



Santiago Zanella-Béguelin
Microsoft Research Cambridge
21 Station Road
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.
  • RF* is an extension of F*, a general-purpose higher-order stateful programming language with a verification system based on refinement types. RF* extends F* with relational refinements and probabilistic computations.

Upcoming events

  • SAC 2014 (Computer Security Track). March 24 - 28, 2014. Gyeongju, South Korea
  • LATIN 2014. March 31 - April 4, 2014. Montevideo, Uruguay
  • FCC-FCS 2014. July 18, 2014. Vienna, Austria

Past Events

Journal Articles
Peer-Reviewed Papers
Invited Papers
Tech Reports