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

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

来源：软件学报, 2021, 32(09): 2849-2866.

DOI：10.13328/j.cnki.jos.005973

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

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

• 单位
  中国科学院信息工程研究所; 中国科学院大学; 中国人民解放军信息工程大学; 信息安全国家重点实验室