I am senior scientist and lecturer in Prof. David Basin’s Information Security group, which I joined in 2004.
My research interests lie in the intersection of formal methods and information security. I am working on the modeling and verification of distributed systems, including security protocols, secure networking protocols, concurrency control protocols, and consensus protocols. I am particularly interested in refinement techniques, (co-)inductive reasoning, compositional reasoning, and in combining model verification with code verification to obtain strong global guarantees about running systems. Tools that I am regularly using include the proof assistant Isabelle/HOL and the Tamarin prover.
Before I joined ETH Zurich, I was a postdoc at INRIA Sophia Antipolis in Prof. Gilles Barthe’s group (2002-2003) and at the Swedish Institute of Computer Science in Prof. Mads Dam’s group (2001-2002). I earned my PhD from EPFL in 2000, supervised by Prof. Claude Petitpierre. In 1992, I have obtained a Diploma (now MSc) in Computer Science from ETH Zurich.
IsaNet: A framework for verifying secure data plane protocolsJ. Comput. Secur., 2023
Igloo: soundly linking compositional refinement and separation logic for distributed system verificationProc. ACM Program. Lang., 2020
Refining security protocolsJ. Comput. Secur., 2018
S&P 2023Sound Verification of Security Protocols: From Design to Interoperable ImplementationsIn 44th IEEE Symposium on Security and Privacy, SP 2023, San Francisco, CA, USA, May 21-25, 2023, 2023
FoSSaCS 2003On the Structure of Inductive Reasoning: Circular and Tree-Shaped Proofs in the \(\mathrmμ\)-CalculusIn Foundations of Software Science and Computational Structures, (FoSSaCS 2003), 2003