My research interests mainly focus on formal methods for security and privacy. I design new verification techniques, algorithms and tools to effectively and efficiently analyze formal security properties. I generally enjoy research projects that combine both foundational contributions and practical applications, including analyzing real-world cryptographic protocols.
Download my CV (PDF)
[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).
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.
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.
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).
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.