Christoph Sprenger


Last Name

Sprenger

First Name

Christoph

ORCID

0000-0003-2941-5165

Organisational unit

03634 - Basin, David / Basin, David

Filters

Reset filters

Search Results

Publications 1 - 10 of 43
  • Consensus Refined
    Item type: Journal Article
    Marić, Ognjen; Sprenger, Christoph (2015)
    Archive of Formal Proofs
  • Looping for Good: Cyclic Proofs for Security Protocols
    Item type: Conference Paper
    Linker, Felix Emanuel; Sprenger, Christoph; Cremers, Cas; et al. (2025)
    CCS '25: Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security
    Security protocols often involve loops, such as for ratcheting or for manipulating inductively-defined data structures. However, the automated analysis of security protocols has struggled to keep up with these features. The state-of-the-art often necessitates working with abstractions of such data structures or relies heavily on auxiliary, user-defined lemmas. In this work, we advance the state-of-the-art in symbolic protocol verification by adapting cyclic induction proof systems to the security protocol domain. We introduce reasoning rules for the Tamarin prover for cyclic proofs, enabling new, compact proofs, and we prove their soundness. Moreover, we implement new, simple, and effective proof search strategies that leverage these rules. With these additions, Tamarin can prove many lemmas that previously required, often complex, auxiliary lemmas. We showcase our approach on fourteen case studies, ranging from toy examples to a detailed model of the Signal protocol. Our work opens an exciting new research area where automatic induction helps scale security protocol verification, as we provide a fundamentally new and general induction mechanism
  • Pushing the Limit: Verified Performance-Optimal Causally-Consistent Database Transactions
    Item type: Conference Paper
    Ghasemirad, Shabnam; Sprenger, Christoph; Liu, Si; et al. (2025)
    Lecture Notes in Computer Science ~ Tools and Algorithms for the Construction and Analysis of Systems
    Modern web services crucially rely on high-performance distributed databases, where concurrent transactions are isolated from each other using concurrency control protocols. Relaxed isolation levels, which permit more complex concurrent behaviors than strong levels like serializability, are used in practice for higher performance and availability. In this paper, we present Eiger-PORT+, a concurrency control protocol that achieves a strong form of causal consistency, called TCCv (Transactional Causal Consistency with convergence). We show that Eiger-PORT+ also provides performance-optimal read transactions in the presence of transactional writes, thus refuting an open conjecture that this is impossible for TCCv. We also deductively verify that Eiger-PORT+ satisfies this isolation level by refining an abstract model of transactions. This yields the first deductive verification of a complex concurrency control protocol. Furthermore, we conduct a performance evaluation showing Eiger-PORT+ ’s superior performance over the state-of-the-art.
  • Protocols to Code: Formal Verification of a Secure Next-Generation Internet Router
    Item type: Conference Paper
    Pereira, João C.; Klenze, Tobias; Giampietro, Sofia; et al. (2025)
    CCS '25: Proceedings of the 2025 on ACM SIGSAC Conference on Computer and Communications Security
    We present the first formally-verified Internet router, which is part of the SCION Internet architecture. SCION routers run a cryptographic protocol for secure packet forwarding in an adversarial environment. We verify both the protocol’s network-wide security properties and the low-level properties of its implementation. Namely, we develop a series of protocol models by refinement in Isabelle/HOL and we use an automated program verifier to prove that the router’s Go code satisfies crash freedom, freedom from data races, and adheres to the most concrete model in our series of refinements. Both verification efforts are soundly linked together. Our work demonstrates the feasibility of coherently verifying a security-critical network component from high-level protocol models down to performance-optimized production code, developed by an independent team. In the process, we uncovered critical attacks and bugs in both the protocol and its implementation, which were confirmed by the code developers, and we strengthened the protocol’s security properties. This paper presents the challenges we faced when verifying an existing real-world system, explains our approach to tackling these challenges, summarizes the main results, and distills valuable lessons for the verification of secure systems, in particular for the techniques and tools employed.
  • Developing Security Protocols by Refinement
    Item type: Report
    Sprenger, Christoph; Basin, David (2013)
    D-INFK Technical Report
    We propose a development method for security protocols based on stepwise refinement. Our refinement strategy transforms abstract security goals into protocols that are secure when operating over an insecure channel controlled by a Dolev-Yao-style intruder. As intermediate levels of abstraction, we employ message-less guard protocols and channel protocols communicating over channels with security properties. These abstractions provide insights on why the protocols are secure and foster the development of families of protocols sharing common structure and properties. We have implemented our method in Isabelle/HOL and used it to develop different entity authentication and key establishment protocols. These protocols include realistic features such as key confirmation, replay caches, and encrypted tickets. Our development highlights that guard protocols and channel protocols provide fundamental abstractions for bridging the gap between security properties and standard protocol descriptions based on cryptographic messages. It also shows that our refinement approach scales to protocols of nontrivial size and complexity.
  • A Monad-Based Modeling and Verification Toolbox with Application to Security Protocols
    Item type: Conference Paper
    Sprenger, Christoph; Basin, David (2007)
    Lecture Notes in Computer Science ~ Theorem proving in higher order logics : proceedings : 20th international conference
  • Abstractions for security protocol verification
    Item type: Report
    Nguyen, Binh Thanh; Sprenger, Christoph (2014)
    We present a large class of security protocol abstractions with the aim of improving the scope and efficiency of verification tools. We present type-based abstractions, which use a term’s type to uniformly select the kind of abstraction applied, as well as untyped abstractions, which enable the removal of atomic messages, variables, and redundant terms. We extend existing work in the area by supporting additional abstractions, user-defined types, and untyped variables to cover type flaw attacks. We prove soundness results for an expressive property language that includes secrecy and authentication. Applying our abstractions to a set of realistic IETF protocol models, we achieve dramatic speedups and extend the scope of several modern security protocol analyzers.
  • Sound Verification of Security Protocols: From Design to Interoperable Implementations
    Item type: Conference Paper
    Arquint, Linard; Wolf, Felix; Lallemand, Joseph; et al. (2023)
    2023 IEEE Symposium on Security and Privacy (SP)
    We provide a framework consisting of tools and metatheorems for the end-to-end verification of security protocols, which bridges the gap between automated protocol verification and code-level proofs. We automatically translate a Tamarin protocol model into a set of I/O specifications expressed in separation logic. Each such specification describes a protocol role's intended I/O behavior against which the role's implementation is then verified. Our soundness result guarantees that the verified implementation inherits all security (trace) properties proved for the Tamarin model. Our framework thus enables us to leverage the substantial body of prior verification work in Tamarin to verify new and existing implementations. The possibility to use any separation logic code verifier provides flexibility regarding the target language. To validate our approach and show that it scales to realworld protocols, we verify a substantial part of the official Go implementation of the WireGuard VPN key exchange protocol.
  • Refining Key Establishment
    Item type: Conference Paper
    Sprenger, Christoph; Basin, David (2012)
    2012 IEEE 25th Computer Security Foundations Symposium (CSF)
  • Cutoff Bounds for Consensus Algorithms
    Item type: Conference Paper
    Marić, Ognjen; Sprenger, Christoph; Basin, David (2017)
    Lecture Notes in Computer Science ~ Computer Aided Verification
Publications 1 - 10 of 43