一种具有前向安全的TLS协议0-RTT握手方案

蒲鹳雄 缪祥华 袁梅宇

基金项目：云南省计算机技术应用重点实验室开放基金（批准号：2021207）资助的课题。

作者简介：蒲鹳雄（1996 -），硕士研究生，从事安全协议形式化分析的研究。

通讯作者：缪祥华（1972 -），副教授，从事信息安全、网络安全、移动通信安全的研究，xianghuamiao @126.com。

引用本文：蒲鹳雄，缪祥华，袁梅宇.一种具有前向安全的TLS协议0-RTT握手方案[J].化工自动化及仪表，2023，50（6）：

000-000.

DOI：10.20030/j.cnki.1000-3932.202306000

摘  要  针对传输层安全协议（TLS）协议1.3版本在握手消息的第1个flight中传输应用数据的0-RTT的握手方案，传输的早期数据由于不存在身份认证，易遭受重放、伪造以及中间人攻击，且不满足前向安全的问题，提出一种具有前向安全的0-RTT优化握手方案，使用tamarin安全协议形式化分析工具对改进前、后的协议进行形式化验证，结果表明：改进方案的早期数据在原方案之上具有了前向保密的安全性质。

关键词  传输层安全（TLS）  完美前向安全（PFS）  0-RTT优化握手方案  安全协议形式化分析  Tamarin

中图分类号  TP393      文献标志码  A      文章编号  1000-3932（2023）06-0000-00

传输层安全协议（TLS）是运行于传输控制协议（TCP）之上的一种安全协议，其主要功能是为建立连接的通信双方实体提供一个安全通道，使用该安全通道的实体间拥有认证性，并维护传输消息的保密性与完整性。基于TCP的应用在传输层的安全需求大都可以使用TLS协议来达成，TLS 1.2协议的正式版本在2008年发布，广泛地应用于各种应用层协议之中，其中布署量最大的就是互联网中大量的HTTPS（安全超文本传输协议）服务。在TLS1.2协议不断更新迭代过程中，设计者发现了协议流程中的一些冗余缺陷与使用的加密套件安全问题，例如Crime攻击、Time攻击由协议中所使用的压缩算法缺陷引起，针对握手协议的三次握手攻击[1]，加密套件中RC4算法存在的漏洞[2]，BEAST攻击、Lucky13攻击[3]等。

为了满足不同环境下存在的更高的安全需求和性能需求，解决以上大量遗留问题[4]，TLS协议的1.3版本被推出。TLS协议的1.3版本相对于1.2版本，增强了安全性，并缩短了握手流程来提高性能。安全性增强方面，1.3版本剔除了认证与加密结合的AEAD（关联数据的认证加密）加密算法[5]外的所有传统的加密算法，并将认证和密钥交换机制、记录保护算法、用于密钥导出功能和握手消息认证码这几项使用的散列分离；在握手协议中，ServerHello之后的所有握手消息都被加密，且使用静态参数的RSA和Diffie-Hellman的密钥交换方式已被删除，所有基于公钥的密钥交换机制现在都提供前向保密性；在密钥导出时，TLS协议1.2版本使用的PRF函数被替换为了更易于分析的HKDF函数[6]。性能增强方面，握手协议中KeyExchange消息已经被删除，客户端在其第1个flight中即提供了密钥交换所需的参数，服务器在接收到参数后可直接计算出对称加密所需的密钥材料，减少了一次往返所需的时间；增加了使用预共享密钥（PSK）的握手模式，并使用该模式取代了会话恢复机制，通过PSK方法增加了零往返时间（0-RTT）模式，该模式可以让客户端在第1个flight即可传输应用数据，在连接设置时为一些应用数据节省了往返时间，但也牺牲了某些安全属性。

