The Matrix Reloaded: A Mechanized Formal Analysis of the Matrix Cryptographic Suite
Jacob Ginesin, Cristina Nita-Rotaru

TL;DR
This paper presents a formal, mechanized analysis of the cryptographic protocols Olm and Megolm used in Matrix, demonstrating their security properties and limitations through computer-aided proofs, and comparing them to Signal's protocols.
Contribution
It provides the first formal, mechanized proofs of Olm and Megolm, revealing their security strengths and weaknesses, and compares their security to Signal's protocols.
Findings
Olm and Megolm achieve authentication, confidentiality, and forward secrecy.
Signed Olm pre-keys improve post-compromise security.
Unsigning Olm pre-keys results in worse post-compromise security.
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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsCryptographic Implementations and Security · Chaos-based Image/Signal Encryption · Coding theory and cryptography
