蒲鸛雄 繆祥華 袁梅宇

基金項目：云南省計算機技術(shù)應用重點實驗室開放基金（批準號：2021207）資助的課題。

作者簡介：蒲鸛雄（1996 -），碩士研究生，從事安全協(xié)議形式化分析的研究。

通訊作者：繆祥華（1972 -），副教授，從事信息安全、網(wǎng)絡安全、移動通信安全的研究，xianghuamiao @126.com。

引用本文：蒲鸛雄，繆祥華，袁梅宇.一種具有前向安全的TLS協(xié)議0-RTT握手方案[J].化工自動化及儀表，2023，50（6）：

000-000.

DOI：10.20030/j.cnki.1000-3932.202306000

摘? 要? 針對傳輸層安全協(xié)議（TLS）協(xié)議1.3版本在握手消息的第1個flight中傳輸應用數(shù)據(jù)的0-RTT的握手方案，傳輸?shù)脑缙跀?shù)據(jù)由于不存在身份認證，易遭受重放、偽造以及中間人攻擊，且不滿足前向安全的問題，提出一種具有前向安全的0-RTT優(yōu)化握手方案，使用tamarin安全協(xié)議形式化分析工具對改進前、后的協(xié)議進行形式化驗證，結(jié)果表明：改進方案的早期數(shù)據(jù)在原方案之上具有了前向保密的安全性質(zhì)。

關(guān)鍵詞? 傳輸層安全（TLS）? 完美前向安全（PFS）? 0-RTT優(yōu)化握手方案? 安全協(xié)議形式化分析? Tamarin

中圖分類號? TP393? ? ? 文獻標志碼? A? ? ? 文章編號? 1000-3932（2023）06-0000-00

傳輸層安全協(xié)議（TLS）是運行于傳輸控制協(xié)議（TCP）之上的一種安全協(xié)議，其主要功能是為建立連接的通信雙方實體提供一個安全通道，使用該安全通道的實體間擁有認證性，并維護傳輸消息的保密性與完整性。基于TCP的應用在傳輸層的安全需求大都可以使用TLS協(xié)議來達成，TLS 1.2協(xié)議的正式版本在2008年發(fā)布，廣泛地應用于各種應用層協(xié)議之中，其中布署量最大的就是互聯(lián)網(wǎng)中大量的HTTPS（安全超文本傳輸協(xié)議）服務。在TLS1.2協(xié)議不斷更新迭代過程中，設計者發(fā)現(xiàn)了協(xié)議流程中的一些冗余缺陷與使用的加密套件安全問題，例如Crime攻擊、Time攻擊由協(xié)議中所使用的壓縮算法缺陷引起，針對握手協(xié)議的三次握手攻擊[1]，加密套件中RC4算法存在的漏洞[2]，BEAST攻擊、Lucky13攻擊[3]等。

為了滿足不同環(huán)境下存在的更高的安全需求和性能需求，解決以上大量遺留問題[4]，TLS協(xié)議的1.3版本被推出。TLS協(xié)議的1.3版本相對于1.2版本，增強了安全性，并縮短了握手流程來提高性能。安全性增強方面，1.3版本剔除了認證與加密結(jié)合的AEAD（關(guān)聯(lián)數(shù)據(jù)的認證加密）加密算法[5]外的所有傳統(tǒng)的加密算法，并將認證和密鑰交換機制、記錄保護算法、用于密鑰導出功能和握手消息認證碼這幾項使用的散列分離；在握手協(xié)議中，ServerHello之后的所有握手消息都被加密，且使用靜態(tài)參數(shù)的RSA和Diffie-Hellman的密鑰交換方式已被刪除，所有基于公鑰的密鑰交換機制現(xiàn)在都提供前向保密性；在密鑰導出時，TLS協(xié)議1.2版本使用的PRF函數(shù)被替換為了更易于分析的HKDF函數(shù)[6]。性能增強方面，握手協(xié)議中KeyExchange消息已經(jīng)被刪除，客戶端在其第1個flight中即提供了密鑰交換所需的參數(shù)，服務器在接收到參數(shù)后可直接計算出對稱加密所需的密鑰材料，減少了一次往返所需的時間；增加了使用預共享密鑰（PSK）的握手模式，并使用該模式取代了會話恢復機制，通過PSK方法增加了零往返時間（0-RTT）模式，該模式可以讓客戶端在第1個flight即可傳輸應用數(shù)據(jù)，在連接設置時為一些應用數(shù)據(jù)節(jié)省了往返時間，但也犧牲了某些安全屬性。

