Théophile Wallez

Research & teaching

Publications

Comparse: Provably Secure Formats for Cryptographic Protocols
ACM CCS 2023. [doi] [eprint]
Théophile Wallez Jonathan Protzenko Karthikeyan Bhargavan

TreeSync: Authenticated Group Management for Messaging Layer Security
USENIX Security '23. [USENIX] [eprint]
Théophile Wallez Jonathan Protzenko Benjamin Beurdouche Karthikeyan Bhargavan

This paper won the Internet Defense Prize and received a Distinguished Paper Award.

Standards work

The Messaging Layer Security (MLS) Protocol
IETF RFC (contributor). [datatracker] [rfc]

I am an active participant in the IETF MLS working group, where I authored several key improvements such as the disambiguation of signatures and the strengthening of group membership agreement.

Awards

Co-winner of the 2023 Internet Defense Prize.

Distinguished Paper Award at USENIX Security ‘23.

Service

POPL 2024 (sub-reviewer)

ESOP 2023 (Artifact Evaluation Committee)

Teaching

Systèmes numériques at ENS Paris (Sept. 2023 - Jan 2024)

Systèmes numériques at ENS Paris (Sept. 2022 - Jan 2023)

Systèmes numériques at ENS Paris (Sept. 2021 - Jan 2022)

Talks

Comparse: Provably Secure Formats for Cryptographic Protocols
at ACM CCS 2023. [slides]

This is the 12-minutes talk for the paper “Comparse: Provably Secure Formats for Cryptographic Protocols”, given at ACM CCS 2023.

"Don't roll your own crypto": les méthodes formelles au service de la sécurité
at Devfest Toulouse (in french). [recording] [slides]

I gave a short talk at Devfest Toulouse 2019, giving a brief overview of what formal methods can be used for (aimed at developers who never heard of this).

End-to-End Encrypted Group Chats with MLS: Design, Implementation and Verification
at Microsoft Research (08/2023) ; Cornell Tech (08/2023) ; IRISA (01/2024) ; NYU (03/2024) ; MIT (04/2024). [slides] [slides v2]

This is the long version (45 to 60 minutes) of the talk for the paper “TreeSync: Authenticated Group Management for Messaging Layer Security”, given at various places.

The second version of the slides include a digression on the paper “Comparse: Provably Secure Formats for Cryptographic Protocols”, to explain more deeply what happened behind the signature ambiguity attack.

TreeSync: Authenticated Group Management for Messaging Layer Security
at USENIX Security '23. [slides]

This is the 12-minutes talk for the paper “TreeSync: Authenticated Group Management for Messaging Layer Security”, given at USENIX Security ‘23.

Applications de Brainfuck, langage minimaliste mais Turing-complet
at Devfest Toulouse (in french). [recording] [slides]

I gave a short talk at Devfest Toulouse 2019, explaining how it was humanly possible to write useful Brainfuck programs. After explaining the syntax of the language, I explained some useful code patterns such as conditions or array management, which allow to write complex programs.

Des tuyaux pour se qualifier au baseball
at Informatique pour Tous (in french). [recording] [slides]

I gave a talk that was aimed to explain a computer science notion for high-school student. I decided to explain the max-flow min-cut theorem and the Ford-Fulkerson algorithm, applied on a problem of deciding whether a baseball team can still qualify or not. I definitely lacked a lot of presentation skills (you can count the “euuuuh”), however I think I found the simplest explanations for the max-flow alogrithm.

Internship reports

A verification framework for secure machine learning
Internship for 2nd year of Master's Degree at INRIA, Paris.
With Karthikeyan Bhargavan Prasad Naldurg [PDF] [slides]

I worked five months in the Prosecco team at INRIA. I wrote a global and local specifications for the online phase of the SPDZ2k protocol, and proved that they computed the same thing.

Faster CakeML compilation with a verified linear scan register allocator
Internship for 1st year of Master's Degree at Chalmers, Göteborg (Sweden).
With Magnus Myreen [PDF] [slides]

I worked five months in the CakeML team to implement a verified linear-scan register allocator. The motivation was that the register allocation was the slowest part of the compilation process, hence a faster algorithm could drastically reduce compilation time.

Détection automatique des adresses exploitables d'un algorithme de cryptographie par timing du cache processeur
Internship for 3rd year of Bachelor's Degree at Secure-IC, Paris.
With Sylvain Guilley [PDF] [slides]

I worked two months on cache timing attacks (before Spectre or Meltdown were known). I found a procedure to analyse a cryptographic library and automatically find parts of the code which break secret independance, and might leak a private key to an attacker running on the same computer.