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. Seek- ing to rectify this situation, we combine the limited public documentation with information we gather through reverse-engineering its implemen- tation 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