| 摘要: |
| 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攻击 |
| DOI：10.13328/j.cnki.jos.005973 |
| 分类号:TP311 |
| 基金项目:国家自然科学基金（61472414，61772514，61602061） |
|
| Formal Analysis and Optimization of TLS1.3 Protocol in Strong Security Model |
|
LU Si-Qi1,2, ZHOU Si-Yuan1, MAO Ying2,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 |
