Automated Symbolic Verification of Telegram's MTProto 2.0

MTProto 2.0 is a suite of cryptographic protocols for instant messaging at the core of the popular Telegram messenger application, which is currently used by more than 400 millions of people. In this paper we analyse MTProto 2.0 using ProVerif, a symbolic cryptographic protocol verifier based on the Dolev-Yao model. In particular, we provide a fully automated proof of the soundness of MTProto 2.0's authentication, normal chat, end-to-end encrypted chat, and re-keying mechanisms with respect to several security properties, including authentication, integrity, confidentiality and perfect forward secrecy. To prove these results we proceed in a modular way: each protocol is examined in isolation, relying only on the guarantees provided by the previous ones and the robustness of the basic cryptographic primitives. Our research proves the formal correctness of MTProto 2.0 in the symbolic model, and it can serve as a reference for implementation and analysis of clients and servers.