We’re pleased to announce that we are engaging with INRIA Paris to cooperate on OpenMLS.
Professor Karthikeyan Bhargavan’s Prosecco team at INRIA decisively contributed to the formally verified cryptographic library HACL* (along with Microsoft Research and CMU) and was deeply involved in the design, analysis and standardization of TLS 1.3. More recently, the team published TreeKEM – the core algorithm of MLS.
While OpenMLS already builds on top of formally verified cryptography in HACL*, the cooperation covers new areas, such as exchanging knowledge and findings in the API design, code structure, real-world performance and usability concerns and last but not least exploring the idea of formally verifying parts of OpenMLS in the longer term.