avatar

About Me

I am Felix Linker, a postdoc in the Information Security and Network Security groups at ETH Zurich, independent consultant, and one of the leading experts for the Tamarin prover, a state-of-the-art protocol verifier. I obtained my Doctorate in that same research group in 2025.

I develop security critical systems, and I conduct formal analyses to prove security guarantees of such systems. Not only does formal analysis enhance the confidence in a system’s security, formal analysis also requires explicit adversary assumptions and desired security guarantees, which can often times be as valuable as the security proofs.

Please reach out if you are interested in a collaboration! Next to the design and formal analysis of security critical systems, I offer Tamarin training and have hosted many workshops on the tool.

Projects

Formal Analysis of iMessage PQ3

In 2024, Apple announced their update of the iMessage message encryption protocol to iMessage PQ3, adding protecting against quantum attackers to the protocol. Prior to release, Apple shared the protocol specification with us, and we formally proved iMessage PQ3’s security against a quantum attacker using the Tamarin prover, something that was previously believed to be impossible.

See the publication and presentations for more details.

Digital Emblems

I help the International Committee of the Red Cross (ICRC) with the development and standardization of a Digital Emblem. A Digital Emblem is the digital equivalent to the physical emblems recognized under International Humanitarian Law (IHL), in particular, the Red Cross, Red Crescent, and Red Crystal. It serves to signal that a digital asset enjoys a special status under IHL and should respected and protected. I advise the ICRC, for example, at the IETF.

Our collaboration started with the development of ADEM: An Authentic Digital Emblem (see the respective publication and GitHub). ADEM has since then been selected as the official prototype for a Digital Emblem by the ICRC, and was featured in the ICRC’s report on Digitalizing the Red Cross, Red Crescent and Red Crystal Emblems. In July 2026, the ICRC launched Phase II of the Digital Emblem project, at which ADEM was also demoed. You can learn more about the Digital Emblem project here.

Key Transparency

I am a co-author of a key transparency draft that is being standardized at the IETF. We currently work on the formal analysis of the draft using the program verifier Gobra.

SecureDrop

I helped Freedom of the Press Foundation with the requirements engineering, design, and formal analysis of an end-to-end encrypted version of the SecureDrop protocol. SecureDrop is a whisteblowing platform that has been deployed at the New York Times, The Guardian, The Washington Post, and many more news outlets. Previously, SecureDrop relied on a secure deployment, e.g., on premises. The new SecureDrop protocol is an end-to-end encryption protocol that removes trust assumptions from the deployment so that it can also be deployed in the cloud, for example.

See the publication and presentations for more details.

Cyclic Induction for the Tamarin Prover

We developed and implemented a new induction scheme for the Tamarin prover in the paper “Looping for Good: Cyclic Proofs for Security Protocols.” This induction scheme exploits recurring patterns in Tamarin’s constraint systems and allows us to prove the Signal protocol secure without using any auxiliary lemmas and almost fully automatically. 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, and we plan to further enhance Tamarin’s proof automation using this work in the future.

This work received a Distinguished Paper Award at CCS 2025. See the publication for more details.

Publications