文献[7]改进了TLS的0-RTT握手方案，使其安全性增强，以抵御重放攻击，同时还减少了带宽开销，让该方案更适合在低功耗的物联网环境下应用；他们使用定点模型检查器（OFMC）提供了形式化的安全性分析，开发了一种新的中间规范语言来帮助进行验证，证明其方案的有效性。文献[8]使用ProVerif模型检测工具分析了EAP-TLS认证协议的安全性，這是TLS在5G认证协议中的相关应用，该协议的RFC（IETF各个工作组组织的互联网标准文档）标准化也正在进行中；该文献的工作使用基于符号模型检查的方法对EAP-TLS认证协议的

相关安全属性进行了全面的形式化分析，发现了当前协议设计中存在的一些细微缺陷，提出并验证了一种修复方法，以减轻这些缺陷。文献[9]分析了TLS1.3协议在eCK强安全模型下的安全性，通过Scyther工具对TLS1.3接收0-RTT数据的两种方案进行了形式化建模与分析，发现了其中存在的密钥泄露伪装攻击，使用添加时间戳和早期数据签名的方式使其可以抗重放、伪装，但依旧不满足前向安全。

笔者将使用Tamarin模型检测工具，对TLS协议1.3版本的PSK-DHE的握手模式进行正确建模，用形式化的方法举出O-RTT模式中早期数据存在的前向安全问题，并提出一种具有前向安全的0-RTT握手方案，再次进行建模分析，与原方案对比，证明改进方案是一种有效且具有前向安全的TLS1.3协议的0-RTT握手方案。

1  TLS1.3协议介绍

TLS1.3协议主要分为握手协议（Handshake Protocol）、记录协议（Record Protocol）和警报协议（Alert Protocol）。握手协议为通信双方建立可信的安全通道；TLS记录协议获取要传输的信息，将数据分割为受保护的记录并进行传输；警报协议负责处理TLS连接过程中的各种异常情况，针对各种情况都有一个alert报文，报文中附加一些错误处理需要的必要信息，TLS 1.3中定义了30种alert报文。TLS的协议栈如图1所示。

笔者主要讨论TLS握手协议，即连接的建立过程，握手协议也是TLS中最重要的部分[10]，连接建立的安全保障都来自于握手协议。通信双方初次握手时的消息流如图2所示，其中，*表示该项非必须发送的消息，根据双方协商的结果可能不会发送；{}为使用握手密钥（handshake_traffic_secret）保护的消息；[]为使用应用数据密钥（application_traffic_secret）保护的消息；（）表示使用早期数据密钥（early_traffic_secret）保护的消息。ClientHello中包括客户端随机数与版本、加密套件协商信息；key_share中包含ECDHE/DHE密钥交换所需的参数；EncryptedExtensions为可包含的扩展信息，如主机名、应用层协议协商等；CertificateRequest、Certificate、CertificateVerify 3条消息用于请求、验证、发送证书；Finished消息用于确认握手的完成，包含了握手信息的消息认证；NewSessionTicket用于建立预共享密钥（PSK）。

对于初次进行连接建立且没有在带外配置PSK的两个实体，无法使用基于PSK的0-RTT握手模式。在两端实体经过初次握手，客户端请求PSK且服务器发送了NewSessionTicket消息后，两端即可创建PSK用于进行0-RTT模式的握手，该PSK也可被用于仅PSK导出密钥的高效率握手，但会极大地降低安全性。0-RTT的握手流程如图3所示。

在0-RTT的握手模式中，key_share不是必须发送的消息，取决于客户端在psk_key_exchange_modes中的选项。如果为仅PSK模式，则不会发送key_share消息，如果为PSK-DHE模式，则会发送带有临时 Diffie-Hellman交换算法所需参数的key_share消息。

图3中，在客户端的第1次飞行中即发送了应用数据，这个应用数据被称为早期数据，早期数据使用PSK导出的early_traffic_secret进行保护，之后的Finished信息与正式的应用数据分别使用handshake_traffic_secret与application_traffic_secret进行保护，这几项密钥在PSK-DHE模式下的导出方式如图4所示。

