Page 225 - 《软件学报》2021年第9期

软件学报 ISSN 1000-9825, CODEN RUXUEW E-mail: jos@iscas.ac.cn
Journal of Software,2021,32(9):2849−2866 [doi: 10.13328/j.cnki.jos.005973] http://www.jos.org.cn
©中国科学院软件研究所版权所有. Tel: +86-10-62562563

∗
强安全模型下 TLS1.3 协议的形式化分析与优化

1
1,2
陆思奇 , 周思渊 , 毛 颖 2,3
1
(解放军信息工程大学,河南 郑州 450001)
2 (信息安全国家重点实验室(中国科学院 信息工程研究所),北京 100093)
3 (中国科学院大学 网络空间安全学院,北京 100093)
通讯作者: 毛颖, E-mail: maoying@iie.ac.cn

摘 要: TLS 协议在 TCP/IP 体系中的传输层和应用层之间工作,通过提供机密性、完整性、必选的服务器认证以
及可选的客户端认证等一系列安全服务,有效保护了传输层的安全.TLS1.3 协议为了降低网络延迟,增加了对 0-RTT
数据的支持,通过客户端缓存服务器的长期公钥,在第 1 条消息中,直接利用该长期公钥生成一个会话密钥发送部分
应用层数据.针对 3 种 0-RTT 模式,使用 Scyther 工具对其进行了形式化分析,得出了在 CK 安全模型下,0-RTT 数据
的两种攻击,并基于其中的 1-RTT semi-static 模式提出了一种优化协议.通过安全性证明和形式化分析,证明了该优
化协议在 CK 安全模型下能够抵抗针对 0-RTT 数据的 KCI 攻击和重放攻击.
关键词: TLS1.3;形式化分析;Syther;CK 安全模型;KCI 攻击
中图法分类号: TP311

中文引用格式: 陆思奇,周思渊,毛颖.强安全模型下 TLS1.3 协议的形式化分析与优化.软件学报,2021,32(9):2849−2866.
http://www.jos.org.cn/1000-9825/5973.htm
英文引用格式: Lu SQ, Zhou SY, Mao Y. Formal analysis and optimization of TLS1.3 protocol in strong security model. Ruan
Jian Xue Bao/Journal of Software, 2021,32(9):2849−2866 (in Chinese). http://www.jos.org.cn/1000-9825/5973.htm

Formal Analysis and Optimization of TLS1.3 Protocol in Strong Security Model
1
1,2
LU Si-Qi , ZHOU Si-Yuan , MAO Ying 2,3
1 (PLA Information Engineering University, Zhengzhou 450001, China)
2 (State Key Laboratory of Information Security (Institute of Information Engineering, Chinese Academy of Sciences), Beijing 100093,
China)
3 (School of Cyber Security, University of Chinese Academy of Sciences, Beijing 100093, China)

Abstract: TLS protocol works between the transport layer and application layer in TCP/IP system. The safety of transport layer is
effectively protected by providing a series of security services such as confidentiality, integrity, authentication server required, as well as
optional client authentication. In order to reduce network latency, TLS1.3 protocol adds the support for 0-RTT data, through caching
long-term public key of server by client, and the long-term public key is directly used to generate a session key to send part of
application layer data in the first message. For three kinds of 0-RTT mode, this study uses Scyther tools for formal analysis to obtain two
attack paths of the 0-RTT data in CK security model, and an optimized protocol is proposed based on the 1-RTT semi-static mode.
Through security proof and formal analysis, it is proved that the protocol is resistant to KCI attacks and replay attack against 0-RTT data
in CK security model.
Key words: TLS1.3; formal analysis; Scyther; CK security model; KCI attacks

网络安全协议能够解决信息的传输安全问题,以互联网工程任务组(Internet engineering task force,简称

∗ 基金项目: 国家自然科学基金(61472414, 61772514, 61602061)
Foundation item: National Natural Science Foundation of China (61472414, 61772514, 61602061)
收稿时间: 2018-03-15; 修改时间: 2018-08-30; 采用时间: 2019-03-18