Secure instant group messaging applications such as WhatsApp, Facebook Messenger, Matrix, and the Signal Application have become ubiquitous in today's internet, cumulatively serving billions of users. Unlike WhatsApp, for example, Matrix can be deployed in a federated manner, allowing users to choose which server manages their chats. To account for this difference in architecture, Matrix employs two novel cryptographic protocols: Olm, which secures pairwise communications, and Megolm, which relies on Olm and secures group communications. Olm and Megolm are similar to and share security goals with Signal and Sender Keys, which are widely deployed in practice to secure group communications. While Olm, Megolm, and Sender Keys have been manually analyzed in the computational model, no symbolic analysis nor mechanized proofs of correctness exist. Using mechanized proofs and computer-aided analysis is important for cryptographic protocols, as hand-written proofs and analysis are error-prone and often carry subtle mistakes. Using Verifpal, we construct formal models of Olm and Megolm, as well as their composition. We prove various properties of interest about Olm and Megolm, including authentication, confidentiality, forward secrecy, and post-compromise security. We also mechanize known limitations, previously discovered attacks, and trivial attacker wins from the specifications and previous literature. Finally, we model Sender Keys and the composition of Signal with Sender Keys in order to draw a comparison with Olm, Megolm, and their composition. From our analysis we conclude the composition of Olm and Megolm has comparable security to the composition of Signal and Sender Keys if Olm pre-keys are signed, and provably worse post-compromise security if Olm pre-keys are not signed.

翻译：诸如 WhatsApp、Facebook Messenger、Matrix 和 Signal 应用等安全的即时群组消息应用在当今互联网中已无处不在，累计服务数十亿用户。与 WhatsApp 等应用不同，Matrix 可以以联邦方式部署，允许用户选择由哪个服务器管理其聊天。为了适应这种架构差异，Matrix 采用了两种新颖的加密协议：用于保障点对点通信安全的 Olm，以及基于 Olm 并保障群组通信安全的 Megolm。Olm 和 Megolm 与 Signal 和 Sender Keys 协议相似，并共享其安全目标，后者在实践中被广泛部署以保障群组通信安全。尽管 Olm、Megolm 和 Sender Keys 已在计算模型中进行过人工分析，但目前尚不存在符号分析或机械化的正确性证明。对于加密协议而言，使用机械化证明和计算机辅助分析至关重要，因为手写证明和分析容易出错，且常包含细微错误。我们使用 Verifpal 构建了 Olm 和 Megolm 及其组合的形式化模型。我们证明了 Olm 和 Megolm 的多种重要属性，包括认证性、保密性、前向安全性和后泄露安全性。我们还从规范及先前文献中，机械化地验证了已知限制、先前发现的攻击以及攻击者显而易见的获胜场景。最后，我们建模了 Sender Keys 以及 Signal 与 Sender Keys 的组合，以便与 Olm、Megolm 及其组合进行比较。根据我们的分析，我们得出结论：如果 Olm 预密钥经过签名，则 Olm 与 Megolm 的组合具有与 Signal 和 Sender Keys 组合相当的安全性；如果 Olm 预密钥未签名，则其后泄露安全性可证明更差。