Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Santiago Zanella-Béguelin


Santiago Zanella-Béguelin
Microsoft Research Cambridge
21 Station Road
United Kingdom

Phone: +44 (0) 1223 479761
Email: santiago at microsoft dot com

I am a 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 Research Engineer position at Inria Rocquencourt 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.


  • miTLS is an open-source verified reference implementation of the TLS protocol. miTLS fully supports most features of TLS, including wire formats, ciphersuites, sessions and connections, re-handshakes and resumptions, alerts and errors, and data fragmentation. miTLS interoperates with mainstream web browsers and servers. The code is carefully structured to enable its modular, automated verification, from its main API down to computational assumptions on its cryptographic algorithms. The stable version of miTLS (v0.9) is written in F# and specified in F7. The development version of miTLS is being re-implemented in F*. Visit our GitHub repository for the latest update.
  • F* is a dependently-typed ML-like functional programming language aimed at program verification. Its rich type system allows expressing precise and compact specifications, including functional correctness properties. The F* type checker proves that programs meet their specifications using a combination of SMT solving and manual proofs. Programs written in F* can be translated to OCaml or F# for execution.
  • Weak Diffie-Hellman and the Logjam Attack. This is an Internet-wide study of the use of Diffie-Hellman key exchange in secure communications protocols, including SSH, TLS, and IPSec. We uncovered several weaknesses in deployments which lead to practical Man-in-the-Middle attacks that could be exploited for mass surveillance. We showed that performing an offline pre-computation on the most common 1024-bit Diffie-Hellman modulus used by web servers would allow passive eavesdropping on connections to 18% of the Top 1 Million HTTPS domains. Doing the same for a second modulus would allow passive decryption of connections to 66% of VPN servers and 26% of SSH servers.
  • 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

Past events

  • CSF 2015. July 13 - 17, 2015. Verona, Italy
  • 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
  • FCS 2013. June 29, 2013. New Orleans LA, USA
  • 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
Peer-Reviewed Papers
Invited Papers
Tech Reports