This talk presents Aegon, a self-auditable key transparency scheme designed for global-scale encrypted messaging. It builds on Iron Dict's polynomial commitment approach to remove per-epoch global work, shards the dictionary for horizontal scaling, and uses proof caching to bound storage. The result is constant-size audit proofs that a lightweight client can verify itself over an entire history, rather than relying on external auditors.
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.