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

Security analysis of TLS1.3 protocol based on HCPN model

作　　者：陈真好 田学成 Chen Zhenhao;Tian Xuecheng(Nanjing Tianchang Information Technology Co.,Ltd.,Nanjing 211100,China;Guodian Nanjing Automation Co.,Ltd.,Nanjing 211100,China)

机构地区：[1]南京天畅信息技术有限公司,江苏南京211100 [2]国电南京自动化股份有限公司,江苏南京211100

出　　处：《网络安全与数据治理》2022年第11期49-58,共10页CYBER SECURITY AND DATA GOVERNANCE

摘　　要：传输层(Transport Layer Security,TLS)协议是保证网络传输安全的重要标准协议,实现了数据加密和数据完整性以及身份验证。由于TLS协议一直存在很多安全漏洞,因此不断更新。目前最新版本TLS1.3(RFC 8846)已经发布,较之前TLS1.2(RFC 5246)在协议内容上有很大改进,提高了安全性和传输效率。使用层次着色Petri网(HCPN)的建模方法对TLS1.3握手协议进行建模,同时添加Delov-Yao攻击模型,并分析了对应模型下的状态空间报告。实验结果表明新发布的TLS1.3握手协议预主密钥有良好的机密性,并且身份认证满足协议规范的安全属性要求。目前国内在协议形式化分析方法的研究方面很少,本文研究在协议形式化分析方法上对其他协议分析具有理论指导意义。The Transport Layer Security(TLS)protocol is an important standard protocol for ensuring network transmission security,which realizes data encryption,data integrity,and identity verification.TLS protocol has been updated because there are many security vulnerabilities.Currently,the latest version is TLS1.3(RFC 8846)which has been released.Compared with the previous TLS1.2(RFC 5246),the content of the protocol has been greatly improved,improving security and transmission efficiency.In this paper,a hierarchical colored Petri net(HCPN)modelling method is used to model the TLS1.3 handshake protocol.At the same time,a Delov-Yao attack model is added,and we also analyze the state space report under the corresponding model.Finally,the experimental results show that the newly released pre-master key of the TLS1.3 handshake protocol has good confidentiality,and the identity authentication meets the security attribute requirements of the protocol specification.At present,there are few types of research on formal analysis methods of protocols in China.Therefore,This paper has theoretical guidance significance for other protocol analysis in terms of formal analysis methods of protocols.

关 键 词：TLS1.3 CPN Tools TLS1.3握手协议 形式化分析 

分 类 号：TN915.08[电子电信—通信与信息系统]