文獻[7]改進了TLS的0-RTT握手方案，使其安全性增強，以抵御重放攻擊，同時還減少了帶寬開銷，讓該方案更適合在低功耗的物聯(lián)網(wǎng)環(huán)境下應用；他們使用定點模型檢查器（OFMC）提供了形式化的安全性分析，開發(fā)了一種新的中間規(guī)范語言來幫助進行驗證，證明其方案的有效性。文獻[8]使用ProVerif模型檢測工具分析了EAP-TLS認證協(xié)議的安全性，這是TLS在5G認證協(xié)議中的相關(guān)應用，該協(xié)議的RFC（IETF各個工作組組織的互聯(lián)網(wǎng)標準文檔）標準化也正在進行中；該文獻的工作使用基于符號模型檢查的方法對EAP-TLS認證協(xié)議的

相關(guān)安全屬性進行了全面的形式化分析，發(fā)現(xiàn)了當前協(xié)議設計中存在的一些細微缺陷，提出并驗證了一種修復方法，以減輕這些缺陷。文獻[9]分析了TLS1.3協(xié)議在eCK強安全模型下的安全性，通過Scyther工具對TLS1.3接收0-RTT數(shù)據(jù)的兩種方案進行了形式化建模與分析，發(fā)現(xiàn)了其中存在的密鑰泄露偽裝攻擊，使用添加時間戳和早期數(shù)據(jù)簽名的方式使其可以抗重放、偽裝，但依舊不滿足前向安全。

筆者將使用Tamarin模型檢測工具，對TLS協(xié)議1.3版本的PSK-DHE的握手模式進行正確建模，用形式化的方法舉出O-RTT模式中早期數(shù)據(jù)存在的前向安全問題，并提出一種具有前向安全的0-RTT握手方案，再次進行建模分析，與原方案對比，證明改進方案是一種有效且具有前向安全的TLS1.3協(xié)議的0-RTT握手方案。

1? TLS1.3協(xié)議介紹

TLS1.3協(xié)議主要分為握手協(xié)議（Handshake Protocol）、記錄協(xié)議（Record Protocol）和警報協(xié)議（Alert Protocol）。握手協(xié)議為通信雙方建立可信的安全通道；TLS記錄協(xié)議獲取要傳輸?shù)男畔ⅲ瑢?shù)據(jù)分割為受保護的記錄并進行傳輸；警報協(xié)議負責處理TLS連接過程中的各種異常情況，針對各種情況都有一個alert報文，報文中附加一些錯誤處理需要的必要信息，TLS 1.3中定義了30種alert報文。TLS的協(xié)議棧如圖1所示。

筆者主要討論TLS握手協(xié)議，即連接的建立過程，握手協(xié)議也是TLS中最重要的部分[10]，連接建立的安全保障都來自于握手協(xié)議。通信雙方初次握手時的消息流如圖2所示，其中，*表示該項非必須發(fā)送的消息，根據(jù)雙方協(xié)商的結(jié)果可能不會發(fā)送；{}為使用握手密鑰（handshake_traffic_secret）保護的消息；[]為使用應用數(shù)據(jù)密鑰（application_traffic_secret）保護的消息；（）表示使用早期數(shù)據(jù)密鑰（early_traffic_secret）保護的消息。ClientHello中包括客戶端隨機數(shù)與版本、加密套件協(xié)商信息；key_share中包含ECDHE/DHE密鑰交換所需的參數(shù)；EncryptedExtensions為可包含的擴展信息，如主機名、應用層協(xié)議協(xié)商等；CertificateRequest、Certificate、CertificateVerify 3條消息用于請求、驗證、發(fā)送證書；Finished消息用于確認握手的完成，包含了握手信息的消息認證；NewSessionTicket用于建立預共享密鑰（PSK）。

