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

陈真好，田学成

(1.南京天畅信息技术有限公司，江苏 南京 211100；2.国电南京自动化股份有限公司，江苏 南京 211100)

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握手协议预主密钥和身份认证的安全性是否满足协议规范的安全属性要求。

1 TLS1.3握手协议

1.1 密钥建立方式

TLS1.3实现身份认证和密钥交换都是通过TLS的扩展部分实现，故TLS1.3密码套件(CipherSuite)仅用来加密和实现散列哈希算法，减少至5个密码套件[3]，见表1。

表1 TLS1.3密码套件

TLS1.3握手协议在协议算法上较之前有很大改变，因为静态的RSA算法不提供向前安全(Perfect Forward Secrecy，PFS)[2]，容易被攻击者窃听通信消息获取服务器私钥，所以在TLS1.3中被弃用，TLS1.3不再支持密钥的压缩算法，同时删除了很多已存在安全隐患的算法。目前TLS1.3只支持三种基本的密钥交换模式：

(1)(EC)DHE：Diffie-Hellman在有限域上或椭圆曲线上密钥交换模式。

(2)Pre-shared-key(PSK)：预主密钥模式。

(3)将上面两者结合的模式。

本文基于有限域上椭圆曲线密钥交换方式建模。由于TLS握手协议的复杂性和认证方式的多样性，在使用CPN Tools建模分析TLS1.3握手协议过程中重点分析了密钥协商和身份认证的安全属性。

1.2 TLS握手协议会话过程

TLS协议的主要目的是保护上层协议安全透明地传输，其协议组成主要有握手协议和记录协议，TLS握手协议实现密钥协商和身份验证以及数据完整性验证。TLS1.3握手协议较之前TLS1.2会话过程发生很大改变。TLS1.2在发送应用程序数据之前需要往返两次(2-RTT)才能完成握手，而TLS1.3只需要往返一次(1-RTT)即可完成[2]，在时间效率上大大提高。

TLS1.3不再支持静态的RSA密码交换算法，而是使用带有向前安全的Diffie-Hellman进行全面握手。使用特殊的扩展来发送密钥协商使用的参数。ServerHello消息发送之后增加了加密EncryptedExtension消息[3]，响应与密钥协商参数无关的其他扩展。使用临时密钥加密减少了可见明文的数量，提高了安全性，同时禁止双方发起重新协商。删除了Change_ChipherSpec协议和ServerKeyExchange、Client-KeyExchange消息。会话的恢复方式被预主密钥(pre_shared_key)模式替代，TLS1.3握手协议会话恢复方式较TLS1.2有较大改变，弃用了TLS1.2使用SessionID连接方式，同时减少了会话次数，提高了效率。

TLS1.3握手协议会话过程如图1所示。

图1 TLS1.3握手协议会话过程

2 着色Petri网的概念和属性

2.1 着色Petri的定义

Colored Petri Nets(CPN)[8]是基于Petri网基础上提出的一种高级Petri网，CPN不但保留了Petri的优点，提供了可操作界面，而且增加了语言表达能力、颜色集等。CPN是一种可以对系统进行检验和仿真的建模语言，用于描述和分析具有通信、同步、并发、分布等特征的复杂系统。HCPN模型是在着色Petri网的基础上增加了层次模型和子模块的概念，使Petri网成为经典Petri网，它是一个有向的连通图，由库所和变迁两种节点以及他们之间的弧构成，定义如下。

定义1Colored Petri Net是一个九元组CPN=(P，T，A，Σ，C，V，G，E，I)[9]，其中：

P：一个有限的库所(Place)的集合，代表一种数据资源，用椭圆表示。

T：有限变迁的集合，且T满足P∩T=φ，描述系统活动，用矩形表示。

A：是一个有向弧的集合，满足A⊆PxT∪TxP，代表数据资源的流动方向，用箭头表示。从库所到变迁的弧描述变迁被触发的条件。从变迁到库所的弧描述变迁点火之后发生的状态。通过定义弧上的函数，可以决定托肯值流向不同的库所。

