Analyzing Group Chat Encryption in Messaging Applications

This talk details a formal security analysis of group chat encryption algorithms in popular messaging applications like MLS, Session, and Keybase. It introduces Symmetric Sign Encryption (SSE) to model these protocols, identifying critical vulnerabilities such as insider replay and reordering attacks in MLS and Session due to insufficient context binding. The analysis highlights the complexities of key-dependent messages and key reuse, demonstrating how formal methods can pinpoint subtle design flaws and suggest robust mitigations for real-world secure communication.