Tidy prover

Tidy was initially the name of a framework introduced in one of my publications, to specify security protocols whose security relies on time-based mechanisms (timeouts, verifiable delay functions...). I have been working on a tool based on these contributions during my post-doc at the Max-Planck Institute, and now develop and maintain it as a personal project.

The tool acts as a front-end to the Tamarin prover, a well-established protocol analyser that does not support quantitative notions such as time. The Tidy prover uses its own (rich, typed, and timed) language, compiles it into a Tamarin specification. It then handles various rounds of interaction with Tamarin to construct an analysis of time-based protocols soundly.

The DeepSec prover

DeepSec (not the smartest name due to all of the homonyms and paronyms...) is a project contributed a lot during my thesis and the following years. This tool was designed as an analysor of privacy-type properties in security protocols with better performances and scope than its competitor at the time. I typically helped shaping the theory behind the tool, and contributed to the design and implementation of optimisation techniques that are now integrated.

I happened to record my PhD defence, which includes a 5min demo of the tool's interface (see the extract below).

The Everest Project

This long-term project (here) carried among others by Microsoft Research and Inria, focuses at producing formally verified implementations of the https ecosystem, mostly using the F* proof assistant. This includes protocols such as TLS but also the IETF version of the QUIC protocol; I contributed to proofs of correctness and security of the latter (mostly of its packet encryption) in 2019.

Scientific popularisation