Messaging applications are nowadays pervasively used to communicate with each other, in particular using group conversations to connect people within a social circle. This is a potential threat for privacy, for example if the messaging application servers were to have access to the conversation content. To address this issue, modern messaging applications provide end-to-end encryption, meaning that messages are encrypted by the sender device and decrypted by the receiver device, so that their content stays hidden from the messaging application servers. Such end-to-end encryption is a feature of cryptographic protocols, whose design is notoriously error-prone. This begs the following question: are secure messaging applications actually secure? In this thesis, we develop a novel methodology to analyze the secure group messaging protocol Messaging Layer Security (MLS) by using formal methods on bit-precise specifications in the symbolic model, and ultimately helped to fix design flaws in MLS before its standardization.

The first axis of this thesis is developing tools to analyze cryptographic protocols, on bit-precise specifications. To handle the complexities exhibited by MLS, such as dynamic group size or recursive data structures, we present several key improvements to DY*, a symbolic analysis framework written in the F* proof assistant. To write bit-precise specifications of cryptographic protocols and handle their precise message formats, we introduce Comparse, a tool to specify and prove properties on message formats in F*. In the process, we study the broad class of message formatting attacks, and derive criteria cryptographic protocols should obey to avoid such attacks.

The second axis of this thesis is applying the tools we developed on MLS. We present a novel modularization of MLS to decompose it into three sub-protocols, thereby allowing us to analyze each sub-protocol independently. We then analyze and produce a machine-checked proof for two out of three sub-protocols, TreeSync and TreeKEM. Our specification for MLS is bit-precise, executable and interoperable with other MLS implementations. During our analysis, we found several design flaws and proposed fixes to the Working Group in charge of its design at the Internet Engineering Task Force (IETF), which were integrated in the MLS standard.