Σ：有限非空颜色集类型的集合。

V：有限变量的集合，对所有变量v∈V满足Type[v]∈Σ。

C：P→Σ是颜色集函数，它给每一个位置分配一个颜色集合。

G：T→EXPRV是弧表达式函数，它为每一个弧分配一个表达式。

I：P→EXPRφ是初始化函数，库所通常需要被赋予一个初始化表达式。

定义2层次化CPN模型HCPN是四元组HCPN=(S，SM，PS，FS)[10]，其中：

S：模型有限集合的模块集合。所有的s1，s2∈S并且s1≠s2，每个模型都是CPN的子模块S=((Ps，Ts，As，Σs，Vs，Cs，Gs，Es，Is)，Tssub，Psport，PTs)要求(Ps1∪Ts1)∩(Ps2∪Ts2)=ϕ。

SM：Tsub→S是子模块函数，用关联替代变迁和对应的CP-nets子模块。

PS：用于定义端口关联关系，∀t∈Tsub，PS(t)⊆其中Psock(t)为替代变迁所在模块的端口库所为与替代变迁关联的CP-nets模块所对应的库所，并且对所有的(p，p")∈PS(t)和所有的t∈Tsub，等式PT(p)=PT(p")，C(p)=C(p")，I(p)＜＞=Ia(p")＜＞都成立。

