Christoph Sprenger


Short CV

  1. 1992: Diploma in Computer Science, ETH Zurich.

  2. 2000: Ph.D., EPF Lausanne.

  3. 2001-2002: Postdoc, Swedish Institute of Computer Science (SICS), Stockholm, with Mads Dam (supported by a Swiss European Fellowship from the SNF).

  4. 2002-2003: Postdoc, INRIA Sophia Antipolis, France, with Gilles Barthe (supported by an ERCIM Fellowship and the ModoCop project).

  5. Spring 2004: Joined David Basin’s Information Security Group at ETH Zurich.


Research interests

Formal methods for the design and analysis of computer programs and protocols with an emphasis on concurrent and distributed systems, security protocols, and information security in general. Correct-by-construction development using stepwise refinement. Abstraction techniques for efficient verification. Compositional and inductive reasoning. Program and temporal logics. Reasoning in higher-order logics and type theories. Interactive theorem proving (e.g., Isabelle, Coq).

Recent projects

  1. 2016-: Verification of secure internet routing protocols (verifiedSCION).

  2. 2014-2017: Development of consensus algorithms by stepwise refinement, verification of consensus algorithms.

  3. 2010-2014: EU NoE project NESSoS, worked on abstractions of security protocols.

  4. 2007-: Development of security protocols by stepwise refinement.

  5. 2008-2012: ZISC project on the development of secure boot processes.

  6. 2004-2008: ZISC project on the cryptographically faithful verification of security protocols.


Here is a list of my publications.


  1. Tobias Klenze, PhD student, started in Autumn 2016.

  2. Joseph Lallemand, pre-doc visitor, 9 months until Summer 2017.

  3. Ognjen Maric, PhD student, defended in February 2017.

  4. Binh Thanh Nguyen, PhD student, defended in May 2015.


Here is a list of my teaching activities.

Contact information

Institute of Information Security

Department of Computer Science
ETH Zurich

Office: CNB F 108

Address details and map

Fon: +41 44 632 75 56
Fax: +41 44 632 11 72

Email: where X=@

GPG public key

Last update: Jan 5, 2018 by Ch. Sprenger