0 引言
TLS协议作为一种协议安全机制最初是由Netscape Communications公司与1995年开发的安全套接层（Secure Sockets Layer，SSL）演变而来的[1]，之后由国际互联网工程任务组(Internet Engineering Task Force，IETF)指定规范并逐渐升级到TLS1.2。在不断的使用过程中发现TLS协议存在很多安全风险[2]。新发布的TLS1.3版本协议内容上较之前有较大的改变，增强了算法的安全性，同时减少了会话次数，提高了效率[3]。在TLS1.3协议安全研究方面，Cas Cremers等人使用Tamarin工具对协议做符号形式化的分析[4]，但该工具攻击模型需要手动输入，设置比较复杂很难掌握，并且不能反映协议执行细节问题。王小峰等人使用基于Applied PI演算对TLS1.3做形式化建模[5]，使用分析工具ProVerify验证了握手协议的认证性和预主密钥的机密性，但该工具在协议漏洞发现上存在欠缺，只能用来验证协议的安全属性是否符合规范。
本文使用CPN Tools形式化建模工具分析TLS1.3握手协议。CPN Tools建模工具可以直观地描述协议执行的细节问题，并且根据需要添加网络时间延迟，更加细致地模拟协议执行过程。它提供状态空间分析方法和模型检测来验证协议安全性能。因为TLS握手协议密钥建立方式的复杂性和身份认证的多样性，本文基于密钥建立方式为有限域上的椭圆曲线方法[3]。基于层次着色Petri网(HCPN)[6]的建模方法使用CPN Tools工具对TLS1.3握手协议进行建模，分析其状态空间，并添加Delov-Yao[7]敌手攻击模型，验证协议的安全属性，根据状态空间输出的数据判断TLS1.3握手协议预主密钥和身份认证的安全性是否满足协议规范的安全属性要求。
本文详细内容请下载：https://www.chinaaet.com/resource/share/2000005026
作者信息：
陈真好1，田学成2
(1.南京天畅信息技术有限公司，江苏 南京211100；2.国电南京自动化股份有限公司，江苏 南京211100)
