Telegram MTProto 2.0的自动符号验证

下载PDF摘要：MTProto 2.0是一套用于即时消息传递的加密协议，它是流行的Telegram Messenger应用程序的核心，该应用程序目前有4亿多人在使用。在本文中，我们使用基于Dolev-Yao模型的符号密码协议验证程序ProVerif分析了MTProto 2.0。特别是，我们提供了有关MTProto 2.0身份验证，常规聊天，端到端加密聊天以及针对多个安全属性（包括身份验证，完整性，机密性和完善性）的重新加密机制的健全性的全自动证明。前向保密。为了证明这些结果，我们以模块化的方式进行：仅依赖于先前协议提供的保证以及基本密码原语的鲁棒性，对每个协议进行了隔离检查。我们的研究证明了符号模型中MTProto 2.0的形式正确性，可以为客户端和服务器的实现和分析提供参考。