Automated Symbolic Verification of Telegram's MTProto 2.0
This research provides formal correctness proofs and identifies a critical vulnerability for developers and users of Telegram's MTProto 2.0.
This paper analyzes Telegram's MTProto 2.0 cryptographic protocols using the symbolic verifier ProVerif, providing automated proofs for authentication, normal chat, end-to-end encrypted chat, and rekeying mechanisms. While proving soundness for most security properties, the study discovered an unknown key-share (UKS) attack vulnerability in the rekeying protocol.
MTProto 2.0 is a suite of cryptographic protocols for instant messaging at the core of the popular Telegram messenger application. In this paper we analyse MTProto 2.0 using the symbolic verifier ProVerif. We provide fully automated proofs of the soundness of MTProto 2.0's authentication, normal chat, end-to-end encrypted chat, and rekeying mechanisms with respect to several security properties, including authentication, integrity, secrecy and perfect forward secrecy; at the same time, we discover that the rekeying protocol is vulnerable to an unknown key-share (UKS) attack. We proceed in an incremental 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 w.r.t. most relevant security properties, and it can serve as a reference for implementation and analysis of clients and servers.