Formal Analysis of Multi-Device Group Messaging in WhatsApp

Martin R. Albrecht; Benjamin Dowling; Daniel Jones

Paper 2025/794

Formal Analysis of Multi-Device Group Messaging in WhatsApp

Martin R. Albrecht, King’s College London

Benjamin Dowling

, King’s College London

Daniel Jones

, Royal Holloway University of London

Abstract

WhatsApp provides end-to-end encrypted messaging to over two billion users. However, due to a lack of public documentation and source code, the specific security guarantees it provides are unclear. Seeking to rectify this situation, we combine the limited public documentation with information we gather through reverse-engineering its implementation to provide a formal description of the subset of WhatsApp that provides multi-device group messaging. We utilise this description to state and prove the security guarantees that this subset of WhatsApp provides. Our analysis is performed within a variant of the Device-Oriented Group Messaging model, which we extend to support device revocation. We discuss how to interpret these results, including the security WhatsApp provides as well as its limitations.

Metadata

Available format(s): PDF
Category: Applications
Publication info: A major revision of an IACR publication in EUROCRYPT 2025
DOI: 10.1007/978-3-031-91101-9_9
Keywords: Secure Messaging Group Messaging Post-Compromise Security Device Management WhatsApp Sender Keys Revocation
Contact author(s): martin albrecht @ kcl ac uk
benjamin dowling @ kcl ac uk
dan jones @ rhul ac uk
History: 2025-05-05: approved; 2025-05-04: received; See all versions
Short URL: https://ia.cr/2025/794
License: CC0

BibTeX

@misc{cryptoeprint:2025/794,
      author = {Martin R. Albrecht and Benjamin Dowling and Daniel Jones},
      title = {Formal Analysis of Multi-Device Group Messaging in {WhatsApp}},
      howpublished = {Cryptology {ePrint} Archive, Paper 2025/794},
      year = {2025},
      doi = {10.1007/978-3-031-91101-9_9},
      url = {https://eprint.iacr.org/2025/794}
}