News

Publications

See also on dblp and G Scholar

. Verification of Stateful Cryptographic Protocols with Exclusive OR. JCS (journal), 2019.

. 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, ACM TOPS, JCS, etc.

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

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

  • (2019-) Paul Artigouha (master student) : Formalizing and verifying privacy for the security protocols from the Noise framework.
  • (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 Telecom Nancy

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