Automated Symbolic Verification of Telegram's MTProto 2.0

TL;DR

This paper uses automated symbolic verification to analyze Telegram's MTProto 2.0, confirming its security properties while identifying a vulnerability in the rekeying protocol.

Contribution

It provides the first fully automated formal verification of MTProto 2.0's security properties using ProVerif, and uncovers a previously unknown key-share attack vulnerability.

Findings

ProVerif successfully verified authentication, integrity, secrecy, and forward secrecy.

Identified a vulnerability in the rekeying protocol to an unknown key-share attack.

Validated the protocol's formal correctness for most security properties.

Abstract

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.