publications | Christoph Sprenger

Journals

The Sumcheck Protocol

Azucena Garvı́a Bosshard, Christoph Sprenger, and Jonathan Bootle

Arch. Formal Proofs, 2024

Bib

@article{DBLP:journals/afp/BosshardSB24,
  author = {Garv{\'{\i}}a Bosshard, Azucena and Sprenger, Christoph and Bootle, Jonathan},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  biburl = {https://dblp.org/rec/journals/afp/BosshardSB24.bib},
  date-added = {2024-03-11 12:46:27 +0100},
  date-modified = {2024-06-14 18:00:34 +0200},
  journal = {Arch. Formal Proofs},
  timestamp = {Tue, 20 Feb 2024 15:24:42 +0100},
  title = {The Sumcheck Protocol},
  volume = {2024},
  year = {2024},
}

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}
}

AFP

IsaNet: Formalization of a Verification Framework for Secure Data Plane Protocols

Tobias Klenze, and Christoph Sprenger

Arch. Formal Proofs, 2022

Bib HTML

@article{DBLP:journals/afp/Klenze022,
  author = {Klenze, Tobias and Sprenger, Christoph},
  journal = {Arch. Formal Proofs},
  title = {IsaNet: Formalization of a Verification Framework for Secure Data Plane Protocols},
  year = {2022},
}

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}
}

JCS

Abstractions for security protocol verification

Thanh Binh Nguyen, Christoph Sprenger, and Cas Cremers

J. Comput. Secur., 2018

Bib HTML PDF

