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.


翻译:MTProto 2. 0 是一套用于在广受欢迎的电讯信使应用程序核心进行即时通讯的加密协议。 在本文中, 我们使用符号验证器 ProVerif 分析 MTProto 2. 0。 我们提供完全自动化的证明, 证明MTProto 2. 0 的认证、 正常聊天、 端对端加密聊天, 以及若干安全特性的重置机制, 包括认证、 完整性、 保密和完美的前方保密 ; 同时, 我们发现重订协议很容易受到未知的钥匙共享( UKS) 攻击 。 我们以渐进的方式行事: 每项协议都被孤立地审查, 仅依赖先前协议提供的保障和基本加密原始特征的坚固性。 我们的研究证明MTProto 2. 0 (w.r.t.) 最相关的安全特性的正式正确性, 它可以作为客户和服务器实施和分析的参考。

0
下载
关闭预览

相关内容

Automator是苹果公司为他们的Mac OS X系统开发的一款软件。 只要通过点击拖拽鼠标等操作就可以将一系列动作组合成一个工作流,从而帮助你自动的(可重复的)完成一些复杂的工作。Automator还能横跨很多不同种类的程序,包括:查找器、Safari网络浏览器、iCal、地址簿或者其他的一些程序。它还能和一些第三方的程序一起工作,如微软的Office、Adobe公司的Photoshop或者Pixelmator等。
专知会员服务
25+阅读 · 2021年4月13日
Linux导论,Introduction to Linux,96页ppt
专知会员服务
78+阅读 · 2020年7月26日
【ICML2020-浙江大学】对抗性互信息的文本生成
专知会员服务
43+阅读 · 2020年7月4日
Stabilizing Transformers for Reinforcement Learning
专知会员服务
59+阅读 · 2019年10月17日
2019年机器学习框架回顾
专知会员服务
35+阅读 · 2019年10月11日
[综述]深度学习下的场景文本检测与识别
专知会员服务
77+阅读 · 2019年10月10日
【SIGGRAPH2019】TensorFlow 2.0深度学习计算机图形学应用
专知会员服务
39+阅读 · 2019年10月9日
最新BERT相关论文清单,BERT-related Papers
专知会员服务
52+阅读 · 2019年9月29日
.NET Core 原生DI+AOP实现注解式编程
DotNet
8+阅读 · 2019年9月9日
计算机 | 入门级EI会议ICVRIS 2019诚邀稿件
Call4Papers
10+阅读 · 2019年6月24日
计算机 | EMNLP 2019等国际会议信息6条
Call4Papers
18+阅读 · 2019年4月26日
CCF A类 | 顶级会议RTSS 2019诚邀稿件
Call4Papers
10+阅读 · 2019年4月17日
Call for Participation: Shared Tasks in NLPCC 2019
中国计算机学会
5+阅读 · 2019年3月22日
强化学习的Unsupervised Meta-Learning
CreateAMind
17+阅读 · 2019年1月7日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
17+阅读 · 2018年12月24日
计算机类 | 期刊专刊截稿信息9条
Call4Papers
4+阅读 · 2018年1月26日
分布式TensorFlow入门指南
机器学习研究会
4+阅读 · 2017年11月28日
【今日新增】IEEE Trans.专刊截稿信息8条
Call4Papers
7+阅读 · 2017年6月29日
Arxiv
0+阅读 · 2021年6月21日
Arxiv
0+阅读 · 2021年6月20日
Arxiv
0+阅读 · 2021年6月17日
The Matrix Calculus You Need For Deep Learning
Arxiv
12+阅读 · 2018年7月2日
VIP会员
相关VIP内容
专知会员服务
25+阅读 · 2021年4月13日
Linux导论,Introduction to Linux,96页ppt
专知会员服务
78+阅读 · 2020年7月26日
【ICML2020-浙江大学】对抗性互信息的文本生成
专知会员服务
43+阅读 · 2020年7月4日
Stabilizing Transformers for Reinforcement Learning
专知会员服务
59+阅读 · 2019年10月17日
2019年机器学习框架回顾
专知会员服务
35+阅读 · 2019年10月11日
[综述]深度学习下的场景文本检测与识别
专知会员服务
77+阅读 · 2019年10月10日
【SIGGRAPH2019】TensorFlow 2.0深度学习计算机图形学应用
专知会员服务
39+阅读 · 2019年10月9日
最新BERT相关论文清单,BERT-related Papers
专知会员服务
52+阅读 · 2019年9月29日
相关资讯
.NET Core 原生DI+AOP实现注解式编程
DotNet
8+阅读 · 2019年9月9日
计算机 | 入门级EI会议ICVRIS 2019诚邀稿件
Call4Papers
10+阅读 · 2019年6月24日
计算机 | EMNLP 2019等国际会议信息6条
Call4Papers
18+阅读 · 2019年4月26日
CCF A类 | 顶级会议RTSS 2019诚邀稿件
Call4Papers
10+阅读 · 2019年4月17日
Call for Participation: Shared Tasks in NLPCC 2019
中国计算机学会
5+阅读 · 2019年3月22日
强化学习的Unsupervised Meta-Learning
CreateAMind
17+阅读 · 2019年1月7日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
17+阅读 · 2018年12月24日
计算机类 | 期刊专刊截稿信息9条
Call4Papers
4+阅读 · 2018年1月26日
分布式TensorFlow入门指南
机器学习研究会
4+阅读 · 2017年11月28日
【今日新增】IEEE Trans.专刊截稿信息8条
Call4Papers
7+阅读 · 2017年6月29日
Top
微信扫码咨询专知VIP会员