Secure Group Messaging in Practice: A cryptographic analysis of real-world multi-device group messaging protocols.

Despite applications such as Matrix, WhatsApp and Signal having pro-
vided end-to-end encryption in their group messaging products as early
as 2014, the understanding of how these systems work, and the security
guarantees they provide, has not been well addressed in the academic
literature.

In this thesis, we seek to fill this very gap. We analyse the implementa-
tions, documentation and specifications of two secure group messaging
applications, Matrix and WhatsApp, resulting in a detailed description
of each protocol.

Finding that no existing model effectively captures the relationships
between users, their devices, and the groups they are a part of, we
introduce the device-oriented group messaging model to do just that.
This model aims to capture the common subset of Matrix and WhatsApp
that provides multi-device group messaging. It captures the confidentiality
and authentication these protocols are able to provide, under varying
forms of corruption and state compromise. We, additionally, develop a
variant of this model to capture WhatsApp’s support for cryptographic
device revocation.

During our study of Matrix, we discover vulnerabilities in its design and
implementation, before demonstrating how practically-exploitable attacks
can be built upon them. We suggest improvements to the protocol and
its implementation in order to remediate these issues. We then proceed
to express multi-device group messaging in Matrix within our model, and
prove that, once the aforementioned vulnerabilities have been fixed, this
subset of Matrix provides confidentiality and authentication in certain
conditions. We proceed to prove the security of WhatsApp’s multi-device
group messaging in a similar manner, finding that it too is secure within
our model.

In both cases, we develop security predicates that detail in what situations
our proof of security applies. We discuss how these predicates (and our
results, more generally) can be interpreted in practice. Notably, we
find that both protocols are able to satisfy the core requirements of
confidentiality and authentication under common usage patterns.
While Matrix and WhatsApp provide limited forward secrecy and post-
compromise security guarantees, the same mechanisms that weaken these
guarantees also serve to provide important features, such as history
sharing, or to aid in recovery after desynchronisation errors. On the other
hand, thanks to its support for cryptographic device revocation, we find
that WhatsApp is able to recover after the complete compromise of a
device, provided that a user’s primary device remains secure.

Finally, we highlight Matrix and WhatsApp’s shared lack of cryptographic
membership control: while both protocols guarantee confidentiality within
the members of a group, clients cede control over who these members are
to the server.

Our approach combines provable security, following the code-based game-
playing approach proposed by Bellare and Rogaway, with detailed protocol
descriptions based upon analysis of the implementations they deploy.