The Matrix Reloaded: A Mechanized Formal Analysis of the Matrix Cryptographic Suite

TL;DR

The paper presents a formal, symbolic analysis of Matrix's Olm and Megolm protocols using automated tools (ProVerif and Verifpal), constructing first-of-their-kind symbolic models for Olm, Megolm, and their composition, and comparing their security guarantees to Signal and Sender Keys. It mechanically proves confidentiality, authentication, forward secrecy, and post-compromise security for Olm/Megolm (under signed pre-keys) while reproducing known attacks (e.g., unknown key-share) and illustrating post-compromise weaknesses when pre-keys are unsigned. The work highlights critical security tradeoffs in federated group messaging, showing that signing Olm pre-keys aligns Matrix's security with Signal/Sender Keys, whereas unsigned pre-keys lead to weaker post-compromise security, and it discusses the Sender Keys extension and MLS-related directions. The results underscore the value of mechanized proofs for cryptographic protocols in federated systems and motivate further formal verification and tooling development for secure group messaging.

Abstract

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.

Figures (5)

• Figure 1: Complete Olm Protocol including optional pre-key signing, describing the initialization and transmission of two messages. Brackets around a message in transit indicates off-band verification, where an attacker can observe but not modify the message.
• Figure 2: Complete Megolm/Sender Keys protocol, communicating 3 messages between Alice and Bob. Note, the constructions of Megolm and Sender Keys are the same besides (1) different ratcheting algorithms, and (2) different secure P2P channel protocols.
• Figure 3: Post-compromise attacker sequence on unsigned Olm key exchange, as described in \ref{['sub:Olm PCS without pre-key signing']}
• Figure 4: Post-compromise attacker sequence on unsigned Olm & Megolm composition, as described in \ref{['sub:OlmMegolm PCS attack']}
• Figure 5: Complete Signal Protocol