基于HCPN模型的TLS1.3协议安全性分析

作者：陈真好; 田学成^*

来源：网络安全与数据治理, 2022, 41(11): 49-58.

DOI：10.19358/j.issn.2097-1788.2022.05.008

• TLS1.3
• CPN Tools
• TLS1.3握手协议
• 形式化分析

传输层(Transport Layer Security,TLS)协议是保证网络传输安全的重要标准协议，实现了数据加密和数据完整性以及身份验证。由于TLS协议一直存在很多安全漏洞，因此不断更新。目前最新版本TLS1.3(RFC 8846)已经发布，较之前TLS1.2 (RFC 5246)在协议内容上有很大改进，提高了安全性和传输效率。使用层次着色Petri网(HCPN)的建模方法对TLS1.3握手协议进行建模，同时添加Delov-Yao攻击模型，并分析了对应模型下的状态空间报告。实验结果表明新发布的TLS1.3握手协议预主密钥有良好的机密性，并且身份认证满足协议规范的安全属性要求。目前国内在协议形式化分析方法的研究方面很少，本文研究在协议形式化分析方法上对其他协议分析具有理论指导意义。

• 单位
  国电南京自动化股份有限公司