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预密钥未签名，则其后渗透安全性可证明地更差。