一種具有前向安全的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）