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

作     者：陆思奇 周思渊 毛颖 LU Si-Qi;ZHOU Si-Yuan;MAO Ying

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

出 版 物：《软件学报》 (Journal of Software)

年 卷 期：2021年第32卷第9期

页      面：2849-2866页

核心收录：

学科分类：08[工学] 0835[工学-软件工程] 0811[工学-控制科学与工程] 0812[工学-计算机科学与技术（可授工学、理学学位）] 081202[工学-计算机软件与理论] 

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

主　　题：TLS1.3 形式化分析 Syther CK安全模型 KCI攻击 

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