软件学报

作者：陆思奇，周思渊，毛颖

单位：陆思奇，解放军信息工程大学, 河南 郑州 450001;信息安全国家重点实验室(中国科学院 信息工程研究所), 北京 10009311,周思渊，解放军信息工程大学, 河南 郑州 45000102,毛颖，信息安全国家重点实验室(中国科学院 信息工程研究所), 北京 100093;中国科学院大学 网络空间安全学院, 北京 10009303

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

基金：国家自然科学基金（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攻击和重放攻击.

来源：2021年第9期

《软件学报》期刊编辑部

查看软件学报杂志2021年第9期