HackerPapers

arXiv:2012.03141cs.CR

Automated Symbolic Verification of Telegram's MTProto 2.0

Marino Miculan, Nicola Vitacolonna

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.

arXiv comments
19 pages
Journal reference
In "Proceedings of the 18th International Conference on Security and Cryptography, SECRYPT 2021". ISBN 978-989-758-524-1, pages 185-197
DOI
doi:10.5220/0010549601850197
Subjects
cs.CRCryptography and Security

On Hacker News

Linked by 5 identifiable commenters in 7 comments across 6 threads, from Jan 2021 to Aug 2024. Found in 4 HN submissions from Dec 2020 to Jan 2023. Open submission discussions.

Comments linking this paper, per year.

Discussed in comments6 threads

  1. Arrest of Pavel Durov, Telegram CEO, charges of terrorism, fraud, child porn 2 comments

    • > They are stored in plaintext on telegram servers FYI, this is a totally misleading and false claim. Telegram uses the MTProto 2.0 Cloud algorithm for non-secret chats[1][2]. In fact, it uses a split-key encryption system and the servers are all stored in multiple…

      NayamAmarsheView on HNParent context

    • That's a popular lie, Telegram uses the MTProto 2.0 Cloud algorithm for non-secret chats, which is audited and verified by multiple independent parties. For example WhatsApp claims it uses EE2E encrypted chats, how ever these claims are unverified and not audited. Also their…

      gloosxView on HNParent context

  2. Deploying key transparency at WhatsApp 1 comment

    • > The algorithm is public. It is a straightforward application of well known primitives. It is hardly proprietary. Note that its predecessor, was very much not that (e.g. https://words.filippo.io/dispatches/telegram-ecdh/ was a vulnerability in it, and it stuck to some weird…

      robrykView on HNParent context

  3. Signal is secure, as proven by hackers 1 comment

    • > Telegram holds the keys to decrypt the messages and that's all you need to know. That's an entirely different problem than TFA (an attacker accessing and being able to impersonate an account by subverting a third party 2FA middleman), which Telegram guards against as as soon…

      lloekiView on HNParent context

  4. Poll: Switching from WhatsApp 1 comment

    • Each of these have fairly different use cases. WhatsApp is bad. They are owned by a data collection company notorious for gross privacy violations. Both the client apps and the server are completely closed source, which means either could be spying on you without any way to…

      j-jamesView on HNParent context

  5. WhatsApp gives users an ultimatum: Share data with Facebook or stop using app 1 comment

    • Telegram's MTProto 2.0 encryption protocol was recently proved correct, but I haven't seen any peer review or discussion on the paper yet. https://arxiv.org/abs/2012.03141

      j-jamesView on HNParent context

  6. Telegram publishes users' locations online 1 comment

    • Telegram's protocol itself isn't necessarily a weakness - recently, a paper was published claiming to have proved the MTProto 2.0 protocol correct. Perhaps because of how recent this was, it doesn't seem to have garnered any discussion or review anywhere.…

      j-jamesView on HNParent context

Submitted to Hacker News

Connected through shared HN threads, not inferred similarity or a recommendation.