News

Publications

See also on dblp and G Scholar

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

Preprint PDF DOI Tool

. Symbolic Analysis of Identity-Based Protocols. Festschrift Symposium in Honor of Catherine Meadows, LNCS 11565, 2019.

PDF DOI 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.

PDF DOI Code

. 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.

PDF DOI

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

PDF Slides DOI Code

Service

I serve in the program committee of the Computer Security track at the 29th ACM Symposium on Applied Computing (SEC@SAC), 2019.

I have reviewed papers for CCS, CSF, Euro S&P, ESORICS, 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.

Tools

Porridge

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

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).

Teaching

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.

Contact