At the 32nd Usenix Security Symposium in Anaheim CA, a paper on the Messaging Layer Security Protocol, co-authored by our founders Jonathan Protzenko and Karthikeyan Bhargavan, was awarded both the Distinguished Paper Award and the prestigious Internet Defense Prize.

The paper, titled “TreeSync: Authenticated Group Management for Messaging Layer Security”, is authored by Théophile Wallez, Jonathan, Benjamin Beurdouche, and Karthik. It presents a precise, executable, machine-checked formal specification of MLS that shows how MLS can be cleanly decomposed into three components: TreeSync, TreeKEM, and TreeDEM. It then presents a formal security definition for TreeSync and a security proof for this sub-protocol in the Dolev-Yao model.

For a high-level overview of MLS, see our earlier blog post. For a blog post with more graphic details on TreeSync and its proof, stay tuned. If you have questions about MLS and how it can be customized for your use case, reach out.