Formal Verification of Labyrinth in Messenger: Reconsidering Security against Abusing Revoked Device

Messenger, a messaging service, is widely used in the United States and around the world, with 947 million monthly active users as of February 2025. In December 2023, a default implementation of end-to-end encryption in Messenger and two accompanying technical white papers were released. Labyrinth Encrypted Message Storage Protocol is one of the protocols presented in these technical white papers and is intended to securely share message history between devices associated with each Messenger account. However, there has been no rigorous discussion of the security of Labyrinth to date, and the security model claimed in the technical white paper has some ambiguity. In this paper, we give the first formal verification of Labyrinth. First, we verify the confidentiality and integrity of the stored messages as the security claim in the specification (i.e., only considering outside adversaries). Next, considering the case of a device that has been revoked from an account and abused, we exhaustively verify under what conditions it is possible to break the confidentiality and integrity of a message. As a result of the verification, we clarify the conditions under which the confidentiality and integrity of stored messages can be broken by abusing a revoked device and the specific procedures for doing so while satisfying all the security claims made by the specification.