Christoph Sprenger

Senior Scientist and Lecturer | Information Security | Computer Science | ETH Zurich


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.


selected publications


  1. IsaNet: A framework for verifying secure data plane protocols
    Tobias Klenze, Christoph Sprenger, and David A. Basin
    J. Comput. Secur., 2023
  2. Igloo: soundly linking compositional refinement and separation logic for distributed system verification
    Christoph Sprenger, Tobias Klenze, Marco Eilers, Felix A. Wolf, Peter Müller, Martin Clochard, and David A. Basin
    Proc. ACM Program. Lang., 2020
  3. Refining security protocols
    Christoph Sprenger, and David A. Basin
    J. Comput. Secur., 2018


  1. S&P 2023
    Sound Verification of Security Protocols: From Design to Interoperable Implementations
    Linard Arquint, Felix A. Wolf, Joseph LallemandRalf SasseChristoph Sprenger, Sven N. Wiesner, David A. Basin, and Peter Müller
    In 44th IEEE Symposium on Security and Privacy, SP 2023, San Francisco, CA, USA, May 21-25, 2023, 2023
  2. FoSSaCS 2003
    On the Structure of Inductive Reasoning: Circular and Tree-Shaped Proofs in the \(\mathrmμ\)-Calculus
    Christoph Sprenger, and Mads Dam
    In Foundations of Software Science and Computational Structures, (FoSSaCS 2003), 2003