About  |  CV  |  Research Interests  |  Software  |  Publications

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 Antipolis-Méditerranée, France, under the supervision of Gilles Barthe. I also collaborate with the Secure Distributed Computations and their Proofs team in the INRIA-Microsoft 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
• Language-based 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 machine-checked construction and verification of language-based 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 game-based techniques such as reasoning about failure events.
• EasyCrypt is an automated tool for elaborating security proofs of cryptographic systems from proof sketches---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, 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

Peer-Reviewed Conferences

1. 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 ]
2. G. Barthe, B. Köpf, F. Olmedo, S. Zanella Béguelin. Probabilistic Reasoning for Differential Privacy. In 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages - POPL 2012. ACM, 2012. To appear.
   [ BibTeX | PDF ]
3. G. Barthe, F. Olmedo, S. Zanella Béguelin. Verifiable Security of Boneh-Franklin Identity-Based Encryption. In 5th International Conference on Provable Security - ProvSec 2011. volume 6980 of Lecture Notes in Computer Science, pages 68-83, Springer, 2011.
   [ BibTeX | PDF | URL ]
4. G. Barthe, B. Grégoire, S. Heraud, S. Zanella Béguelin. Computer-Aided Security Proofs for the Working Cryptographer. In Advances in Cryptology - CRYPTO 2011, volume 6841 of Lecture Notes in Computer Science, pages 71-90, Springer, 2011.
   Best Paper Award
   [ BibTeX | PDF | URL | Slides ]
5. G. Barthe, B. Grégoire, S. Zanella Béguelin, Y. Lakhnech. Beyond Provable Security. Verifiable IND-CCA Security of OAEP. In Topics in Cryptology - CT-RSA 2011, volume 6558 of Lecture Notes in Computer Science, pages 180-196, Springer, 2011.
   [ BibTeX | PDF | URL ]
6. G. Barthe, D. Hedin, S. Zanella Béguelin, B. Grégoire, S. Heraud. A Machine-Checked Formalization of Sigma-Protocols. In Proceedings of the 23rd IEEE Computer Security Foundations Symposium, CSF 2010, pages 246-260, IEEE Computer Society, 2010.
   [ BibTeX | PDF | URL | Slides ]
7. 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 115-130, Springer, 2010.
   [ BibTeX | PDF | URL | Slides ]
8. 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 237-250, IEEE Computer Society, 2009.
   [ BibTeX | PDF | URL | Slides ]
9. G. Barthe, B. Grégoire, S. Zanella Béguelin. Formal certification of code-based cryptographic proofs. In Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, pages 90-101, ACM, 2009.
   [ BibTeX | PDF | URL | Slides ]

Peer-Reviewed Workshops

1. 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 220-234, Springer, 2006.
   [ BibTeX | PDF | URL | Slides ]
2. 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 155-273. Springer, 2006.
   [ BibTex | PDF | URL ]

Invited Papers

1. 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 1-19, Springer, 2009.
   [ BibTeX | PDF | URL ]

PhD Thesis

1. S. Zanella Béguelin. Formal Certification of Game-Based Cryptographic Proofs. École Nationale Supérieure des Mines de Paris, 2010.
   [ BibTeX | PDF | Slides ]