@article{DBLP:journals/jcs/NguyenSC18,
  author = {Nguyen, Thanh Binh and Sprenger, Christoph and Cremers, Cas},
  doi = {10.3233/JCS-15769},
  journal = {J. Comput. Secur.},
  number = {4},
  pages = {459--508},
  title = {Abstractions for security protocol verification},
  url = {https://doi.org/10.3233/JCS-15769},
  volume = {26},
  year = {2018},
  bdsk-url-1 = {https://doi.org/10.3233/JCS-15769}
}

AFP

Refining Authenticated Key Agreement with Strong Adversaries

Joseph Lallemand, and Christoph Sprenger

Arch. Formal Proofs, 2017

Bib HTML

@article{DBLP:journals/afp/LallemandS17,
  author = {Lallemand, Joseph and Sprenger, Christoph},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  journal = {Arch. Formal Proofs},
  title = {Refining Authenticated Key Agreement with Strong Adversaries},
  year = {2017},
}

AFP

Developing Security Protocols by Refinement

Christoph Sprenger, and Ivano Somaini

Arch. Formal Proofs, 2017

Bib HTML

@article{DBLP:journals/afp/SprengerS17,
  author = {Sprenger, Christoph and Somaini, Ivano},
  journal = {Arch. Formal Proofs},
  title = {Developing Security Protocols by Refinement},
  year = {2017},
}

AFP

Consensus Refined

Ognjen Maric, and Christoph Sprenger

Arch. Formal Proofs, 2015

Bib HTML

@article{DBLP:journals/afp/MaricS15,
  author = {Maric, Ognjen and Sprenger, Christoph},
  journal = {Arch. Formal Proofs},
  title = {Consensus Refined},
  volume = {2015},
  year = {2015},
}

Inf. Comput.

Compositional verification of sequential programs with procedures

Dilian Gurov, Marieke Huisman, and Christoph Sprenger

Inf. Comput., 2008

Bib HTML PDF

@article{DBLP:journals/iandc/GurovHS08,
  author = {Gurov, Dilian and Huisman, Marieke and Sprenger, Christoph},
  doi = {10.1016/j.ic.2008.03.003},
  journal = {Inf. Comput.},
  number = {7},
  pages = {840--868},
  title = {Compositional verification of sequential programs with procedures},
  url = {https://doi.org/10.1016/j.ic.2008.03.003},
  volume = {206},
  year = {2008},
  bdsk-url-1 = {https://doi.org/10.1016/j.ic.2008.03.003}
}

On global induction mechanisms in a \(\mathrmμ\)-calculus with explicit approximations

Christoph Sprenger, and Mads Dam

RAIRO Theor. Informatics Appl., 2003

Bib HTML PDF

@article{DBLP:journals/ita/SprengerD03,
  author = {Sprenger, Christoph and Dam, Mads},
  doi = {10.1051/ita:2003024},
  journal = {{RAIRO} Theor. Informatics Appl.},
  number = {4},
  pages = {365--391},
  title = {On global induction mechanisms in a {\(\mathrm{\mu}\)}-calculus with explicit approximations},
  url = {https://doi.org/10.1051/ita:2003024},
  volume = {37},
  year = {2003},
  bdsk-url-1 = {https://doi.org/10.1051/ita:2003024}
}

SCIDDLE: A tool for large scale distributed computing

Peter Arbenz, Christoph Sprenger, Hans Peter Lüthi, and Stefan Vogel

Concurr. Pract. Exp., 1995

Bib HTML

@article{DBLP:journals/concurrency/ArbenzSLV95,
  author = {Arbenz, Peter and Sprenger, Christoph and L{\"{u}}thi, Hans Peter and Vogel, Stefan},
  doi = {10.1002/cpe.4330070203},
  journal = {Concurr. Pract. Exp.},
  number = {2},
  pages = {121--146},
  title = {{SCIDDLE:} {A} tool for large scale distributed computing},
  url = {https://doi.org/10.1002/cpe.4330070203},
  volume = {7},
  year = {1995},
  bdsk-url-1 = {https://doi.org/10.1002/cpe.4330070203}
}

Conferences

CSF 2024

Formal Verification of the Sumcheck Protocol

Azucena Garvia Bosshard, Jonathan Bootle, and Christoph Sprenger

In 37th IEEE Computer Security Foundations Symposium, CSF 2024, Enschede, The Netherlands, July 8-12, 2024, 2024

To appear.

Bib

@inproceedings{GarviaSprengerBootle24,
  author = {Garvia Bosshard, Azucena and Bootle, Jonathan and Sprenger, Christoph},
  booktitle = {37th {IEEE} Computer Security Foundations Symposium, {CSF} 2024, Enschede, The Netherlands, July 8-12, 2024},
  date-modified = {2024-05-29 09:12:52 +0200},
  note = {To appear.},
  publisher = {{IEEE}},
  title = {Formal Verification of the Sumcheck Protocol},
  year = {2024},
  bdsk-url-1 = {https://doi.org/10.1109/CSF51468.2021.00018}
}

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}
}

CSF 2022

N-Tube: Formally Verified Secure Bandwidth Reservation in Path-Aware Internet Architectures

Thilo Weghorn, Si Liu, Christoph Sprenger, Adrian Perrig, and David A. Basin

In 35th IEEE Computer Security Foundations Symposium, CSF 2022, Haifa, Israel, August 7-10, 2022, 2022

Bib HTML PDF

@inproceedings{DBLP:conf/csfw/WeghornLSPB22,
  author = {Weghorn, Thilo and Liu, Si and Sprenger, Christoph and Perrig, Adrian and Basin, David A.},
  biburl = {https://dblp.org/rec/conf/csfw/WeghornLSPB22.bib},
  booktitle = {35th {IEEE} Computer Security Foundations Symposium, {CSF} 2022, Haifa, Israel, August 7-10, 2022},
  doi = {10.1109/CSF54842.2022.9919646},
  pages = {147--162},
  publisher = {{IEEE}},
  title = {N-Tube: Formally Verified Secure Bandwidth Reservation in Path-Aware Internet Architectures},
  url = {https://doi.org/10.1109/CSF54842.2022.9919646},
  year = {2022},
  bdsk-url-1 = {https://doi.org/10.1109/CSF54842.2022.9919646}
}

CSF 2021

Formal Verification of Secure Forwarding Protocols

Tobias Klenze, Christoph Sprenger, and David A. Basin

In 34th IEEE Computer Security Foundations Symposium, CSF 2021, Dubrovnik, Croatia, June 21-25, 2021, 2021

Bib HTML PDF

@inproceedings{DBLP:conf/csfw/Klenze0B21,
  author = {Klenze, Tobias and Sprenger, Christoph and Basin, David A.},
  booktitle = {34th {IEEE} Computer Security Foundations Symposium, {CSF} 2021, Dubrovnik, Croatia, June 21-25, 2021},
  date-added = {2024-05-29 09:06:05 +0200},
  date-modified = {2024-05-29 09:06:05 +0200},
  doi = {10.1109/CSF51468.2021.00018},
  pages = {1--16},
  publisher = {{IEEE}},
  title = {Formal Verification of Secure Forwarding Protocols},
  url = {https://doi.org/10.1109/CSF51468.2021.00018},
  year = {2021},
  bdsk-url-1 = {https://doi.org/10.1109/CSF51468.2021.00018}
}

EuroS&P 2020

SoK: Delegation and Revocation, the Missing Links in the Web’s Chain of Trust

Laurent Chuat, AbdelRahman Abdou, Ralf Sasse, Christoph Sprenger, David A. Basin, and Adrian Perrig

In IEEE European Symposium on Security and Privacy, EuroS&P 2020, Genoa, Italy, September 7-11, 2020, 2020

arXiv Bib HTML PDF

@inproceedings{DBLP:conf/eurosp/ChuatAS0BP20,
  author = {Chuat, Laurent and Abdou, AbdelRahman and Sasse, Ralf and Sprenger, Christoph and Basin, David A. and Perrig, Adrian},
  booktitle = {{IEEE} European Symposium on Security and Privacy, EuroS{\&}P 2020, Genoa, Italy, September 7-11, 2020},
  doi = {10.1109/EuroSP48549.2020.00046},
  pages = {624--638},
  publisher = {{IEEE}},
  title = {SoK: Delegation and Revocation, the Missing Links in the Web's Chain of Trust},
  url = {https://doi.org/10.1109/EuroSP48549.2020.00046},
  year = {2020},
  bdsk-url-1 = {https://doi.org/10.1109/EuroSP48549.2020.00046}
}

USENIX Sec. 2020

EPIC: Every Packet Is Checked in the Data Plane of a Path-Aware Internet

Markus Legner, Tobias Klenze, Marc Wyss, Christoph Sprenger, and Adrian Perrig

In 29th USENIX Security Symposium, USENIX Security 2020, August 12-14, 2020, 2020

Bib HTML

@inproceedings{DBLP:conf/uss/LegnerKW0P20,
  author = {Legner, Markus and Klenze, Tobias and Wyss, Marc and Sprenger, Christoph and Perrig, Adrian},
  booktitle = {29th {USENIX} Security Symposium, {USENIX} Security 2020, August 12-14, 2020},
  editor = {Capkun, Srdjan and Roesner, Franziska},
  pages = {541--558},
  publisher = {{USENIX} Association},
  title = {{EPIC:} Every Packet Is Checked in the Data Plane of a Path-Aware Internet},
  url = {https://www.usenix.org/conference/usenixsecurity20/presentation/legner},
  year = {2020},
  bdsk-url-1 = {https://www.usenix.org/conference/usenixsecurity20/presentation/legner}
}

CAV 2017

Cutoff Bounds for Consensus Algorithms

Ognjen Maric, Christoph Sprenger, and David A. Basin

In Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II, 2017

Bib HTML PDF

@inproceedings{DBLP:conf/cav/MaricSB17,
  author = {Maric, Ognjen and Sprenger, Christoph and Basin, David A.},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  booktitle = {Computer Aided Verification - 29th International Conference, {CAV} 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part {II}},
  doi = {10.1007/978-3-319-63390-9\_12},
  editor = {Majumdar, Rupak and Kuncak, Viktor},
  pages = {217--237},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  title = {Cutoff Bounds for Consensus Algorithms},
  url = {https://doi.org/10.1007/978-3-319-63390-9\_12},
  volume = {10427},
  year = {2017},
  bdsk-url-1 = {https://doi.org/10.1007/978-3-319-63390-9%5C_12}
}

EuroS&P 2017

Refining Authenticated Key Agreement with Strong Adversaries

Joseph Lallemand, David A. Basin, and Christoph Sprenger

In 2017 IEEE European Symposium on Security and Privacy, EuroS&P 2017, Paris, France, April 26-28, 2017, 2017

Bib HTML PDF Code

@inproceedings{DBLP:conf/eurosp/LallemandBS17,
  author = {Lallemand, Joseph and Basin, David A. and Sprenger, Christoph},
  booktitle = {2017 {IEEE} European Symposium on Security and Privacy, EuroS{\&}P 2017, Paris, France, April 26-28, 2017},
  doi = {10.1109/EuroSP.2017.22},
  pages = {92--107},
  publisher = {{IEEE}},
  title = {Refining Authenticated Key Agreement with Strong Adversaries},
  url = {https://doi.org/10.1109/EuroSP.2017.22},
  year = {2017},
  bdsk-url-1 = {https://doi.org/10.1109/EuroSP.2017.22}
}

DSN 2015

Consensus Refined

Ognjen Maric, Christoph Sprenger, and David A. Basin

In 45th Annual IEEE/IFIP International Conference on Dependable Systems and Networks, DSN 2015, Rio de Janeiro, Brazil, June 22-25, 2015, 2015

Bib HTML PDF Code

@inproceedings{DBLP:conf/dsn/MaricSB15,
  author = {Maric, Ognjen and Sprenger, Christoph and Basin, David A.},
  booktitle = {45th Annual {IEEE/IFIP} International Conference on Dependable Systems and Networks, {DSN} 2015, Rio de Janeiro, Brazil, June 22-25, 2015},
  doi = {10.1109/DSN.2015.38},
  pages = {391--402},
  publisher = {{IEEE} Computer Society},
  title = {Consensus Refined},
  url = {https://doi.org/10.1109/DSN.2015.38},
  year = {2015},
  bdsk-url-1 = {https://doi.org/10.1109/DSN.2015.38}
}

POST 2015

Abstractions for Security Protocol Verification

Thanh Binh Nguyen, and Christoph Sprenger

In Principles of Security and Trust - 4th International Conference, POST 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2015, London, UK, April 11-18, 2015, Proceedings, 2015

Bib HTML PDF

@inproceedings{DBLP:conf/post/0003S15,
  author = {Nguyen, Thanh Binh and Sprenger, Christoph},
  booktitle = {Principles of Security and Trust - 4th International Conference, {POST} 2015, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2015, London, UK, April 11-18, 2015, Proceedings},
  doi = {10.1007/978-3-662-46666-7\_11},
  editor = {Focardi, Riccardo and Myers, Andrew C.},
  pages = {196--215},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  title = {Abstractions for Security Protocol Verification},
  url = {https://doi.org/10.1007/978-3-662-46666-7\_11},
  volume = {9036},
  year = {2015},
  bdsk-url-1 = {https://doi.org/10.1007/978-3-662-46666-7%5C_11}
}

FM 2014

Verification of a Transactional Memory Manager under Hardware Failures and Restarts

Ognjen Maric, and Christoph Sprenger

In FM 2014: Formal Methods - 19th International Symposium, Singapore, May 12-16, 2014. Proceedings, 2014

Bib HTML PDF

@inproceedings{DBLP:conf/fm/MaricS14,
  author = {Maric, Ognjen and Sprenger, Christoph},
  booktitle = {{FM} 2014: Formal Methods - 19th International Symposium, Singapore, May 12-16, 2014. Proceedings},
  doi = {10.1007/978-3-319-06410-9\_31},
  editor = {Jones, Cliff B. and Pihlajasaari, Pekka and Sun, Jun},
  pages = {449--464},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  title = {Verification of a Transactional Memory Manager under Hardware Failures and Restarts},
  url = {https://doi.org/10.1007/978-3-319-06410-9\_31},
  volume = {8442},
  year = {2014},
  bdsk-url-1 = {https://doi.org/10.1007/978-3-319-06410-9%5C_31}
}

POST 2013

Sound Security Protocol Transformations

Thanh Binh Nguyen, and Christoph Sprenger

In Principles of Security and Trust - Second International Conference, POST 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings, 2013

Bib HTML PDF

@inproceedings{DBLP:conf/post/NguyenS13,
  author = {Nguyen, Thanh Binh and Sprenger, Christoph},
  booktitle = {Principles of Security and Trust - Second International Conference, {POST} 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2013, Rome, Italy, March 16-24, 2013. Proceedings},
  doi = {10.1007/978-3-642-36830-1\_5},
  editor = {Basin, David A. and Mitchell, John C.},
  pages = {83--104},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  title = {Sound Security Protocol Transformations},
  url = {https://doi.org/10.1007/978-3-642-36830-1\_5},
  volume = {7796},
  year = {2013},
  bdsk-url-1 = {https://doi.org/10.1007/978-3-642-36830-1%5C_5}
}

CSF 2012

Refining Key Establishment

Christoph Sprenger, and David A. Basin

In 25th IEEE Computer Security Foundations Symposium, CSF 2012, Cambridge, MA, USA, June 25-27, 2012, 2012

Bib HTML PDF

@inproceedings{DBLP:conf/csfw/SprengerB12,
  author = {Sprenger, Christoph and Basin, David A.},
  booktitle = {25th {IEEE} Computer Security Foundations Symposium, {CSF} 2012, Cambridge, MA, USA, June 25-27, 2012},
  doi = {10.1109/CSF.2012.21},
  editor = {Chong, Stephen},
  pages = {230--246},
  publisher = {{IEEE} Computer Society},
  title = {Refining Key Establishment},
  url = {https://doi.org/10.1109/CSF.2012.21},
  year = {2012},
  bdsk-url-1 = {https://doi.org/10.1109/CSF.2012.21}
}

CCS 2010

Developing security protocols by refinement

Christoph Sprenger, and David A. Basin

In Proceedings of the 17th ACM Conference on Computer and Communications Security, CCS 2010, Chicago, Illinois, USA, October 4-8, 2010, 2010

Bib HTML PDF

@inproceedings{DBLP:conf/ccs/SprengerB10,
  author = {Sprenger, Christoph and Basin, David A.},
  booktitle = {Proceedings of the 17th {ACM} Conference on Computer and Communications Security, {CCS} 2010, Chicago, Illinois, USA, October 4-8, 2010},
  doi = {10.1145/1866307.1866349},
  editor = {Al{-}Shaer, Ehab and Keromytis, Angelos D. and Shmatikov, Vitaly},
  pages = {361--374},
  publisher = {{ACM}},
  title = {Developing security protocols by refinement},
  url = {https://doi.org/10.1145/1866307.1866349},
  year = {2010},
  bdsk-url-1 = {https://doi.org/10.1145/1866307.1866349}
}

CSF 2008

Cryptographically-Sound Protocol-Model Abstractions

Christoph Sprenger, and David A. Basin

In Proceedings of the 21st IEEE Computer Security Foundations Symposium, CSF 2008, Pittsburgh, Pennsylvania, USA, 23-25 June 2008, 2008

Bib HTML PDF

@inproceedings{DBLP:conf/csfw/SprengerB08,
  author = {Sprenger, Christoph and Basin, David A.},
  biburl = {https://dblp.org/rec/conf/csfw/SprengerB08.bib},
  booktitle = {Proceedings of the 21st {IEEE} Computer Security Foundations Symposium, {CSF} 2008, Pittsburgh, Pennsylvania, USA, 23-25 June 2008},
  doi = {10.1109/CSF.2008.19},
  pages = {115--129},
  publisher = {{IEEE} Computer Society},
  title = {Cryptographically-Sound Protocol-Model Abstractions},
  url = {https://doi.org/10.1109/CSF.2008.19},
  year = {2008},
  bdsk-url-1 = {https://doi.org/10.1109/CSF.2008.19}
}

TPHOLs 2007

A Monad-Based Modeling and Verification Toolbox with Application to Security Protocols

Christoph Sprenger, and David A. Basin

In Theorem Proving in Higher Order Logics, 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007, Proceedings, 2007

Bib HTML PDF

@inproceedings{DBLP:conf/tphol/SprengerB07,
  author = {Sprenger, Christoph and Basin, David A.},
  booktitle = {Theorem Proving in Higher Order Logics, 20th International Conference, TPHOLs 2007, Kaiserslautern, Germany, September 10-13, 2007, Proceedings},
  doi = {10.1007/978-3-540-74591-4\_23},
  editor = {Schneider, Klaus and Brandt, Jens},
  pages = {302--318},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  title = {A Monad-Based Modeling and Verification Toolbox with Application to Security Protocols},
  url = {https://doi.org/10.1007/978-3-540-74591-4\_23},
  volume = {4732},
  year = {2007},
  bdsk-url-1 = {https://doi.org/10.1007/978-3-540-74591-4%5C_23}
}

CSFW 2006

Cryptographically Sound Theorem Proving

Christoph Sprenger, Michael Backes, David A. Basin, Birgit Pfitzmann, and Michael Waidner

In 19th IEEE Computer Security Foundations Workshop, (CSFW-19 2006), 5-7 July 2006, Venice, Italy, 2006

Bib HTML PDF

@inproceedings{DBLP:conf/csfw/SprengerBBPW06,
  author = {Sprenger, Christoph and Backes, Michael and Basin, David A. and Pfitzmann, Birgit and Waidner, Michael},
  booktitle = {19th {IEEE} Computer Security Foundations Workshop, {(CSFW-19} 2006), 5-7 July 2006, Venice, Italy},
  doi = {10.1109/CSFW.2006.10},
  pages = {153--166},
  publisher = {{IEEE} Computer Society},
  title = {Cryptographically Sound Theorem Proving},
  url = {https://doi.org/10.1109/CSFW.2006.10},
  year = {2006},
  bdsk-url-1 = {https://doi.org/10.1109/CSFW.2006.10}
}

FASE 2004

Checking Absence of Illicit Applet Interactions: A Case Study

Marieke Huisman, Dilian Gurov, Christoph Sprenger, and Gennady Chugunov

In Fundamental Approaches to Software Engineering, 7th International Conference, FASE 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004 Barcelona, Spain, March 29 - april 2, 2004, Proceedings, 2004

Bib HTML PDF

@inproceedings{DBLP:conf/fase/HuismanGSC04,
  author = {Huisman, Marieke and Gurov, Dilian and Sprenger, Christoph and Chugunov, Gennady},
  booktitle = {Fundamental Approaches to Software Engineering, 7th International Conference, {FASE} 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, {ETAPS} 2004 Barcelona, Spain, March 29 - april 2, 2004, Proceedings},
  doi = {10.1007/978-3-540-24721-0\_6},
  editor = {Wermelinger, Michel and Margaria, Tiziana},
  pages = {84--98},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  title = {Checking Absence of Illicit Applet Interactions: {A} Case Study},
  url = {https://doi.org/10.1007/978-3-540-24721-0\_6},
  volume = {2984},
  year = {2004},
  bdsk-url-1 = {https://doi.org/10.1007/978-3-540-24721-0%5C_6}
}

MEMOCODE 2004

Compositional verification for secure loading of smart card applets

Christoph Sprenger, Dilian Gurov, and Marieke Huisman

In 2nd ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2004), 23-25 June 2004, San Diego, California, USA, Proceedings, 2004

Bib HTML PDF

  author = {Sprenger, Christoph and Gurov, Dilian and Huisman, Marieke},
  booktitle = {2nd {ACM} {\&} {IEEE} International Conference on Formal Methods and Models for Co-Design {(MEMOCODE} 2004), 23-25 June 2004, San Diego, California, USA, Proceedings},
  doi = {10.1109/MEMCOD.2004.1459857},
  pages = {211--222},
  publisher = {{IEEE} Computer Society},
  title = {Compositional verification for secure loading of smart card applets},
  url = {https://doi.org/10.1109/MEMCOD.2004.1459857},
  year = {2004},
  bdsk-url-1 = {https://doi.org/10.1109/MEMCOD.2004.1459857}
}

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}
}

MEMOCODE 2003

A Verification Methodology for Infinite-State Message Passing Systems

Christoph Sprenger, and Krzysztof Worytkiewicz

In 1st ACM & IEEE International Conference on Formal Methods and Models for Co-Design (MEMOCODE 2003), 24-26 June 2003, Mont Saint-Michel, France, Proceedings, 2003

Bib HTML PDF

  author = {Sprenger, Christoph and Worytkiewicz, Krzysztof},
  booktitle = {1st {ACM} {\&} {IEEE} International Conference on Formal Methods and Models for Co-Design {(MEMOCODE} 2003), 24-26 June 2003, Mont Saint-Michel, France, Proceedings},
  doi = {10.1109/MEMCOD.2003.1210110},
  pages = {255--264},
  publisher = {{IEEE} Computer Society},
  title = {A Verification Methodology for Infinite-State Message Passing Systems},
  url = {https://doi.org/10.1109/MEMCOD.2003.1210110},
  year = {2003},
  bdsk-url-1 = {https://doi.org/10.1109/MEMCOD.2003.1210110}
}

FICS 2002

A note on global induction in a mu-calculus with explicit approximations

Christoph Sprenger, and Mads Dam

In Fixed Points in Computer Science, FICS 2002, Copenhagen, Denmark, 20-21 July 2002, Preliminary Proceedings, 2002

Bib PDF

@inproceedings{DBLP:conf/fics/SprengerD02,
  author = {Sprenger, Christoph and Dam, Mads},
  booktitle = {Fixed Points in Computer Science, {FICS} 2002, Copenhagen, Denmark, 20-21 July 2002, Preliminary Proceedings},
  editor = {{\'{E}}sik, Zolt{\'{a}}n and Ing{\'{o}}lfsd{\'{o}}ttir, Anna},
  pages = {22--24},
  publisher = {University of Aarhus},
  series = {{BRICS} Notes Series},
  title = {A note on global induction in a mu-calculus with explicit approximations},
  volume = {{NS-02-2}},
  year = {2002}
}

TACAS 1998

A Verified Model Checker for the Modal \(\mathrmμ\)-calculus in Coq

Christoph Sprenger

In Tools and Algorithms for Construction and Analysis of Systems, 4th International Conference, TACAS ’98, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS’98, Lisbon, Portugal, March 28 - April 4, 1998, Proceedings, 1998

Bib HTML PDF

@inproceedings{DBLP:conf/tacas/Sprenger98,
  author = {Sprenger, Christoph},
  booktitle = {Tools and Algorithms for Construction and Analysis of Systems, 4th International Conference, {TACAS} '98, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS'98, Lisbon, Portugal, March 28 - April 4, 1998, Proceedings},
  doi = {10.1007/BFb0054171},
  editor = {Steffen, Bernhard},
  pages = {167--183},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  title = {A Verified Model Checker for the Modal {\(\mathrm{\mu}\)}-calculus in Coq},
  url = {https://doi.org/10.1007/BFb0054171},
  volume = {1384},
  year = {1998},
  bdsk-url-1 = {https://doi.org/10.1007/BFb0054171}
}

SCIDDLE: A Tool for Large Scale Cooperative Computing

Peter Arbenz, Hans Peter Lüthi, Christoph Sprenger, and Stefan Vogel

In High-Performance Computing and Networking, International Conference and Exhibition, HPCN Europe 1994, Munich, Germany, April 18-20, 1994, Proceedings, Volume II: Networking and Tools, 1994

Bib HTML

@inproceedings{DBLP:conf/hpcn/ArbenzLSV94,
  author = {Arbenz, Peter and L{\"{u}}thi, Hans Peter and Sprenger, Christoph and Vogel, Stefan},
  booktitle = {High-Performance Computing and Networking, International Conference and Exhibition, {HPCN} Europe 1994, Munich, Germany, April 18-20, 1994, Proceedings, Volume {II:} Networking and Tools},
  doi = {10.1007/3-540-57981-8\_138},
  editor = {Gentzsch, Wolfgang and Harms, Uwe},
  pages = {326--327},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  title = {{SCIDDLE:} {A} Tool for Large Scale Cooperative Computing},
  url = {https://doi.org/10.1007/3-540-57981-8\_138},
  volume = {797},
  year = {1994},
  bdsk-url-1 = {https://doi.org/10.1007/3-540-57981-8%5C_138}
}

Technical Reports

Pushing the Limit: Verified Performance-Optimal Causally-Consistent Database Transactions

Shabnam Ghasemirad, Christoph Sprenger, Si Liu, Luca Multazzu, and David Basin

2024

arXiv Bib

@techreport{DBLP:journals/corr/abs-2411-07049,
  author = {Ghasemirad, Shabnam and Sprenger, Christoph and Liu, Si and Multazzu, Luca and Basin, David},
  title = {Pushing the Limit: Verified Performance-Optimal Causally-Consistent Database Transactions},
  year = {2024},
  doi = {10.48550/ARXIV.2411.07049},
  eprint = {2411.07049},
  eprinttype = {arXiv},
  archiveprefix = {arXiv},
  journal = {CoRR},
  primaryclass = {cs.DB},
  volume = {abs/2411.07049}
}

Formal Verification of the Sumcheck Protocol

Azucena Garvı́a Bosshard, Jonathan Bootle, and Christoph Sprenger

2024

arXiv Bib

@techreport{DBLP:journals/corr/abs-2402-06093,
  author = {Bosshard, Azucena Garv{\'{\i}}a and Bootle, Jonathan and Sprenger, Christoph},
  bibsource = {dblp computer science bibliography, https://dblp.org},
  biburl = {https://dblp.org/rec/journals/corr/abs-2402-06093.bib},
  date-added = {2024-03-11 12:47:49 +0100},
  date-modified = {2024-03-11 12:47:49 +0100},
  doi = {10.48550/ARXIV.2402.06093},
  eprint = {2402.06093},
  eprinttype = {arXiv},
  journal = {CoRR},
  timestamp = {Fri, 16 Feb 2024 13:00:19 +0100},
  title = {Formal Verification of the Sumcheck Protocol},
  url = {https://doi.org/10.48550/arXiv.2402.06093},
  volume = {abs/2402.06093},
  year = {2024},
  bdsk-url-1 = {https://doi.org/10.48550/arXiv.2402.06093}
}

Protocols to Code: Formal Verification of a Next-Generation Internet Router

João C. Pereira, Tobias Klenze, Sofia Giampietro, Markus Limbeck, Dionysios Spiliopoulos, Felix A. Wolf, Marco Eilers, Christoph Sprenger, David Basin, Peter Müller, and Adrian Perrig

2024

arXiv Bib

@techreport{arXiv.2405.06074,
  author = {Pereira, João C. and Klenze, Tobias and Giampietro, Sofia and Limbeck, Markus and Spiliopoulos, Dionysios and Wolf, Felix A. and Eilers, Marco and Sprenger, Christoph and Basin, David and Müller, Peter and Perrig, Adrian},
  doi = {10.48550/arXiv.2405.06074},
  eprint = {2405.06074},
  eprinttype = {arXiv},
  journal = {CoRR},
  title = {Protocols to Code: Formal Verification of a Next-Generation Internet Router},
  url = {https://doi.org/10.48550/arXiv.2405.06074},
  volume = {abs/2405.06074},
  year = {2024},
  bdsk-url-1 = {https://doi.org/10.48550/arXiv.2405.06074}
}

Sound Verification of Security Protocols: From Design to Interoperable Implementations (extended version)

Linard Arquint, Felix A. Wolf, Joseph Lallemand, Ralf Sasse, Christoph Sprenger, Sven N. Wiesner, David A. Basin, and Peter Müller

2022

arXiv Bib

@techreport{DBLP:journals/corr/abs-2212-04171,
  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},
  doi = {10.48550/arXiv.2212.04171},
  eprint = {2212.04171},
  eprinttype = {arXiv},
  journal = {CoRR},
  title = {Sound Verification of Security Protocols: From Design to Interoperable Implementations (extended version)},
  url = {https://doi.org/10.48550/arXiv.2212.04171},
  volume = {abs/2212.04171},
  year = {2022},
  bdsk-url-1 = {https://doi.org/10.48550/arXiv.2212.04171}
}

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

2020

arXiv Bib

@techreport{DBLP:journals/corr/abs-2010-04749,
  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.},
  eprint = {2010.04749},
  eprinttype = {arXiv},
  journal = {CoRR},
  title = {Igloo: Soundly Linking Compositional Refinement and Separation Logic for Distributed System Verification},
  volume = {abs/2010.04749},
  year = {2020},
}

Proxy Certificates: The Missing Link in the Web’s Chain of Trust

Laurent Chuat, AbdelRahman Abdou, Ralf Sasse, Christoph Sprenger, David A. Basin, and Adrian Perrig

2019

arXiv Bib

@techreport{DBLP:journals/corr/abs-1906-10775,
  author = {Chuat, Laurent and Abdou, AbdelRahman and Sasse, Ralf and Sprenger, Christoph and Basin, David A. and Perrig, Adrian},
  eprint = {1906.10775},
  eprinttype = {arXiv},
  journal = {CoRR},
  title = {Proxy Certificates: The Missing Link in the Web's Chain of Trust},
  volume = {abs/1906.10775},
  year = {2019},
}

Cryptographically Sound Theorem Proving

Christoph Sprenger, Michael Backes, David A. Basin, Birgit Pfitzmann, and Michael Waidner

2006

IACR Cryptol. ePrint Arch.

Bib HTML

@techreport{DBLP:journals/iacr/SprengerBBPW06,
  author = {Sprenger, Christoph and Backes, Michael and Basin, David A. and Pfitzmann, Birgit and Waidner, Michael},
  journal = {{IACR} Cryptol. ePrint Arch.},
  note = {{IACR} Cryptol. ePrint Arch.},
  pages = {47},
  title = {Cryptographically Sound Theorem Proving},
  url = {http://eprint.iacr.org/2006/047},
  year = {2006},
  bdsk-url-1 = {http://eprint.iacr.org/2006/047}
}

Theses

Deductive Local Model Checking – On the Verification of CTL* Properties of Infinite-State Reactive Systems

Christoph Sprenger

EPFL, Lausanne, Switzerland, 2000

PhD thesis

Bib PDF

@phdthesis{Sprenger2000,
  author = {Sprenger, Christoph},
  note = {PhD thesis},
  school = {EPFL, Lausanne, Switzerland},
  title = {Deductive Local Model Checking -- On the Verification of CTL* Properties of Infinite-State Reactive Systems},
  year = {2000}
}