Telegram MTProto 2.0 的自动化符号验证
密码学与安全
2021-07-27 v2
摘要
MTProto 2.0 是一套加密协议，用于流行即时通讯应用 Telegram 核心的即时消息传递。本文中，我们使用符号验证器 ProVerif 分析 MTProto 2.0。我们针对若干安全性质（包括认证性、完整性、保密性和完美前向安全性）提供了 MTProto 2.0 认证、普通聊天、端到端加密聊天以及重密钥机制的完全自动化soundness证明；同时，我们发现重密钥协议易遭未知密钥共享 (UKS) 攻击。我们以增量方式进行：每个协议被孤立检验，仅依赖前述协议所提供的保证以及基本密码原语的健壮性。我们的研究证明了 MTProto 2.0 相对于最相关安全性质的正式正确性，并可作为客户端与服务器实现及分析的参考。
引用
@article{arxiv.2012.03141,
title = {Automated Symbolic Verification of Telegram's MTProto 2.0},
author = {Marino Miculan and Nicola Vitacolonna},
journal= {arXiv preprint arXiv:2012.03141},
year = {2021}
}
备注
19 pages