在PSK-DHE的握手模式中，早期数据密钥的原始秘密（用于导出密钥的秘密值）为PSK，握手密钥的原始秘密为双方协商的DHE（使用临时参数的Diffie-Hellman交换算法）参数，应用数据密钥的原始秘密为PSK与DHE参数同时使用。在使用Derive-Secret函数导出不同的密钥时，将会使用不同的标签，但这些标签都是字符串常量。

2  形式化建模

Tamarin验证器是一个强大的安全协议模型检测工具，用于对安全协议进行符号化建模和分析[11]。它将一个安全协议模型作为输入，以不同角色来执行安全协议模型中所定义代理采取的行动（模型中定义的代理指一个公共的角色，这个角色可以是协议发起者、响应者或受信任的密钥服务器）。然后指定敌手能力，并定义协议预期需求的安全属性。最后，Tamarin可以自动构建一个证明，即使在任意多的协议角色实例平行交错的情况下，加上敌手的干扰，该协议也满足其定义的安全属性。

2.1  TLS1.3协议PSK-DHE模式建模

对于协议模型的建立，Tamarin使用的是安全协议理论语言（spthy）。该语言使用规则（rule）描述协议可能的状态，rule中包含的是一系列的事实（fact），既存事实的变化就是协议状态的变化，事实又由一系列术语组成，这些术语包括各种加密原语、变量、常量等；使用定理（lemma）来描述希望协议满足的安全性质，定理由一系列时间变量与逻辑符号组成。其余还有限制（restriction）等规则用于辅助协议的建立[12]。

从第1节对协议的介绍可知，协议主要包含两个参与实体之间的通信：Client与Server。首先，对于PSK-DHE模式下的0-RTT握手，需要在两个实体间配置一个PSK[13]，这个PSK由首次握手协商或在带外配置，将其建模为一个客户端与服务器间的长期密钥（Tamarin的规则中事实是会被消耗的，在事实前添加叹号表示这是一个长期事实，能被无限制地使用，常用于建模长期密钥）：

rule Set_PSK：

[Fr（～psk）]

--[]->

[！GePs（$C，～psk），！GePs（$S，～psk）]

然后对客户端的第1次飞行过程进行建模，eadk为早期密钥，使用Stat事实保存客户端的部分状态，部分值在客户端的下一次飞行中会使用：

rule Client_1：

let

eadk=HKDF（～psk，～nc）

in

[！GePs（$C，～psk）

，Fr（～nc）

，Fr（～x）

，Fr（～ead）

，Fr（～tid）

]

--[Send_1（$C，senc（～ead，eadk）），Honest（$C），Honest（$S）

]->

[Stat_C1（～tid，$C，$S，～nc，～x）

，Out（<～nc，'g'^～x，senc（～ead，eadk）>）]

對服务器的第1次飞行进行建模，由于服务器接收到了来自客户端的DHE参数和随机数，自身生成DHE参数后即可计算出握手密钥htk与应用数据密钥apk，之后的信息都将受到保护[14]：

rule Server_1：

let

eadk=HKDF（～psk，rc）

htk=HKDF（X^～y，）

apk=HKDF（，）

eads=sdec（senc（ead，eadk），HKDF（～psk，rc））

in

[！GePs（$S，～psk）

，In（）

，Fr（～ns）

，Fr（～y）

，Fr（～apds）

，Fr（～sFi）

]

--[Secret（eads），Honest（$C），Honest（$S），Role（'S'），

Recv_1（$S，senc（ead，eadk）），Send_2（$S，'g'^～y），

]->

[Out（<～ns，'g'^～y，senc（～sFi，htk），senc（～apds，apk）>）]

对客户端最后一次飞行进行建模，使用首次飞行中保留的部分状态与服务器发送的各项参数计算htk与apk，发送Finished与应用数据，整个握手流程结束：

