Formal Methods; Practical Verification; Privacy; Security Protocols; Specification; Verification and Synthesis

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. In this paper we analyse MTProto 2.0 using the symbolic verifier ProVerif. We provide fully automated proofs of the …