International Association
for Cryptologic Research

In this talk, we report on our experience in producing machine-checked security proofs for cryptographic protocol standards in all their gory detail, and more specifically for Messaging Layer Security (MLS). We outline the methodology we used to tackle this beast of a protocol, talk about the formal verification tools we developed along the way, and give some insights on protocol design, analysis, and standardization that we learned during this journey.