對于初次進行連接建立且沒有在帶外配置PSK的兩個實體，無法使用基于PSK的0-RTT握手模式。在兩端實體經(jīng)過初次握手，客戶端請求PSK且服務器發(fā)送了NewSessionTicket消息后，兩端即可創(chuàng)建PSK用于進行0-RTT模式的握手，該PSK也可被用于僅PSK導出密鑰的高效率握手，但會極大地降低安全性。0-RTT的握手流程如圖3所示。

在0-RTT的握手模式中，key_share不是必須發(fā)送的消息，取決于客戶端在psk_key_exchange_modes中的選項。如果為僅PSK模式，則不會發(fā)送key_share消息，如果為PSK-DHE模式，則會發(fā)送帶有臨時 Diffie-Hellman交換算法所需參數(shù)的key_share消息。

圖3中，在客戶端的第1次飛行中即發(fā)送了應用數(shù)據(jù)，這個應用數(shù)據(jù)被稱為早期數(shù)據(jù)，早期數(shù)據(jù)使用PSK導出的early_traffic_secret進行保護，之后的Finished信息與正式的應用數(shù)據(jù)分別使用handshake_traffic_secret與application_traffic_secret進行保護，這幾項密鑰在PSK-DHE模式下的導出方式如圖4所示。

在PSK-DHE的握手模式中，早期數(shù)據(jù)密鑰的原始秘密（用于導出密鑰的秘密值）為PSK，握手密鑰的原始秘密為雙方協(xié)商的DHE（使用臨時參數(shù)的Diffie-Hellman交換算法）參數(shù)，應用數(shù)據(jù)密鑰的原始秘密為PSK與DHE參數(shù)同時使用。在使用Derive-Secret函數(shù)導出不同的密鑰時，將會使用不同的標簽，但這些標簽都是字符串常量。

2? 形式化建模

Tamarin驗證器是一個強大的安全協(xié)議模型檢測工具，用于對安全協(xié)議進行符號化建模和分析[11]。它將一個安全協(xié)議模型作為輸入，以不同角色來執(zhí)行安全協(xié)議模型中所定義代理采取的行動（模型中定義的代理指一個公共的角色，這個角色可以是協(xié)議發(fā)起者、響應者或受信任的密鑰服務器）。然后指定敵手能力，并定義協(xié)議預期需求的安全屬性。最后，Tamarin可以自動構(gòu)建一個證明，即使在任意多的協(xié)議角色實例平行交錯的情況下，加上敵手的干擾，該協(xié)議也滿足其定義的安全屬性。

2.1? TLS1.3協(xié)議PSK-DHE模式建模

對于協(xié)議模型的建立，Tamarin使用的是安全協(xié)議理論語言（spthy）。該語言使用規(guī)則（rule）描述協(xié)議可能的狀態(tài)，rule中包含的是一系列的事實（fact），既存事實的變化就是協(xié)議狀態(tài)的變化，事實又由一系列術(shù)語組成，這些術(shù)語包括各種加密原語、變量、常量等；使用定理（lemma）來描述希望協(xié)議滿足的安全性質(zhì)，定理由一系列時間變量與邏輯符號組成。其余還有限制（restriction）等規(guī)則用于輔助協(xié)議的建立[12]。

從第1節(jié)對協(xié)議的介紹可知，協(xié)議主要包含兩個參與實體之間的通信：Client與Server。首先，對于PSK-DHE模式下的0-RTT握手，需要在兩個實體間配置一個PSK[13]，這個PSK由首次握手協(xié)商或在帶外配置，將其建模為一個客戶端與服務器間的長期密鑰（Tamarin的規(guī)則中事實是會被消耗的，在事實前添加嘆號表示這是一個長期事實，能被無限制地使用，常用于建模長期密鑰）：