rule Client_2：

let

htk=HKDF（Y^～x，<～nc，rs>）

sfi=sdec（senc（sFi，htk），htk）

apk=HKDF（，<～nc，sfi>）

apdr=sdec（senc（apds，apk），apk）

in

[！GePs（$C，～psk）

，Stat_C1（～tid，$C，$S，～nc，～x）

，In（）

，Fr（～apdc）

，Fr（～cFi）

]

--[Secret（apdr），Honest（$C），Honest（$S），Role（'C'），

Recv_2（$C，Y）

]->

[Out（）]

2.2  安全性质建模

安全性质方面主要考虑的是0-RTT握手中早期数据的前向安全性质。对于其认证相关性质，由于TLS1.3的1-RTT与0-RTT方案是在没有经过完整连接建立的情况下即发送了数据，使用基于PSK的握手时不允许请求证书，是容易遭到伪造与重放的。故参考文献[15，16]的工作，在服务器与客户端往外发送的消息中添加他们自身的签名与消息的MAC（消息认证码）保障认证性质。本研究的重点仍在于早期数据的前向安全。

首先根据Dolev-Yao敌手模型[17]与eCK强安全模型[18]的敌手能力，使得敌手能够获取公共信道上的数据，并能揭露长期密钥，以及在公共信道发送自己伪造的信息。以下的前两条为Tamarin中的内置规则，！KU（x）指攻击者知晓x：

[Out（x）]->[！KU（x）]

[！KU（x）]--[K（x）]->[In（x）].

rule Reveal_ltpsk：

[！GePs（$X，pskX）]--[Reveal（$X）]->[Out（pskX）]

然后定义两条存在性定理，用于证明协议的正确性。第1条为客户端发送早期数据后，能够证明服务器可以获取到早期数据；第2条为服务器发送应用数据后，能够证明客户端获取到应用数据：

lemma executable_ead：

exists-trace

"Ex C S m #i #j.Send_1（C，m）@i & Recv_1（S，m）@j"

lemma executable_apd：

exists-trace

"Ex C S m #i #j.Send_2（S，m）@i & Recv_2（C，m）@j"

接下来定义早期数据的保密性质与前向安全性质[19]。exists-trace表示追踪该定理是否存在，对前向保密性的定义使用否定前向保密性质的证明是否存在来进行建模，即如果不存在一个否定前向保密性的证明，即说明满足前向保密：

lemma secret_ead：

all-traces

"All n #i.Secret（n）@i & Role（'S'）@i ==>

not（Ex #j.K（n）@j）|（Ex S #r.Reveal（S）@r & Honest（S）@i）"

lemma secrecy_PFS_ead：

exists-trace

"not All n #i.

Secret（n）@i & Role（'S'）@i==>not（Ex #j.K（n）@j）|

（Ex S #r.Reveal（S）@r & Honest（S）@i & r

3  TLS1.3協议0-RTT模式验证分析

根据笔者定义的安全性质模型进行检测后的结果见表1。对于两条存在性定理皆检测通过，早期数据的保密性和前向安全皆验证失败。

该结果表示，存在正确的路径使得早期数据和应用数据能够正确地被发送和接收。但存在不安全的路径使得早期数据会被敌手知晓，保密性和前向安全皆无法保证。敌手获取早期数据的路径如图5所示。

敌手获取早期数据的流程如下：

a. 敌手截获客户端向服务器发送的第1个飞行中的消息，获取其中明文传输的随机数nc；

b. 从上述消息中同样获取早期数据的密文senc（～ead，HKDF（～psk，～nc））；

c. 敌手通过Reveal_ltpsk规则导出长期预共享密钥～psk；

d. 敌手计算HKDF（～psk，～nc）得到早期数据密钥，解密密文获取到早期数据ead。

4  改进方法及验证结果

