Specification; Verification and synthesis; Security protocols; Practical verification; Privacy; Formal methods

MTProto 2.0 is the suite of security protocols for instant messaging at the core of the popular Telegram messenger application. In this paper we analyse MTProto 2.0 using ProVerif, a state-of-the-art symbolic security protocol verifier based on the …