rule Set_PSK：

[Fr（～psk）]

--[]->

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

然后對客戶端的第1次飛行過程進行建模，eadk為早期密鑰，使用Stat事實保存客戶端的部分狀態(tài)，部分值在客戶端的下一次飛行中會使用：

rule Client_1：

let

eadk=HKDF（～psk，～nc）

in

[！GePs（$C，～psk）

，F(xiàn)r（～nc）

，F(xiàn)r（～x）

，F(xiàn)r（～ead）

，F(xiàn)r（～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參數(shù)和隨機數(shù)，自身生成DHE參數(shù)后即可計算出握手密鑰htk與應用數(shù)據(jù)密鑰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（）

，F(xiàn)r（～ns）

，F(xiàn)r（～y）

，F(xiàn)r（～apds）

，F(xiàn)r（～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）>）]

對客戶端最后一次飛行進行建模，使用首次飛行中保留的部分狀態(tài)與服務器發(fā)送的各項參數(shù)計算htk與apk，發(fā)送Finished與應用數(shù)據(jù)，整個握手流程結(jié)束：

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（）

，F(xiàn)r（～apdc）

，F(xiàn)r（～cFi）

]

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

Recv_2（$C，Y）

]->

[Out（）]

2.2? 安全性質(zhì)建模

安全性質(zhì)方面主要考慮的是0-RTT握手中早期數(shù)據(jù)的前向安全性質(zhì)。對于其認證相關(guān)性質(zhì)，由于TLS1.3的1-RTT與0-RTT方案是在沒有經(jīng)過完整連接建立的情況下即發(fā)送了數(shù)據(jù)，使用基于PSK的握手時不允許請求證書，是容易遭到偽造與重放的。故參考文獻[15，16]的工作，在服務器與客戶端往外發(fā)送的消息中添加他們自身的簽名與消息的MAC（消息認證碼）保障認證性質(zhì)。本研究的重點仍在于早期數(shù)據(jù)的前向安全。

首先根據(jù)Dolev-Yao敵手模型[17]與eCK強安全模型[18]的敵手能力，使得敵手能夠獲取公共信道上的數(shù)據(jù)，并能揭露長期密鑰，以及在公共信道發(fā)送自己偽造的信息。以下的前兩條為Tamarin中的內(nèi)置規(guī)則，！KU（x）指攻擊者知曉x：

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

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

rule Reveal_ltpsk：

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

然后定義兩條存在性定理，用于證明協(xié)議的正確性。第1條為客戶端發(fā)送早期數(shù)據(jù)后，能夠證明服務器可以獲取到早期數(shù)據(jù)；第2條為服務器發(fā)送應用數(shù)據(jù)后，能夠證明客戶端獲取到應用數(shù)據(jù)：

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"

接下來定義早期數(shù)據(jù)的保密性質(zhì)與前向安全性質(zhì)[19]。exists-trace表示追蹤該定理是否存在，對前向保密性的定義使用否定前向保密性質(zhì)的證明是否存在來進行建模，即如果不存在一個否定前向保密性的證明，即說明滿足前向保密：

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協(xié)議0-RTT模式驗證分析

根據(jù)筆者定義的安全性質(zhì)模型進行檢測后的結(jié)果見表1。對于兩條存在性定理皆檢測通過，早期數(shù)據(jù)的保密性和前向安全皆驗證失敗。

該結(jié)果表示，存在正確的路徑使得早期數(shù)據(jù)和應用數(shù)據(jù)能夠正確地被發(fā)送和接收。但存在不安全的路徑使得早期數(shù)據(jù)會被敵手知曉，保密性和前向安全皆無法保證。敵手獲取早期數(shù)據(jù)的路徑如圖5所示。

敵手獲取早期數(shù)據(jù)的流程如下：

a. 敵手截獲客戶端向服務器發(fā)送的第1個飛行中的消息，獲取其中明文傳輸?shù)碾S機數(shù)nc；

b. 從上述消息中同樣獲取早期數(shù)據(jù)的密文senc（～ead，HKDF（～psk，～nc））；

