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

Formal Analysis and Optimization of TLS1.3 Protocol in Strong Security Model

作　　者：陆思奇 周思渊 毛颖 LU Si-Qi;ZHOU Si-Yuan;MAO Ying(PLA Information Engineering University,Zhengzhou 450001,China;State Key Laboratory of Information Security(Institute of Information Engineering,Chinese Academy of Sciences),Beijing 100093,China;School of Cyber Security,University of Chinese Academy of Sciences,Beijing 100093,China)

机构地区：[1]解放军信息工程大学,河南郑州450001 [2]信息安全国家重点实验室(中国科学院信息工程研究所),北京100093 [3]中国科学院大学网络空间安全学院,北京100093

出　　处：《软件学报》2021年第9期2849-2866,共18页Journal of Software

基　　金：国家自然科学基金(61472414,61772514,61602061)。

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

关 键 词：TLS1.3 形式化分析 Syther CK安全模型 KCI攻击 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]