See also on dblp and G Scholar

. A method for unbounded verification of privacy-type properties. JCS (journal), 2019.

Preprint PDF Tool

. Symbolic Analysis of Identity-Based Protocols. CathyFest Workshop, LNCS X., 2019.

PDF Models

. A Formal Analysis of 5G Authentication. CCS, 2018.

PDF Slides Extended version DOI Media coverage Models

. A Reduced Semantics for Deciding Trace Equivalence. LMCS (journal), 2017.


. Mobile subscriber WiFi privacy. Security & Privacy Workshops (MoST), 2017.

PDF Best paper award Models

. A method for verifying privacy-type properties: the unbounded case. Security & Privacy (Oakland), 2016.

PDF Slides DOI Tool Models

. Towards Completeness via Proof Search in the Linear Time μ-calculus. LICS, 2016.


. Partial Order Reduction for Security Protocols. CONCUR, 2015.

PDF Slides DOI Code


I have reviewed papers for CSF, Euro S&P, CCS, POST (ETAPS), the Journal of Computer Security (JCS) and the journal LNCS Transactions on Petri Nets and Other Models of Concurrency (ToPNOC).

I have participated to the following projects: joint project between Huawei Technologies Singapore Research Center and ETH Zürich on 5G protocols, ERC Starting Grant POPSTAR, ANR project Sequoia, ANR project ProSe, ANR JCJC project VIP.



Porridge is a standalone OCaml library implementing Partial Order Reduction techniques for checking trace equivalence of security protocols. It is not restricted to the limited class of action-deterministic protocols as in prior works. It has been successfully integrated into two state-of-the-art verifiers DeepSec and Apte, bringing significant speedups. Theory and practical results are described in our ESORICS’18 paper.


UKano is a tool that enables the automatic formal verification of unlinkability and anonymity for a large class of 2-agents protocols that was previously out of scope. It has been notably used to discover new attacks on ePassport protocols. I have written this tool by leveraging our new verification method proposed in our S&P’16 paper.

Partial Order Reduction Techniques in APTE

I have developed and implemented Partial Order Reduction techniques for a class of security protocols (those that are action-deterministic) in the tool Apte, dramatically improving its practical impact. I also have implemented a preliminary version of those techniques in the tool SPEC (more details).


Student Supervisions

  • (2018-2019) Guillaume Girol (master student) : Formalizing and verifying the security protocols from the noise framework (co-supervision).
  • (2018-2019) Läubli Silvan (bachelor student) : Implementing a public bulletin board for Alethea (co-supervision)
  • (2018-2019) Andris Suter-Dörig (bachelor student) : Formalizing and verifying the security protocols from the noise framework (co-supervision)
  • (2018) Falconieri Vincent (master student working as an academic assistant (Hiwi)): Fuzzing authentication protocols in LTE (co-supervision)
  • (2017-2018) Vincent Stettler (master student working as an academic assistant (Hiwi)) : NextGen Network Security Analysis (co-supervision)
  • (2017) David Lanzenberger (bachelor student) : Formal Analysis of 5G Protocols (co-supervision)

Teaching at ETH Zürich

Teaching during my PhD at ENS Cachan

  • Responsible of the course on the theorem prover Coq & SAT-Solving,
  • TA for Logic, Software Engineering, Computability, Computer Programming & Compilation.

More details can be found on my old website at ENS Cachan.

A comprehensive list of my talks (from <2017) can be found on my website at ENS Cachan.

[Invited talk] Doctoral Dissertation Award
May 31, 2018 5:35 PM
[Invited Talk] Cryptographic Flaw in the AKA Protocol - Locate, Track and Monitor Mobile Users
Jul 27, 2017 12:00 AM
PhD Defense
Apr 21, 2017 10:00 AM