iiinova — where your digital self keeps evolving

Théophile Wallez @twal.org · 25/07/2026

If you are interested, please read the paper, or contact me if you have any questions!

Théophile Wallez @twal.org · 25/07/2026

Finally, in term of proof engineering, DyLean is embedded in Lean rather than F*, and hence benefits from a great interactive mode, rather than black-box SMT automation. And thanks to Lean's grind tactic, DyLean proofs are actually as automated as DY* proofs.

100

Théophile Wallez @twal.org · 25/07/2026

This is unlike protocols specified in DY* that can only be proved with DY*, and this opens the way to explore different proof methodologies on the same protocol specification.

100

Théophile Wallez @twal.org · 25/07/2026

Furthermore, in DyLean, the symbolic semantics (to specify cryptographic protocols and their expected security properties) are completely separated from the proof method (to prove security properties indeed hold): our proof method is a suggestion on how to achieve your proof, not a restriction.

100

Théophile Wallez @twal.org · 25/07/2026

Instead, in DyLean, the semantics are fully user-extensible. In fact, we provide a framework to define symbolic semantics. Support for specific cryptographic functions are not hardcoded into the tool, but available as a standard library, and can be defined by DyLean users.

100

Théophile Wallez @twal.org · 25/07/2026

The semantics of the symbolic model are hardcoded in DY*: this inherently limits the expressivity of DY*. For example, the set of cryptographic functions available to specify protocols is fixed in DY*: if you need a cryptographic function outside this set, you cannot use DY*.

100

Théophile Wallez @twal.org · 25/07/2026

DyLean builds on ideas from DY*, and as such inherits from all the improvements I proposed in my latest paper, including the ability to compose security proofs in many scenarios. But DyLean also improves on DY* in many ways!

100

Théophile Wallez @twal.org · 25/07/2026

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.

272

Théophile Wallez @twal.org · 04/03/2025

In the paper, we provide a detailed yet accessible description of TreeKEM internals (Section 2). If you always wanted to know how TreeKEM works but were too scared to read the huge and intimidating RFC, this is another reason to read the paper! eprint.iacr.org/2025/410

010

Théophile Wallez @twal.org · 04/03/2025

In turn, our security theorem implies many nice properties on TreeKEM's shared secret, such as forward secrecy and post-compromise security. Furthermore, the security theorem can be audited and provides insights on the secure deployments of MLS, that we reported to the MLS Working Group.

100

Théophile Wallez @twal.org · 04/03/2025

Our theorem consider an active attacker that may steal secret keys of the group participants (e.g. if a smartphone is scanned at a border control). We prove that if an attacker knows TreeKEM's shared secret, they must have stolen some participant's secret keys (and tell precisely which secret keys).

110

Théophile Wallez @twal.org · 04/03/2025

In this paper, we provide a machine-checked security proof for TreeKEM. To our knowledge, this is the first machine-checked security proof for a group key exchange in the context of dynamic groups (participants can join and leave). Furthermore, our specification is bit-precise and interoperable!

110

Théophile Wallez @twal.org · 04/03/2025

TreeKEM is a sub-protocol of MLS in charge of establishing a shared secret keys between participants of a group, which is then used by another sub-protocol to encrypt messages. Hence, the strong confidentiality guarantees provided by MLS rely on the strong secrecy of TreeKEM's shared secret.

110

Théophile Wallez @twal.org · 04/03/2025

MLS is a recent secure group messaging protocol designed to handle large groups while providing strong confidentiality guarantees, such as forward secrecy and post-compromise security (more on these notions here www.twal.org/blog/0001_wh... ).

100

Théophile Wallez @twal.org · 04/03/2025

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

153