基于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握手協議預主密鑰和身份認證安全性符合協議設計規范的要求的安全屬性。不足之處是本文使用的攻擊模型不是強安全攻擊模型，在后續研究中將使用攻擊能力更強的攻擊模型。