Christoph Sprenger

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

Journals

JCS

IsaNet: A framework for verifying secure data plane protocols

Tobias Klenze, Christoph Sprenger, and David A. Basin

J. Comput. Secur., 2023

Bib HTML PDF Code

@article{DBLP:journals/jcs/KlenzeSB23,
  author = {Klenze, Tobias and Sprenger, Christoph and Basin, David A.},
  doi = {10.3233/JCS-220021},
  journal = {J. Comput. Secur.},
  number = {3},
  pages = {217--259},
  title = {IsaNet: {A} framework for verifying secure data plane protocols},
  url = {https://doi.org/10.3233/JCS-220021},
  volume = {31},
  year = {2023},
  bdsk-url-1 = {https://doi.org/10.3233/JCS-220021}
}

OOPSLA

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

arXiv Bib HTML PDF

@article{DBLP:journals/pacmpl/0001KEW0CB20,
  author = {Sprenger, Christoph and Klenze, Tobias and Eilers, Marco and Wolf, Felix A. and M{\"{u}}ller, Peter and Clochard, Martin and Basin, David A.},
  doi = {10.1145/3428220},
  journal = {Proc. {ACM} Program. Lang.},
  number = {{OOPSLA}},
  pages = {152:1--152:31},
  title = {Igloo: soundly linking compositional refinement and separation logic for distributed system verification},
  url = {https://doi.org/10.1145/3428220},
  volume = {4},
  year = {2020},
  bdsk-url-1 = {https://doi.org/10.1145/3428220}
}

JCS

Refining security protocols

Christoph Sprenger, and David A. Basin

J. Comput. Secur., 2018

Bib HTML PDF Code

@article{DBLP:journals/jcs/SprengerB18,
  author = {Sprenger, Christoph and Basin, David A.},
  doi = {10.3233/JCS-16814},
  journal = {J. Comput. Secur.},
  number = {1},
  pages = {71--120},
  title = {Refining security protocols},
  url = {https://doi.org/10.3233/JCS-16814},
  volume = {26},
  year = {2018},
  bdsk-url-1 = {https://doi.org/10.3233/JCS-16814}
}

Conferences

S&P 2023

Sound Verification of Security Protocols: From Design to Interoperable Implementations

Linard Arquint, Felix A. Wolf, Joseph Lallemand, Ralf Sasse, Christoph 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

arXiv Bib HTML PDF

@inproceedings{DBLP:conf/sp/ArquintWLSSWBM23,
  author = {Arquint, Linard and Wolf, Felix A. and Lallemand, Joseph and Sasse, Ralf and Sprenger, Christoph and Wiesner, Sven N. and Basin, David A. and M{\"{u}}ller, Peter},
  booktitle = {44th {IEEE} Symposium on Security and Privacy, {SP} 2023, San Francisco, CA, USA, May 21-25, 2023},
  doi = {10.1109/SP46215.2023.10179325},
  pages = {1077--1093},
  publisher = {{IEEE}},
  title = {Sound Verification of Security Protocols: From Design to Interoperable Implementations},
  url = {https://doi.org/10.1109/SP46215.2023.10179325},
  year = {2023},
  bdsk-url-1 = {https://doi.org/10.1109/SP46215.2023.10179325}
}

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

Bib HTML PDF

@inproceedings{DBLP:conf/fossacs/SprengerD03,
  author = {Sprenger, Christoph and Dam, Mads},
  booktitle = {Foundations of Software Science and Computational Structures, ({FoSSaCS} 2003)},
  doi = {10.1007/3-540-36576-1\_27},
  editor = {Gordon, Andrew D.},
  pages = {425--440},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  title = {On the Structure of Inductive Reasoning: Circular and Tree-Shaped Proofs in the {\(\mathrm{\mu}\)}-Calculus},
  url = {https://doi.org/10.1007/3-540-36576-1\_27},
  volume = {2620},
  year = {2003},
  bdsk-url-1 = {https://doi.org/10.1007/3-540-36576-1%5C_27}
}