通过攻击路径可知，因为早期数据密钥导出使用的原始秘密只有PSK，使得只要PSK被揭露，敌手就可以获取到早期数据密钥。而PSK是一个长期密钥，被敌手揭露的可能性较大[20]，且被揭露后每次会话的早期数据都会被敌手获取，不满足前向安全。

4.1  改进方法

PSK通过两个实体初次握手发送的NewSessionTicket消息创建，PSK握手模式的选项在psk_key_exchange_modes中选择，除仅PSK模式和PSK-DHE模式外，在其中添加0-RTT-PFS模式，服务端接收到此模式的消息后，以创建一个DH参数来替代NewSessionTicket的PSK，将这个参数记为'g'^z，在Tamarin中的形式化描述如下：

rule Set_0RTT_PFS：

[Fr（～z）]

--[]->

[GeDhc（$C，'g'^～z），GeDhs（$S，～z）]

并且将这个DH参数对两个实体之间的绑定事实设定为非长期事实，它们只在导出早期数据密钥时使用一次。

对客户端的第1次飞行的形式化描述改变如下，早期数据密钥的导出使用初次会话中获取的服务器DH参数'g'^z与客户端参数x计算：

rule Client_1：

let

Z='g'^z

eadk=HKDF（Z^～x，～nc）

in

[GeDhc（$C，'g'^z）

，Fr（～nc）

，Fr（～x）

，Fr（～ead）

，Fr（～tid）

]

--[Send_1（$C，senc（～ead，eadk）），Honest（$C），Honest（$S）

]->

[Stat_C1（～tid，$C，$S，～nc，～x）

，Out（<～nc，'g'^～x，senc（～ead，eadk）>）]

在服务器的第1次飞行的形式化描述中，与客户端同样，将早期数据密钥的導出方式改为一次DH运算。即eadk=HKDF（X^～z，rc），其余部分的形式化基本相同，此处省略。

4.2  验证结果

使用上述方法对PSK-DHE的0-RTT模式进行改进后，使用相同的安全性质定理对其进行分析，分析验证的结果见表2，对早期数据的保密性与前向安全性的验证皆得到满足。

5  结束语

使用Tamarin对TLS1.3版本的PSK-DHE模式的握手协议进行了形式化建模，同时对其中的早期数据的保密性与前向保密性进行了安全性质的形式化建模，证明0-RTT的早期数据在预共享密钥被揭露后无法满足保密性与前向安全。针对上述问题提出了改进措施，根据客户端选项，服务器向客户端提供一个保障前向安全的DH参数来进行具有前向安全的0-RTT握手。这种方式没有增加往返时间，但客户端和服务器都需要额外进行一次DH运算，增加了计算开销，但该方案可以根据客户端选项调整，对于资源较为受限的客户端或服务器，可以采用原本的0-RTT握手，较为灵活。

TLS协议的1.3版本的标准化文档虽已上线数年，但仍然无法撼动1.2版本的地位，使用1.3版本的网站、应用数量稀少。为进行普及，出现了大量TLS1.3的改进协议与分析文献。在笔者所建立模型的基础上进行修改，可以进一步对各种TLS改进协议进行分析。

参  考  文  献

[1] BHARGAVAN K，LAVAUD A，FOURNET C，et al.Triple handshakes and cookie cutters：Breaking and fixing authentication over TLS[C]//2014 IEEE Symposium on Security and Privacy.Berkeley，CA，USA：IEEE Computer Society，2014：98?113.DOI：10.1109/SP.2014.14.

[2] ALFARDAN N，BERNSTEIN D，PATERSON K，et al.On the security of RC4 in TLS[C]//Proceedings of the 22nd USENIX conference on Security.USENIX Association，2013：305?320.

[3] FARDAN N J A，PATERSON K G.Lucky thirteen：Breaking the TLS and DTLS record protocols[C]//2013 IEEE Symposium on Security and Privacy.Berkeley，CA，USA：IEEE Computer Society，2013：526?540.DOI：10.1109/SP.2013.42.

