News

  • [March 2020] New paper accepted at Usenix Security 2020. We propose a formal verification framework for the Noise security protocols. We use our framework to automatically infer when and under which circumstances (e.g., for which threat models) each of the relevant Noise security goals holds. Our analysis reveals missing assumptions and several shortcomings in the Noise specification for which we propose fixes.

  • [Summer 2019] The privacy attack on 5G (and also on 3G and 4G) we disclosed in our PETS’19 paper have been added to the list of key issues in 5G authentication (see Technical Report 33.846). Various vendors have proposed to 3GPP several change requests (CRs) with dedicated countermeasures (see the CRs from Qualcomm, Gemalto, ChinaMobile, Thales, Nokia, ZTE, and Huawei).

Publications

See also on dblp and G Scholar

. A Spectral Analysis of Noise: A Comprehensive, Automated, Formal Analysis of Diffie-Hellman Protocols. Usenix Security, 2020.

PDF Tool Models and proofs

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

Preprint PDF DOI Code

. 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 been external scientific experts for the ANR (French National Agency for Research) Generic Call 2019-2020. I have reviewed papers for CCS, CSF, Euro S&P, ESORICS, ACM TOPS, JCS, etc.

I have participated to the following projects: ANR Chair of research and teaching in artificial intelligence (ASAP), joint project between Huawei Technologies Singapore Research Center and ETH Zürich on 5G protocols, ERC Consolidator Grant SPOOC, ERC Starting Grant POPSTAR, various ANR projects.

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

  • (2020) Guilhem Roy (master student, École Polytechnique, France): Symbolic-Model-Aware Fuzzing of Cryptographic Protocols.
  • (2020) Timothé Bonhoure (bachelor student, ENS Lyon, France): Improving Cryptographic Protocols Verification: The Best of Two Worlds.
  • (2020) Karan Agarwalla (bachelor student, IIT Bombay, India): Formally Comparing and Evaluating Privacy Properties.
  • (2019-2020) Paul Artigouha (master student, Mines de Nancy, France): Formalizing and verifying privacy for the security protocols from the Noise framework.
  • (2018-2019) Guillaume Girol (master student, École Polytechnique, France): Formalizing and verifying the security protocols from the Noise framework.
  • (2018-2019) Läubli Silvan (bachelor student, ETH Zurich, Switzerland): Implementing a public bulletin board for Alethea.
  • (2018-2019) Andris Suter-Dörig (bachelor student, ETH Zurich, Switzerland): Formalizing and verifying the security protocols from the Noise framework.
  • (2018) Falconieri Vincent (master student working as an academic assistant (Hiwi), ETH Zurich, Switzerland): Fuzzing authentication protocols in LTE.
  • (2017-2018) Vincent Stettler (master student working as an academic assistant (Hiwi), ETH Zurich, Switzerland): NextGen Network Security Analysis.
  • (2017) David Lanzenberger (bachelor student, ETH Zurich, Switzerland): Formal Analysis of 5G Protocols.

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