FS：FS⊆2P是库所融合集，对所用的p，p"∈fs，所有fs∈FS，等 式C(p)=C(p")，I(p)＜＞=Ia(p")＜＞成立。一个库所融合集中的所有库所实质上为同一个库所。

2.2 CPN Tools属性特征

CPN Tools是由奥尔胡斯大学团队研发的一款系统建模分析工具[11]，在CPN Tools工具中，模型描述语言由Petri网图和编程语言CPN ML构成，提供良好的用户界面(GUI)，具有增量语法检查和代码生成功能。不必关心协议具体实现的细节问题[12]。可以进行单步执行或连续执行，用户可以利用CPN Tools对模型的各个部分进行测试，保证模型的正确性。可以处理未定时和定时的网络，创建层次的CPN的可达图，计算状态空间并生成状态空间报告，状态空间报告可用于分析模型的静态和动态特性，标准状态空间报告包含注入边界和活性属性等信息，具有回馈机制可以将错误进行定位，这给分析协议系统模型提供很大帮助。表2是CPN Tools支持定义的数据类型的颜色集。

表2 CPN Tools定义的颜色集类型

基于CPN模型检测方法对协议安全性能的分析主要包括以下基础属性：活性、可达性、有界性、完整性、认证性、机密性、可恢复性等。其中协议活性用来描述协议逾期事件的发生，可达性用来描述预定的协议状态会发生。协议能够按照期望的行为方式运行，安全属性在攻击者模型中特指协议不存在与预期状态相悖的行为。非预期状态通常会导致模型出现死锁，有界性通常用来判断特定状态下消息库所的容量上下限。可恢复性可以表明协议模型在出现错误后能否在有限时间内返回到预期状态并进入正常序列。

3 基于HCPN模型的TLS1.3握手协议建模

3.1 TLS1.3预主密钥和身份认证

TLS1.3协议规范中制定了协议的降级保护[13]，通过增加确定的扩展结构，保持与之前版本的兼容性，避免未升级的通信服务端和中间件因为不能解释而拒绝响应服务，这使得新的功能被移值到扩展结构中。如果含有扩展字段support_version则表示采用TLS1.3连接方式[3]。LTS1.3握手协议密钥的建立是通过多个输入密钥结合创建实际工作的密钥材料实现的[14]。所以可以将复杂的密钥算法抽象成特定的函数替换。为了简化整个握手的过程，将不参加密钥建立和认证的参数不计入形式化分析过程，根据图1分析的握手协议顺序图可以得到TLS1.3握手协议形式化描述过程如下：

(1)Client→Server：(ProtocolVersion_c，Clietn_Random，CipherSuitec，Compressionmethods，Extension)

(2)Server→Client：(ProtocolVersion_s，Server_Random，CipherSuite_s)

(3)Server→Client：(Signature_Algorithm，Pre_Shared_Key)

(4)Server→Client：(ServerCerficate)

(5)Client→Server：(Cerficate，CerficateVerify，Finished)

(6)Server→Client：(Cerficate，CerficateVerify，Finished)

身份认证过程和预主密钥计算过程指定私钥PR使用函数Sign对消息签名，公钥PU使用函数Versign验证签名，公钥PU使用函数Anec对消息加密，私钥PR使用函数Adec对消息解密。客户端发送的ClientHello消息和服务端发送的ServerHello消息都是明文传输。之后从服务端发送的消息都开始加密传输。服务端在发送Pre_Shared_Key时使用非对称算法加密：

EncryptedEx=Anec(Pre_Shared_Key，PU(k_rsa))

客户端接收到该消息之后对其解密获取预主密钥：

Pre_(Shared_Key)=Adec(Encryptedx，PR(k_rsa))

之后进行客户端对服务端的身份认证，服务端发送加密的身份信息：

SignedCerficateS=Sign(ServerCerficate，PR(Signkey))

客户端接收到之后对其进行解密：

ServerCerficate=Versign(SignedCerficate，PU(Signkey))

根据解密得到的证书信息查询证书链，认证服务端的身份信息。同时客户端发送加密的身份信息：

SignedCerficateC=Sign(ClientCerficate，PR(Signkey))

服务端接收到之后对其进行解密：

ServerCerficate=Versign(SignedCerficateC，PU(Signkey))

根据解密得到的证书信息查询证书链，验证客户端身份信息。建模主要目的是验证协议设计是否违背安全属性，所以在模型中不再考虑网络数据丢失情况。

3.2 模型使用的颜色和变量定义

CPN Tools中有多重数据类型的定义，如Integer、String、Unit、Product(不同类型的叉积)、union(不同类型的中的一种)，records、list等[11]，根据协议规范文档TLS1.3(RFC 8446)的定义，对其模型抽象简化，TLS握手协议中客户端和服务端之间密钥传输过程中使用的参数字段对应表见表3。

表3 协议参数字段含义

根据CPN ML语言，定义模型中要使用的数据类型的颜色集，因为TLS1.3协议复杂性，定义的颜色集较多，这里只列举部分重要的相关颜色集定义。对明文传输的ClientHello和ServerHello消息使用乘积(product)类型颜色集定义，而对于后续加密的消息则使用记录(record)类型颜色集定义。为了避免CPN模型状态空间爆炸问题，限定了随机数ClientRandom和ServerRandom的范围为4～6，同时定义了客户端支持的协议版本ProtocolVersion_c的托肯值为2和3，表示支持的协议版本TLS1.3或者TLS1.2。而服务端只提供ProtocolVersion_s的托肯值为3的一种情况，表示服务端默认选择TLS1.3。定义的颜色集和变量如表4所示。

表4 模型数据类型颜色值定义

根据协议中存在的函数加密解密过程，定义客户端和服务端分别持有的公钥和私钥。使用ML形式化描述语言抽象成下面的的函数。

(fun DecryptionKey(k：PublicKey)

=@PU=＞PR@|Aenc=＞Adec@|Signed=＞Versign；)

3.3 TLS1.3协 议 的HCPN建 模

按照TLS1.3握手协议密钥协商形式化描述过程，协议发起者Client和响应者Server按照协议规范RFC 8846执行，CPN模型主要描述TLS1.3握手协议版本的选择和预主密钥Pre_Shared_key传输以及双双身份认证过程。实验的主要目的是验证预主密钥和身份认证的安全性。

使用CPN Tools对TLS1.3握手协议建模，同时添加Dolev-Yao攻击者模型，验证协议设计是否存在安全隐患。基于HCPN的TLS1.3握手协议模型分为顶层模型TLS，实体层模型Client、Server和Network。顶层模型TLS描述TLS1.3协议的总体概况，顶层模型包括协议实体Client和Server以及Network三个节点。之后采用HCPN层次化建模方法为每个实体节点创建一个替代变迁，对顶层模型中的每个替代变迁细化描述。TLS1.3原始模型建好之后，得到状态空间报告，之后在此模型基础上添加Dolev-Yao攻击者模型，该攻击者模型能够获取协议实体(Client↔Server)节点之间的所有通信数据。

图2所示为TLS1.3握手协议的顶层模型，图3是节点Server的实体层模型。图2中的每个替代变迁对应实体层的一个子页，替代变迁Client对客户端实体层模型，替代变迁Server对应图4服务端实体层模型，替代变迁Network对应于网络层实体模型。

图2 TLS1.3握手协议的顶层模型

图3 节点Sever端实体层模型

Client实体层模型中客户端首先发送密钥交换材料，定义变迁clientrandom表示随机数，限定了随机 数 的 范 围 为4～6。定 义 变 迁protocolversionC表 示客户端支持的协议版本，用整数2和3表示TLS协议版本TLS1.2和TLS1.3。客户端发送ClientHello消息之后，服务端接收该消息，并选择自己支持的协议版本TLS1.3和相关的密钥材料。之后响应客户端ServerHello消息。

Server实体层模型反映服务端的实现细节，从客户端接收密钥材料，并根据自己支持的协议版本和密钥套件来选择建立主秘钥使用的协议版本和相关算法。使用布尔(bool)类型判断双方之间协商的协议版本是否为TLS1.3，如果为真，则继续后续的会话过程。为之后完成预主密钥传输和双方身份认证建立基础。

所有的会话过程都要经过网络层传输才能被接收，这里只分析协议本身设计上的安全性，不考虑网络重传或者数据丢失等问题。而攻击者也是在网络层中截获和存储信息。

图4是服务端实体层模型，表达客户端和服务端协商协议版本TLS1.3成功，当客户端提供的协议版本和服务端支持的协议版本相同时通过变迁逻辑判断输出“true”，继续执行模型后续协议会话过程。

图4 服务端选择TLS协议版本

图5是服务端预主密Pre_Shared_Key加密传输完成之后，客户端解密获得预主密钥，服务端加密发送服务端证书，客户端解密获得证书后查询证书链验证服务端的身份信息。

图5 客户端对服务端的身份认证

客户端对服务端身份认证完成之后，客户端加密发送自己的证书信息，服务端接收到信息之后解密获得客户端证书，通过查询证书链据此验证客户端身份信息。

图6是协议执行的最终状态，客户端完成对服务端身份信息的认证，同时服务端也完成对客户端身份信息的认证。模拟执行结束。在这基础上添加攻击者模型，验证密钥和身份认证的安全属性。

图6 顶层模型最终状态

3.4 TLS1.3添加DY敌手模型

Dolev-Yao[6]攻击模型被认为不具有攻破密码算法的能力，在没有私钥的情况下没有办法获知加密消息的内容。在此前提下Dolev-Yao模型规定攻击者具有可以不被协议主体察觉的情况下掌握整个通信网络的情况，并拦截和存储网络中的通信消息，同时攻击者可以伪造消息，之后以合法协议参与者的身份发送消息。整个协议的执行过程都暴露在攻击者的监视之下。基于此攻击者采用union类型表示攻击者拥有的数据类型，包括双方之间明文传输的随机数、协议版本号、密钥套件以及加密传输的所有原子信息。敌手攻击模型中敌手根据从网络中俘获的参数来重组消息，构造更强的攻击能力，以协议参与者的身份发送消息，达到窃取网络终端信息的目的。图7和图8是攻击者模型。攻击者通过构造信息之后发送给接收者。

图7 预主密钥传输攻击者模型

图8 身份认证攻击模型

因为服务端在传输预主密钥的时候使用了持有的私钥PR加密，之后将加密的密文和签名算法作为明文信息再次使用公钥Aenc加密。攻击者只能解密获得被加密的Pre_Shared_Key，之后使用自己的公钥对其再次加密之后伪装成服务端发送给客户端，并不能获得预主秘钥的信息。这样客户端将无法解密加密的预主密钥，中断传输。

客户端和服务端之间的身份认证方式是相同的，证书发送之前使用对应的的私钥加密，之后对加密信息再使用公钥加密，对应的接收端解密获得证书信息之后查询证书链，验证证书信息是否合法，据此判断双方的身份信息。Dolev-Yao攻击模型攻击者截获加密的证书信息之后，因为不具备双方私钥能力无法解密证书信息，加密后再次发送给接收者，接收者在接收到信息之后无法解密出证书信息。会话建立不成功。

4 协议安全性分析

基于HCPN模型的TLS1.3握手协议建模完成之后，分析了TLS1.3握手协议模型中预主密钥Pre_Shared_Key和双方身份认证的安全性，之后在该模型中加入攻击者模型，通过形式化验证协议模型是否违背TLS握手协议规范的安全属性。本文不考虑攻击者作为会话发起者的情况，只考虑攻击者作为协议会话的截获者重放消息或者伪装成其他实体发送消息，并且协议模型只考虑协议运行的单次会话的执行情况。

下面是CPN Tools生成的TLS1.3握手协议原模型的状态空间报告和基于Dolev-Yao攻击模型生成的状态空间报告。基于篇幅原因，这里只分析对应报告中重要的三种数据：统计数字分析、有界性分析和活性分析。

(1)TLS1.3握手协议原模型状态空间报告

表6列举了CPN Tools仿真得到的状态统计信息，其中State Spcae表示状态空间的节点和连接弧的个数，在该CPN模型中，节点数为2 194，连接弧为5 073，构造该状态空间过程在计算机上花费9 s，Scc Graph为强连接图，这与状态空间的节点数和连接弧个数相等，说明协议模型中的数据不需要重传。为了方便研究协议安全性，在设计之初不考虑网络重传问题。

表6 统计数字分析

表7是每个库所对应的托肯的数量区间，库所Client"clientrandom最多有3个托肯，最少托肯值为2，库所Client protocolversionC的托肯的上界是2，下界是0；Server"psk1的托肯上界是1，下届也是1。从这些库所的结果中可以看出该模型中的库所符合实际要求。

表7 有界性分析

表8是模型的活性分析表。其中Dead Markings指的是死标识状态，在该标识下任何变迁都是非使能的。Dead Transition指的是死变迁，即该变迁在模型中的任何发生序列中都无法发生，一般情况下死变迁的出现预示着模型的设计不合理，可以去掉死变迁而不影响模型的动态执行。本实验输出的结果显示不存在死变迁。Live Transition是活变迁，即在任何可达标识下，该变迁都在一个可发生序列中，输出结果显示本实验模型中不存在活变迁，因为该模型存在死标识状态，所以在该标识下任何变迁都是不能发生的。也就是在该模型中数据传输完成的一种状态。

表8 状态空间报告—活性分析

(2)基于Dolev-Yao攻模型的状态空间报告

添加Dolev-Yao攻击模型后输出的状态空间属性报告如表9、表10所示。从表中可见不存在死变迁，说明设计符合安全性。

表9 有界性分析

表10 活性分析

5 结论

本文详细分析TLS1.3握手协议过程，归纳了TLS1.3握手协议内容上改进的措施，使用CPN Tools建模工具层次化建模了TLS1.3握手协议中版本选择以及预主密钥传输和双方身份认证过程，并计算模型生成状态空间报告，之后在此模型上添加了Dolev-Yao攻击模型对TLS1.3握手协议预主密钥传输和身份认证过程进行了安全性分析。最后通过状态空间报告分析验证了TLS1.3握手协议预主密钥和身份认证安全性符合协议设计规范的要求的安全属性。不足之处是本文使用的攻击模型不是强安全攻击模型，在后续研究中将使用攻击能力更强的攻击模型。