论文标题
Telegram的MTPROTO 2.0的自动符号验证
Automated Symbolic Verification of Telegram's MTProto 2.0
论文作者
论文摘要
MTPROTO 2.0是一套密码协议套件，用于在流行的Telegram Messenger应用程序的核心中进行即时消息传递。在本文中，我们使用符号验证者箴言分析了mtproto 2.0。我们提供了MTPROTO 2.0的身份验证，正常聊天，端到端加密聊天以及对几个安全属性的重新钥匙机制的完整自动化证明，包括身份验证，完整性，保密和完美的远期保密；同时，我们发现重钥匙协议很容易受到未知的钥匙份（UKS）攻击。我们以增量的方式进行：每个协议都是隔离检查的，仅依靠先前提供的保证以及基本加密原始原始的鲁棒性。我们的研究证明了MTPROTO 2.0 W.R.T.的正式正确性。大多数相关的安全性属性，它可以作为对客户和服务器的实现和分析的参考。
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.
