Tessera

Folgen

Théophile Wallez

@twal.org

Post-doc researcher at CISPA, working on secure group messaging & machine-checked security proofs.

15 Posts94 Follower 38 Folgt

Théophile Wallez @twal.org · 2w ago

My latest project, in collaboration with @cascremers.bsky.social, is out! It is Bob DyLean, a framework to analyze cryptographic protocols in the symbolic model, in Lean.

ePrint Updates@eprint.ing.bot · 2w ago

Bob DyLean: A Framework for the Symbolic Analysis of Cryptographic Protocols in Lean (Théophile Wallez, Cas Cremers) ia.cr/2026/1493

Abstract. Over the last decades, symbolic (Dolev-Yao) methods for the analysis of security protocols have proven to be effective to analyze and establish strong guarantees for widely deployed protocols and systems, such as TLS 1.3, E-voting protocols, EMV, and MLS. On the one hand, analysis methods like Tamarin and ProVerif provide automation and support for user-defined equational theories. On the other hand, methods like DY* offer more flexible and modular reasoning, but hardcode threat models and do not support custom equational theories.

We present DyLean, a framework for the symbolic analysis of cryptographic protocols in the Lean theorem prover. Our framework comprises both a flexible general-purpose symbolic semantics, as well as a concrete proof methodology.

DyLean allows defining protocols and expected security properties; its semantics and equational theories can be customized by the user. Furthermore, the semantics are agnostic of the specific proof methodology: our goal is to provide a generic framework that can be used by the community as a foundation to develop various proof methodologies.

Moreover, we provide a concrete proof methodology inspired by DY, based on trace invariants. Thus, DyLean inherits from the qualities of DY: it is able to analyze protocols involving unbounded loops or datastructures, and is able to compose security proofs in a variety of scenarios. Our proof methodology improves on DY* by allowing for user-defined equational theories and threat models. We exercise DyLean on several focused case studies, which include protocols using merkle trees, ratcheting protocols, post-quantum protocols, and protocols analyzed under different equational theories, which demonstrates that DyLean can effectively analyze protocols with each of these features.

Théophile Wallez @twal.org · last yr.

New paper on the formal analysis of TreeKEM is out! Some explanations below. 🧵

ePrint Updates@eprint.ing.bot · last yr.

TreeKEM: A Modular Machine-Checked Symbolic Security Analysis of Group Key Agreement in Messaging Layer Security (Théophile Wallez, Jonathan Protzenko, Karthikeyan Bhargavan) ia.cr/2025/410

Abstract. The Messaging Layer Security (MLS) protocol standard proposes a novel tree-based protocol that enables efficient end-to-end encrypted messaging over large groups with thousands of members. Its functionality can be divided into three components: TreeSync for authenticating and synchronizing group state, TreeKEM for the core group key agreement, and TreeDEM for group message encryption. While previous works have analyzed the security of abstract models of TreeKEM, they do not account for the precise low-level details of the protocol standard. This work presents the first machine-checked security proof for TreeKEM. Our proof is in the symbolic Dolev-Yao model and applies to a bit-level precise, executable, interoperable specification of the protocol. Furthermore, our security theorem for TreeKEM composes naturally with a previous result for TreeSync to provide a strong modular security guarantee for the published MLS standard.