Felix Emanuel Linker


Last Name

Linker

First Name

Felix Emanuel

ORCID

0009-0000-7886-4480

Organisational unit

03634 - Basin, David / Basin, David

Filters

2024 - 20254
Reset filters

Search Results

Publications1 - 4 of 4
  • SOAP: A Social Authentication Protocol
    Item type: Conference Paper
    Linker, Felix Emanuel; Basin, David (2024)
    Proceedings of the 33rd USENIX Security Symposium
    Social authentication has been suggested as a usable authentication ceremony to replace manual key authentication in messaging applications. Using social authentication, chat partners authenticate their peers using digital identities managed by identity providers. In this paper, we formally define social authentication, present a protocol called SOAP that largely automates social authentication, formally prove SOAP’s security, and demonstrate SOAP’s practicality in two prototypes. One prototype is web-based, and the other is implemented in the open-source Signal messaging application. Using SOAP, users can significantly raise the bar for compromising their messaging accounts. In contrast to the default security provided by messaging applications such as Signal and WhatsApp, attackers must compromise both the messaging account and all identity provider-managed identities to attack a victim. In addition to its security and automation, SOAP is straightforward to adopt as it is built on top of the well-established OpenID Connect protocol.
  • Protocol Design and Analysis in the Symbolic Model
    Item type: Doctoral Thesis
    Linker, Felix Emanuel (2025)
  • 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
  • A Formal Analysis of Apple's iMessage PQ3 Protocol
    Item type: Conference Paper
    Linker, Felix Emanuel; Sasse, Ralf; Basin, David (2025)
    Proceedings of the 34th USENIX Security Symposium
    We present the formal verification of Apple's iMessage PQ3, a highly performant, device-to-device messaging protocol offering strong security guarantees even against an adversary with quantum computing capabilities. PQ3 leverages Apple's identity services together with a custom, post-quantum secure initialization phase and afterwards it employs a double ratchet construction in the style of Signal, extended to provide post-quantum, post-compromise security. We present a detailed formal model of PQ3, a precise specification of its fine-grained security properties, and machine-checked security proofs using the TAMARIN prover. Particularly novel is the integration of post-quantum secure key encapsulation into the relevant protocol phases and the detailed security claims along with their complete formal analysis. Our analysis covers both key ratchets, including unbounded loops, which was believed by some to be out of scope of symbolic provers like TAMARIN (it is not!).
Publications1 - 4 of 4