I am scientific director at the Max Planck Institute for Security and Privacy (MPI-SP) in Bochum, Germany, and a part-time research professor at IMDEA Software Institute in Madrid, Spain.

Research

My research interests include:

• Computer security, cryptography, differential privacy
• Programming languages and formal verification
• Logic and foundations of computer science

Current projects

• EasyCrypt: https://easycrypt.info/
  A toolset for reasoning about cryptographic constructions and proving their security.
• Jasmin: https://jasmin-lang.org/
  A language and toolchain for high-assurance, high-performance cryptographic implementations.
• FORMOSA: https://formosa-crypto.org/
  Formal methods for high-assurance cryptography.

Past projects (selection)

• CertiCrypt: https://github.com/EasyCrypt/certicrypt
  Machine-checked cryptographic proofs.
• maskverif: https://cryptoexperts.com/maskverif/
  Language-based, compositional, verification of higher-order masking.

PhD Students

Current

• Xingyu Xie — Automated proofs of security (since 2024)
• Yingte Xu — Formal verification of Dirac notation (since 2023)
• Santiago Olmos-Arranz — Securing the Jasmin compiler (since 2022)

Alumni

• Miguel Quaresma — High-Assurance Post-Quantum Cryptography (2026), co-advised with Peter Schwabe. Currently Security and Cryptography Researcher and Engineer at Least Authority
• Basavesh Ammanaghatta-Shivakumar — High-Assurance Protections of Crypto Software against Micro-Architectural Leakage (2024), co-advised with Peter Schwabe. Incoming Assistant Professor at Washington State University
• Marcel Fourné — Human Factors in Open Source Security (2024), co-advised with Peter Schwabe. Last affiliation: Paderborn University.
• Alejandro Aguirre — Relational Verification of Higher-Order Effectful Programs (2021). Currently assistant professor at Aarhus University
• Miguel Ambrona — Automated analysis of cryptographic constructions (2018). Currently senior cryptography engineer at Input Output (IOG)
• Juan Manuel Crespo — Automation and Modularity of Cryptographic Proofs in the Computational Model (2016). Currently Head of Connectivity Cybersecurity and Testing at Volkswagen China
• Juan Diego Campo — Formally Verified Countermeasures Against Cache-Based Attacks in Virtualization Platforms (2015). Currently Assistant Professor at Universidad de la República, Uruguay
• Federico Olmedo — Approximate Relational Reasoning for Probabilistic Programs (2014). Currently Assistant Professor at the University of Chile
• Santiago Zanella-Béguelin — Formal certification of game-based cryptographic proofs (2010). Currently Principal Researcher at Microsoft Research (Cambridge)
• César Kunz — Proof Carrying Code architecture for expressive policies (2009). Currently Senior Researcher at Huawei (Dresden)
• Mariela Pavlova — Specification and verification of Java bytecode (2007). Currently Security Certification Expert at Infineon
• Tamara Rezk — Enforcing confidentiality policies of mobile code (2006). Currently Research Director at Inria
• Sabrina Tarento — Machine-checked proofs of idealized models of cryptography (2006). Currently High-school mathematics teacher
• Maria João Frade — Constructor subtyping and type-based termination in typed lambda calculi (2004) . Currently Assistant Professor at the University of Minho / INESC TEC
• Guillaume Dufay — Formal verification of the Java Card platform (2003). Currently Senior Security Manager at ProvenRun
• Simão Sousa — Tools and techniques for the formal verification of the Java Card platform (2003). Currently Full Professor at the University of Algarve

Service (current)

• Program committees: POPL 2027, LICS 2027
• Editorial boards: Journal of Automated Reasoning
• Steering committees: FOSAD

Awards

• Honorary Doctor, Chalmers University, Sweden, 2024
• Test-of-Time Awards (2024) Secure information flow by self-composition, CSF'04)
• Lucas Award (2026) Relational Verification Using Product Programs, FM'11)
• Best Paper Awards: FSE'16, PPoPP'13, CRYPTO'11
• Distinguished Paper Awards: CCS'25, CCS'24, S&P'23, LICS'22, POPL'21, CSF'18

Publications

Selected publications are available . See full list on Google Scholar or DBLP.

Professional Experience

• Founding and Scientific Director, MPI-SP (since 2018)
• Research Professor, IMDEA Software Institute (since 2008, now part-time)
• Researcher/Research Director, INRIA Sophia-Antipolis (1999–2008)
• Assistant Professor, Universidade do Minho (1998-1999)

Eduction

• Ph.D. in Mathematical Logic, University of Manchester, 1993
• Maitrise in Pure Mathematics, University Paris XI, 1990
• Licence in Pure Mathematics, University Paris XI, 1989