Analysing Real-world Protocols for Secure Group Messaging

安全的组消息传递协议允许一组人使用端到端加密在不安全的链路上安全地通信。直到最近，文献中安全消息传递的设计和分析都集中在双方消息传递协议上。在过去的几年中，出现了许多新的安全组消息传递协议，其中许多是作为消息传递层安全标准化过程的输入。然而，早在2014年，Matrix[0]、WhatsApp[1]和Signal[2]等应用程序就在其群消息产品中提供了端到端加密。这些系统的设计与近年来引进的系统有很大的不同。在本论文中，我们旨在回答以下问题：1。当前安全组消息传递应用程序的安全目标是什么？这些设计与文献中的设计有何不同？*我们调查了真实世界安全组消息传递应用程序的文档和规范，以确定这些应用程序的目标安全保证。*我们确定了一个新的安全模型，面向设备的组消息传递，以捕获这些协议的预期功能和安全保证。2. 现实世界中的安全组消息传递协议在实践中实现了这些安全目标吗？*我们的分析重点是矩阵，我们分析其规格和实现，以确定他们是否达到这些保证。*我们提出了针对Matrix的设计和实现的实际可利用的攻击，建议对协议及其实现进行改进，以纠正这些问题。*我们在面向设备的组消息模型中提供安全证明，确定这些协议提供的精确安全保证。通过这个过程，我们确定了在实践中部署的组消息传递协议的安全性与文献中提供的结构之间的一些差距。我们注意到一些实际的考虑因素，这些考虑因素导致了具有非最佳安全性的实际部署，并考虑如何在不牺牲安全性的情况下解决此类问题。我们的方法结合了可证明的安全性，遵循Bellare和Rogaway在b[3]中描述的基于代码的游戏方法，以及基于其实现的协议描述。(0) https://matrix.org/(1) https://www.whatsapp.com/(2) https://signal.org/(3) https://eprint.iacr.org/2004/331.pdf

Secure group messaging protocols allow groups of people to communicate securely over an insecure link, using end-to-end encryption.Until recently, the design and analysis of secure messaging in the literature has focused on two-party messaging protocols. The past few years has seen a number of new secure group messaging protocols being introduced, many as input into the Messaging Layer Security standardisation process.However, applications such as Matrix [0], WhatsApp [1] and Signal [2] have provided end-to-end encryption in their group messaging products since as early as 2014. The design of these systems differ considerablyfrom those being introduced in current years. In this thesis we aim to answer the following questions: 1. What are the security goals that current secure group messaging applications aim for? How do these differ from designs in the literature? * We survey the documentation and specifications of real-world secure group messaging applications to determine the security guarantees that these applications aim for. * We identify a new security model, Device-Oriented Group Messaging, to capture both the intended functionality and security guarantees of such protocols. 2. Do real-world secure group messaging protocols achieve these security goals in practice? * Focusing our analysis on Matrix, we analyse both its specification and implementation to determine whether they achieve these guarantees. * We present practically-exploitable attacks against Matrix's design and implementation, suggesting improvements to the protocol and its implementation that would remediate these issues. * We present security proofs, within the Device-Oriented Group Messaging model, determining the precise security guarantees these protocols provide.Through this process we identify a number of gaps between the security of group messaging protocols as they are deployed in practice and constructions provided in the literature. We note a number of practicalconsiderations that have lead to real-world deployments with non-optimal security, and consider how such problems might be solved without sacrificing security.Our approach combines provable security, following the code-based game-playing approach described by Bellare and Rogaway in [3], with protocol descriptions based upon their implementations.(0) https://matrix.org/(1) https://www.whatsapp.com/(2) https://signal.org/(3) https://eprint.iacr.org/2004/331.pdf