avatar

About Me

I am Felix Linker, a Doctoral student in the Information Security group at ETH Zurich, independent consultant, and one of the leading experts for the Tamarin prover, a state-of-the-art protocol verifier.

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. You can find more details in our paper.

Digital Emblems

I help the International Committee of the Red Cross (ICRC) with the requirements engineering, development, and standardization of ADEM, a proposal for a Digital Emblem. I represent the ICRC from a technical point of view, for example, at the IETF.

A Digital Emblem marks digital assets, for example web servers, as protected under International Humanitarian Law - just like the physical emblems of the Red Cross, Red Crescent, and Red Crystal do in the physical world. This work started as a research project during my Doctoral studies and is now transitioning to adoption.

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 help 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. I previously helped supervise a Masters thesis on the formal analysis of SecureDrop, and we currently continue to enhance the design.

Cyclic Induction for the Tamarin Prover

Recently, we developed and implemented a new induction scheme for the Tamarin prover. This induction scheme allowed us to prove the Signal protocol secure without using any auxiliary lemmas and almost fully automatically. This work is currently under submission for scientific publication.

Publications