c. 敵手通過Reveal_ltpsk規(guī)則導出長期預共享密鑰～psk；

d. 敵手計算HKDF（～psk，～nc）得到早期數(shù)據(jù)密鑰，解密密文獲取到早期數(shù)據(jù)ead。

4? 改進方法及驗證結(jié)果

通過攻擊路徑可知，因為早期數(shù)據(jù)密鑰導出使用的原始秘密只有PSK，使得只要PSK被揭露，敵手就可以獲取到早期數(shù)據(jù)密鑰。而PSK是一個長期密鑰，被敵手揭露的可能性較大[20]，且被揭露后每次會話的早期數(shù)據(jù)都會被敵手獲取，不滿足前向安全。

4.1? 改進方法

PSK通過兩個實體初次握手發(fā)送的NewSessionTicket消息創(chuàng)建，PSK握手模式的選項在psk_key_exchange_modes中選擇，除僅PSK模式和PSK-DHE模式外，在其中添加0-RTT-PFS模式，服務端接收到此模式的消息后，以創(chuàng)建一個DH參數(shù)來替代NewSessionTicket的PSK，將這個參數(shù)記為'g'^z，在Tamarin中的形式化描述如下：

rule Set_0RTT_PFS：

[Fr（～z）]

--[]->

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

并且將這個DH參數(shù)對兩個實體之間的綁定事實設定為非長期事實，它們只在導出早期數(shù)據(jù)密鑰時使用一次。

對客戶端的第1次飛行的形式化描述改變?nèi)缦拢缙跀?shù)據(jù)密鑰的導出使用初次會話中獲取的服務器DH參數(shù)'g'^z與客戶端參數(shù)x計算：

rule Client_1：

let

Z='g'^z

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

in

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

，F(xiàn)r（～nc）

，F(xiàn)r（～x）

，F(xiàn)r（～ead）

，F(xiàn)r（～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次飛行的形式化描述中，與客戶端同樣，將早期數(shù)據(jù)密鑰的導出方式改為一次DH運算。即eadk=HKDF（X^～z，rc），其余部分的形式化基本相同，此處省略。

4.2? 驗證結(jié)果

使用上述方法對PSK-DHE的0-RTT模式進行改進后，使用相同的安全性質(zhì)定理對其進行分析，分析驗證的結(jié)果見表2，對早期數(shù)據(jù)的保密性與前向安全性的驗證皆得到滿足。

5? 結(jié)束語

使用Tamarin對TLS1.3版本的PSK-DHE模式的握手協(xié)議進行了形式化建模，同時對其中的早期數(shù)據(jù)的保密性與前向保密性進行了安全性質(zhì)的形式化建模，證明0-RTT的早期數(shù)據(jù)在預共享密鑰被揭露后無法滿足保密性與前向安全。針對上述問題提出了改進措施，根據(jù)客戶端選項，服務器向客戶端提供一個保障前向安全的DH參數(shù)來進行具有前向安全的0-RTT握手。這種方式?jīng)]有增加往返時間，但客戶端和服務器都需要額外進行一次DH運算，增加了計算開銷，但該方案可以根據(jù)客戶端選項調(diào)整，對于資源較為受限的客戶端或服務器，可以采用原本的0-RTT握手，較為靈活。

TLS協(xié)議的1.3版本的標準化文檔雖已上線數(shù)年，但仍然無法撼動1.2版本的地位，使用1.3版本的網(wǎng)站、應用數(shù)量稀少。為進行普及，出現(xiàn)了大量TLS1.3的改進協(xié)議與分析文獻。在筆者所建立模型的基礎(chǔ)上進行修改，可以進一步對各種TLS改進協(xié)議進行分析。

參? 考? 文? 獻

[1] BHARGAVAN K，LAVAUD A，F(xiàn)OURNET 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協(xié)議設計和實現(xiàn)中的安全缺陷綜述[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 協(xié)議的形式化分析與優(yōu)化[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 協(xié)議形式化分析及其改進方法[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，F(xiàn)ISCHLIN 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）