[4] 韦俊琳，段海新，万涛.HTTPS/TLS协议设计和实现中的安全缺陷综述[J].信息安全学报，2018，3（2）：1-15.

[5] McGREW D. An Interface and Algorithms for Authenticated Encryption[R].IETF RFC5116，2008.www.rfc-editor.org/rfc/rfc5116.txt.

[6] KRAWCZYK H，ERONEN P.HMAC-based Extract-and-Expand Key Derivation Function（HKDF）[R].IETF RFC 5869，2010.www.rfc-editor.org/rfc/rfc5869.txt.

[7] TANGE K，M?DERSHEIM S，LALOS A，et al.rTLS：Secure and Efficient TLS Session Resumption for the Internet of Things[J].Sensors，2021，21（19）：6524.

[8] ZHANG J J，YANG L，CAO W P，et al.Formal analysis of 5G EAP-TLS authentication protocol using proverif[J].IEEE access，2020（8）：23674-23688.

[9] 陆思奇，周思渊，毛颖.强安全模型下 TLS1.3 协议的形式化分析与优化[J].软件学报，2021，32（9）2849-2866.

[10] CREMERS C，HORVAT M，HOYLAND J，et al.A comprehensive symbolic analysis of TLS 1.3[C]//Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security.NewYork：ACM，2017：1773-1788.DOI：10.1145/3133956.3134063.

[11] MEIER S，SCHMIDT B，CREMERS C，et al.The TAMARIN prover for the symbolic analysis of security protocols[C]//International conference on computer aided verification.Springer.Berlin，Heidelberg，2013：696-701.

[12] 刘镝，王梓屹，李大伟，等.基于 Tamarin 的 5G AKA 协议形式化分析及其改进方法[J].密码学报，2021，9（2）：237-247.

[13] CREMERS C，HORVAT M，SCOTT S，et al.Automated analysis and verification of TLS 1.3：0-RTT，resumption and delayed authentication[C]//2016 IEEE Symposium on Security and Privacy（SP）.Piscataway，NJ：IEEE，2016：470-485.

[14] BHARGAVAN K，BLANCHET B，KOBEISSI N.Verified models and reference implementations for the TLS 1.3 standard candidate[C]//2017 IEEE Symposium on Security and Privacy（SP）.Piscataway，NJ：IEEE，2017：483-502.

[15] DOWLING B，FISCHLIN M，G?NTHER F，et al.A cryptographic analysis of the TLS 1.3 handshake protocol candidates[C]//Proceedings of the 22nd ACM SIGSAC conference on computer and communications security. NewYork：ACM，2015：1197-1210.

[16] FISCHLIN M，G?NTHER F，SCHMIDT B，et al.Key confirmation in key exchange：A formal treatment and implications for TLS 1.3[C]//2016 IEEE Symposium on Security and Privacy（SP）.Piscataway，NJ：IEEE，2016：452-469.

[17] DOLEV D，YAO A C.On the security of public key protocols[J].IEEE Transactions on Information Theory，1983，29（2）：198-208.

[18] CANETTI R，KRAWCZYK H.Analysis of key-exchange protocols and their use for building secure channels[C]//Proceedings of the Advances in Cryptology（EUROCRYPT 2001）.Berlin：Springer-Verlag，2001：453?474.

[19] KRAWCZYK H.HMQV：A high-performance secure Diffie-Hellman protocol[C]//Annual International Cryptology Conference.Berlin，Heidelberg：Springer，2005：546-566.

[20] CELI S，HOYLAND J，STEBILA D，et al.A tale of two models：Formal verification of KEMTLS via Tamarin[C]//European Symposium on Research in Computer Security. Heidelberg：Springer，2022：63-83.

（收稿日期：2022-12-28，修回日期：2023-03-14）