Cryspen on Mythryl: “At IEEE S&P, Théophile Wallez presented new results on the formal…”

At IEEE S&P, Théophile Wallez presented new results on the formal security verification of a bit-precise executable specification of TreeKEM, the core key agreement component of the MLS protocol. This work was done in collaboration with chief research scientist Karthikeyan Bhargavan.

buff.lyTreeKEM: A Modular Machine-Checked Symbolic Security Analysis of Group Key Agreement in Messaging Layer SecurityThe 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…

10/6/25, 1:20 pm0 reposts0 likes

Post