基于HCPN模型的TLS1.3協(xié)議安全性分析

陳真好，田學(xué)成

(1.南京天暢信息技術(shù)有限公司，江蘇 南京 211100；2.國電南京自動(dòng)化股份有限公司，江蘇 南京 211100)

0 引言

TLS協(xié)議作為一種協(xié)議安全機(jī)制最初是由Netscape Communications公司與1995年開發(fā)的安全套接層（Secure Sockets Layer，SSL）演變而來的[1]，之后由國際互聯(lián)網(wǎng)工程任務(wù)組(Internet Engineering Task Force，IETF)指定規(guī)范并逐漸升級(jí)到TLS1.2。在不斷的使用過程中發(fā)現(xiàn)TLS協(xié)議存在很多安全風(fēng)險(xiǎn)[2]。新發(fā)布的TLS1.3版本協(xié)議內(nèi)容上較之前有較大的改變，增強(qiáng)了算法的安全性，同時(shí)減少了會(huì)話次數(shù)，提高了效率[3]。在TLS1.3協(xié)議安全研究方面，Cas Cremers等人使用Tamarin工具對(duì)協(xié)議做符號(hào)形式化的分析[4]，但該工具攻擊模型需要手動(dòng)輸入，設(shè)置比較復(fù)雜很難掌握，并且不能反映協(xié)議執(zhí)行細(xì)節(jié)問題。王小峰等人使用基于Applied PI演算對(duì)TLS1.3做形式化建模[5]，使用分析工具ProVerify驗(yàn)證了握手協(xié)議的認(rèn)證性和預(yù)主密鑰的機(jī)密性，但該工具在協(xié)議漏洞發(fā)現(xiàn)上存在欠缺，只能用來驗(yàn)證協(xié)議的安全屬性是否符合規(guī)范。

本文使用CPN Tools形式化建模工具分析TLS1.3握手協(xié)議。CPN Tools建模工具可以直觀地描述協(xié)議執(zhí)行的細(xì)節(jié)問題，并且根據(jù)需要添加網(wǎng)絡(luò)時(shí)間延遲，更加細(xì)致地模擬協(xié)議執(zhí)行過程。它提供狀態(tài)空間分析方法和模型檢測(cè)來驗(yàn)證協(xié)議安全性能。因?yàn)門LS握手協(xié)議密鑰建立方式的復(fù)雜性和身份認(rèn)證的多樣性，本文基于密鑰建立方式為有限域上的橢圓曲線方法[3]?；趯哟沃玃etri網(wǎng)(HCPN)[6]的建模方法使用CPN Tools工具對(duì)TLS1.3握手協(xié)議進(jìn)行建模，分析其狀態(tài)空間，并添加Delov-Yao[7]敵手攻擊模型，驗(yàn)證協(xié)議的安全屬性，根據(jù)狀態(tài)空間輸出的數(shù)據(jù)判斷TLS1.3握手協(xié)議預(yù)主密鑰和身份認(rèn)證的安全性是否滿足協(xié)議規(guī)范的安全屬性要求。

1 TLS1.3握手協(xié)議

1.1 密鑰建立方式

TLS1.3實(shí)現(xiàn)身份認(rèn)證和密鑰交換都是通過TLS的擴(kuò)展部分實(shí)現(xiàn)，故TLS1.3密碼套件(CipherSuite)僅用來加密和實(shí)現(xiàn)散列哈希算法，減少至5個(gè)密碼套件[3]，見表1。

表1 TLS1.3密碼套件

TLS1.3握手協(xié)議在協(xié)議算法上較之前有很大改變，因?yàn)殪o態(tài)的RSA算法不提供向前安全(Perfect Forward Secrecy，PFS)[2]，容易被攻擊者竊聽通信消息獲取服務(wù)器私鑰，所以在TLS1.3中被棄用，TLS1.3不再支持密鑰的壓縮算法，同時(shí)刪除了很多已存在安全隱患的算法。目前TLS1.3只支持三種基本的密鑰交換模式：

(1)(EC)DHE：Diffie-Hellman在有限域上或橢圓曲線上密鑰交換模式。

(2)Pre-shared-key(PSK)：預(yù)主密鑰模式。

(3)將上面兩者結(jié)合的模式。

本文基于有限域上橢圓曲線密鑰交換方式建模。由于TLS握手協(xié)議的復(fù)雜性和認(rèn)證方式的多樣性，在使用CPN Tools建模分析TLS1.3握手協(xié)議過程中重點(diǎn)分析了密鑰協(xié)商和身份認(rèn)證的安全屬性。

1.2 TLS握手協(xié)議會(huì)話過程

TLS協(xié)議的主要目的是保護(hù)上層協(xié)議安全透明地傳輸，其協(xié)議組成主要有握手協(xié)議和記錄協(xié)議，TLS握手協(xié)議實(shí)現(xiàn)密鑰協(xié)商和身份驗(yàn)證以及數(shù)據(jù)完整性驗(yàn)證。TLS1.3握手協(xié)議較之前TLS1.2會(huì)話過程發(fā)生很大改變。TLS1.2在發(fā)送應(yīng)用程序數(shù)據(jù)之前需要往返兩次(2-RTT)才能完成握手，而TLS1.3只需要往返一次(1-RTT)即可完成[2]，在時(shí)間效率上大大提高。

TLS1.3不再支持靜態(tài)的RSA密碼交換算法，而是使用帶有向前安全的Diffie-Hellman進(jìn)行全面握手。使用特殊的擴(kuò)展來發(fā)送密鑰協(xié)商使用的參數(shù)。ServerHello消息發(fā)送之后增加了加密EncryptedExtension消息[3]，響應(yīng)與密鑰協(xié)商參數(shù)無關(guān)的其他擴(kuò)展。使用臨時(shí)密鑰加密減少了可見明文的數(shù)量，提高了安全性，同時(shí)禁止雙方發(fā)起重新協(xié)商。刪除了Change_ChipherSpec協(xié)議和ServerKeyExchange、Client-KeyExchange消息。會(huì)話的恢復(fù)方式被預(yù)主密鑰(pre_shared_key)模式替代，TLS1.3握手協(xié)議會(huì)話恢復(fù)方式較TLS1.2有較大改變，棄用了TLS1.2使用SessionID連接方式，同時(shí)減少了會(huì)話次數(shù)，提高了效率。

TLS1.3握手協(xié)議會(huì)話過程如圖1所示。

圖1 TLS1.3握手協(xié)議會(huì)話過程

2 著色Petri網(wǎng)的概念和屬性

2.1 著色Petri的定義

Colored Petri Nets(CPN)[8]是基于Petri網(wǎng)基礎(chǔ)上提出的一種高級(jí)Petri網(wǎng)，CPN不但保留了Petri的優(yōu)點(diǎn)，提供了可操作界面，而且增加了語言表達(dá)能力、顏色集等。CPN是一種可以對(duì)系統(tǒng)進(jìn)行檢驗(yàn)和仿真的建模語言，用于描述和分析具有通信、同步、并發(fā)、分布等特征的復(fù)雜系統(tǒng)。HCPN模型是在著色Petri網(wǎng)的基礎(chǔ)上增加了層次模型和子模塊的概念，使Petri網(wǎng)成為經(jīng)典Petri網(wǎng)，它是一個(gè)有向的連通圖，由庫所和變遷兩種節(jié)點(diǎn)以及他們之間的弧構(gòu)成，定義如下。

定義1Colored Petri Net是一個(gè)九元組CPN=(P，T，A，Σ，C，V，G，E，I)[9]，其中：

P：一個(gè)有限的庫所(Place)的集合，代表一種數(shù)據(jù)資源，用橢圓表示。

T：有限變遷的集合，且T滿足P∩T=φ，描述系統(tǒng)活動(dòng)，用矩形表示。

A：是一個(gè)有向弧的集合，滿足A?PxT∪TxP，代表數(shù)據(jù)資源的流動(dòng)方向，用箭頭表示。從庫所到變遷的弧描述變遷被觸發(fā)的條件。從變遷到庫所的弧描述變遷點(diǎn)火之后發(fā)生的狀態(tài)。通過定義弧上的函數(shù)，可以決定托肯值流向不同的庫所。

Σ：有限非空顏色集類型的集合。

V：有限變量的集合，對(duì)所有變量v∈V滿足Type[v]∈Σ。

C：P→Σ是顏色集函數(shù)，它給每一個(gè)位置分配一個(gè)顏色集合。

G：T→EXPRV是弧表達(dá)式函數(shù)，它為每一個(gè)弧分配一個(gè)表達(dá)式。

I：P→EXPRφ是初始化函數(shù)，庫所通常需要被賦予一個(gè)初始化表達(dá)式。

定義2層次化CPN模型HCPN是四元組HCPN=(S，SM，PS，F(xiàn)S)[10]，其中：

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

SM：Tsub→S是子模塊函數(shù)，用關(guān)聯(lián)替代變遷和對(duì)應(yīng)的CP-nets子模塊。

PS：用于定義端口關(guān)聯(lián)關(guān)系，?t∈Tsub，PS(t)?其中Psock(t)為替代變遷所在模塊的端口庫所為與替代變遷關(guān)聯(lián)的CP-nets模塊所對(duì)應(yīng)的庫所，并且對(duì)所有的(p，p")∈PS(t)和所有的t∈Tsub，等式PT(p)=PT(p")，C(p)=C(p")，I(p)＜＞=Ia(p")＜＞都成立。

FS：FS?2P是庫所融合集，對(duì)所用的p，p"∈fs，所有fs∈FS，等 式C(p)=C(p")，I(p)＜＞=Ia(p")＜＞成立。一個(gè)庫所融合集中的所有庫所實(shí)質(zhì)上為同一個(gè)庫所。

2.2 CPN Tools屬性特征

CPN Tools是由奧爾胡斯大學(xué)團(tuán)隊(duì)研發(fā)的一款系統(tǒng)建模分析工具[11]，在CPN Tools工具中，模型描述語言由Petri網(wǎng)圖和編程語言CPN ML構(gòu)成，提供良好的用戶界面(GUI)，具有增量語法檢查和代碼生成功能。不必關(guān)心協(xié)議具體實(shí)現(xiàn)的細(xì)節(jié)問題[12]?？梢赃M(jìn)行單步執(zhí)行或連續(xù)執(zhí)行，用戶可以利用CPN Tools對(duì)模型的各個(gè)部分進(jìn)行測(cè)試，保證模型的正確性?？梢蕴幚砦炊〞r(shí)和定時(shí)的網(wǎng)絡(luò)，創(chuàng)建層次的CPN的可達(dá)圖，計(jì)算狀態(tài)空間并生成狀態(tài)空間報(bào)告，狀態(tài)空間報(bào)告可用于分析模型的靜態(tài)和動(dòng)態(tài)特性，標(biāo)準(zhǔn)狀態(tài)空間報(bào)告包含注入邊界和活性屬性等信息，具有回饋機(jī)制可以將錯(cuò)誤進(jìn)行定位，這給分析協(xié)議系統(tǒng)模型提供很大幫助。表2是CPN Tools支持定義的數(shù)據(jù)類型的顏色集。

表2 CPN Tools定義的顏色集類型

基于CPN模型檢測(cè)方法對(duì)協(xié)議安全性能的分析主要包括以下基礎(chǔ)屬性：活性、可達(dá)性、有界性、完整性、認(rèn)證性、機(jī)密性、可恢復(fù)性等。其中協(xié)議活性用來描述協(xié)議逾期事件的發(fā)生，可達(dá)性用來描述預(yù)定的協(xié)議狀態(tài)會(huì)發(fā)生。協(xié)議能夠按照期望的行為方式運(yùn)行，安全屬性在攻擊者模型中特指協(xié)議不存在與預(yù)期狀態(tài)相悖的行為。非預(yù)期狀態(tài)通常會(huì)導(dǎo)致模型出現(xiàn)死鎖，有界性通常用來判斷特定狀態(tài)下消息庫所的容量上下限?？苫謴?fù)性可以表明協(xié)議模型在出現(xiàn)錯(cuò)誤后能否在有限時(shí)間內(nèi)返回到預(yù)期狀態(tài)并進(jìn)入正常序列。

3 基于HCPN模型的TLS1.3握手協(xié)議建模

3.1 TLS1.3預(yù)主密鑰和身份認(rèn)證

TLS1.3協(xié)議規(guī)范中制定了協(xié)議的降級(jí)保護(hù)[13]，通過增加確定的擴(kuò)展結(jié)構(gòu)，保持與之前版本的兼容性，避免未升級(jí)的通信服務(wù)端和中間件因?yàn)椴荒芙忉尪芙^響應(yīng)服務(wù)，這使得新的功能被移值到擴(kuò)展結(jié)構(gòu)中。如果含有擴(kuò)展字段support_version則表示采用TLS1.3連接方式[3]。LTS1.3握手協(xié)議密鑰的建立是通過多個(gè)輸入密鑰結(jié)合創(chuàng)建實(shí)際工作的密鑰材料實(shí)現(xiàn)的[14]。所以可以將復(fù)雜的密鑰算法抽象成特定的函數(shù)替換。為了簡(jiǎn)化整個(gè)握手的過程，將不參加密鑰建立和認(rèn)證的參數(shù)不計(jì)入形式化分析過程，根據(jù)圖1分析的握手協(xié)議順序圖可以得到TLS1.3握手協(xié)議形式化描述過程如下：

(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，F(xiàn)inished)

(6)Server→Client：(Cerficate，CerficateVerify，F(xiàn)inished)

身份認(rèn)證過程和預(yù)主密鑰計(jì)算過程指定私鑰PR使用函數(shù)Sign對(duì)消息簽名，公鑰PU使用函數(shù)Versign驗(yàn)證簽名，公鑰PU使用函數(shù)Anec對(duì)消息加密，私鑰PR使用函數(shù)Adec對(duì)消息解密?？蛻舳税l(fā)送的ClientHello消息和服務(wù)端發(fā)送的ServerHello消息都是明文傳輸。之后從服務(wù)端發(fā)送的消息都開始加密傳輸。服務(wù)端在發(fā)送Pre_Shared_Key時(shí)使用非對(duì)稱算法加密：

EncryptedEx=Anec(Pre_Shared_Key，PU(k_rsa))

客戶端接收到該消息之后對(duì)其解密獲取預(yù)主密鑰：

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

之后進(jìn)行客戶端對(duì)服務(wù)端的身份認(rèn)證，服務(wù)端發(fā)送加密的身份信息：

SignedCerficateS=Sign(ServerCerficate，PR(Signkey))

客戶端接收到之后對(duì)其進(jìn)行解密：

ServerCerficate=Versign(SignedCerficate，PU(Signkey))

根據(jù)解密得到的證書信息查詢證書鏈，認(rèn)證服務(wù)端的身份信息。同時(shí)客戶端發(fā)送加密的身份信息：

SignedCerficateC=Sign(ClientCerficate，PR(Signkey))

服務(wù)端接收到之后對(duì)其進(jìn)行解密：

ServerCerficate=Versign(SignedCerficateC，PU(Signkey))

根據(jù)解密得到的證書信息查詢證書鏈，驗(yàn)證客戶端身份信息。建模主要目的是驗(yàn)證協(xié)議設(shè)計(jì)是否違背安全屬性，所以在模型中不再考慮網(wǎng)絡(luò)數(shù)據(jù)丟失情況。

3.2 模型使用的顏色和變量定義

CPN Tools中有多重?cái)?shù)據(jù)類型的定義，如Integer、String、Unit、Product(不同類型的叉積)、union(不同類型的中的一種)，records、list等[11]，根據(jù)協(xié)議規(guī)范文檔TLS1.3(RFC 8446)的定義，對(duì)其模型抽象簡(jiǎn)化，TLS握手協(xié)議中客戶端和服務(wù)端之間密鑰傳輸過程中使用的參數(shù)字段對(duì)應(yīng)表見表3。

表3 協(xié)議參數(shù)字段含義

根據(jù)CPN ML語言，定義模型中要使用的數(shù)據(jù)類型的顏色集，因?yàn)門LS1.3協(xié)議復(fù)雜性，定義的顏色集較多，這里只列舉部分重要的相關(guān)顏色集定義。對(duì)明文傳輸?shù)腃lientHello和ServerHello消息使用乘積(product)類型顏色集定義，而對(duì)于后續(xù)加密的消息則使用記錄(record)類型顏色集定義。為了避免CPN模型狀態(tài)空間爆炸問題，限定了隨機(jī)數(shù)ClientRandom和ServerRandom的范圍為4～6，同時(shí)定義了客戶端支持的協(xié)議版本ProtocolVersion_c的托肯值為2和3，表示支持的協(xié)議版本TLS1.3或者TLS1.2。而服務(wù)端只提供ProtocolVersion_s的托肯值為3的一種情況，表示服務(wù)端默認(rèn)選擇TLS1.3。定義的顏色集和變量如表4所示。

表4 模型數(shù)據(jù)類型顏色值定義

根據(jù)協(xié)議中存在的函數(shù)加密解密過程，定義客戶端和服務(wù)端分別持有的公鑰和私鑰。使用ML形式化描述語言抽象成下面的的函數(shù)。

(fun DecryptionKey(k：PublicKey)

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

3.3 TLS1.3協(xié) 議 的HCPN建 模

按照TLS1.3握手協(xié)議密鑰協(xié)商形式化描述過程，協(xié)議發(fā)起者Client和響應(yīng)者Server按照協(xié)議規(guī)范RFC 8846執(zhí)行，CPN模型主要描述TLS1.3握手協(xié)議版本的選擇和預(yù)主密鑰Pre_Shared_key傳輸以及雙雙身份認(rèn)證過程。實(shí)驗(yàn)的主要目的是驗(yàn)證預(yù)主密鑰和身份認(rèn)證的安全性。

使用CPN Tools對(duì)TLS1.3握手協(xié)議建模，同時(shí)添加Dolev-Yao攻擊者模型，驗(yàn)證協(xié)議設(shè)計(jì)是否存在安全隱患?；贖CPN的TLS1.3握手協(xié)議模型分為頂層模型TLS，實(shí)體層模型Client、Server和Network。頂層模型TLS描述TLS1.3協(xié)議的總體概況，頂層模型包括協(xié)議實(shí)體Client和Server以及Network三個(gè)節(jié)點(diǎn)。之后采用HCPN層次化建模方法為每個(gè)實(shí)體節(jié)點(diǎn)創(chuàng)建一個(gè)替代變遷，對(duì)頂層模型中的每個(gè)替代變遷細(xì)化描述。TLS1.3原始模型建好之后，得到狀態(tài)空間報(bào)告，之后在此模型基礎(chǔ)上添加Dolev-Yao攻擊者模型，該攻擊者模型能夠獲取協(xié)議實(shí)體(Client?Server)節(jié)點(diǎn)之間的所有通信數(shù)據(jù)。

圖2所示為TLS1.3握手協(xié)議的頂層模型，圖3是節(jié)點(diǎn)Server的實(shí)體層模型。圖2中的每個(gè)替代變遷對(duì)應(yīng)實(shí)體層的一個(gè)子頁，替代變遷Client對(duì)客戶端實(shí)體層模型，替代變遷Server對(duì)應(yīng)圖4服務(wù)端實(shí)體層模型，替代變遷Network對(duì)應(yīng)于網(wǎng)絡(luò)層實(shí)體模型。

圖2 TLS1.3握手協(xié)議的頂層模型

圖3 節(jié)點(diǎn)Sever端實(shí)體層模型

Client實(shí)體層模型中客戶端首先發(fā)送密鑰交換材料，定義變遷clientrandom表示隨機(jī)數(shù)，限定了隨機(jī) 數(shù) 的 范 圍 為4～6。定 義 變 遷protocolversionC表 示客戶端支持的協(xié)議版本，用整數(shù)2和3表示TLS協(xié)議版本TLS1.2和TLS1.3?？蛻舳税l(fā)送ClientHello消息之后，服務(wù)端接收該消息，并選擇自己支持的協(xié)議版本TLS1.3和相關(guān)的密鑰材料。之后響應(yīng)客戶端ServerHello消息。

Server實(shí)體層模型反映服務(wù)端的實(shí)現(xiàn)細(xì)節(jié)，從客戶端接收密鑰材料，并根據(jù)自己支持的協(xié)議版本和密鑰套件來選擇建立主秘鑰使用的協(xié)議版本和相關(guān)算法。使用布爾(bool)類型判斷雙方之間協(xié)商的協(xié)議版本是否為TLS1.3，如果為真，則繼續(xù)后續(xù)的會(huì)話過程。為之后完成預(yù)主密鑰傳輸和雙方身份認(rèn)證建立基礎(chǔ)。

所有的會(huì)話過程都要經(jīng)過網(wǎng)絡(luò)層傳輸才能被接收，這里只分析協(xié)議本身設(shè)計(jì)上的安全性，不考慮網(wǎng)絡(luò)重傳或者數(shù)據(jù)丟失等問題。而攻擊者也是在網(wǎng)絡(luò)層中截獲和存儲(chǔ)信息。

圖4是服務(wù)端實(shí)體層模型，表達(dá)客戶端和服務(wù)端協(xié)商協(xié)議版本TLS1.3成功，當(dāng)客戶端提供的協(xié)議版本和服務(wù)端支持的協(xié)議版本相同時(shí)通過變遷邏輯判斷輸出“true”，繼續(xù)執(zhí)行模型后續(xù)協(xié)議會(huì)話過程。

圖4 服務(wù)端選擇TLS協(xié)議版本

圖5是服務(wù)端預(yù)主密Pre_Shared_Key加密傳輸完成之后，客戶端解密獲得預(yù)主密鑰，服務(wù)端加密發(fā)送服務(wù)端證書，客戶端解密獲得證書后查詢證書鏈驗(yàn)證服務(wù)端的身份信息。

圖5 客戶端對(duì)服務(wù)端的身份認(rèn)證

客戶端對(duì)服務(wù)端身份認(rèn)證完成之后，客戶端加密發(fā)送自己的證書信息，服務(wù)端接收到信息之后解密獲得客戶端證書，通過查詢證書鏈據(jù)此驗(yàn)證客戶端身份信息。

圖6是協(xié)議執(zhí)行的最終狀態(tài)，客戶端完成對(duì)服務(wù)端身份信息的認(rèn)證，同時(shí)服務(wù)端也完成對(duì)客戶端身份信息的認(rèn)證。模擬執(zhí)行結(jié)束。在這基礎(chǔ)上添加攻擊者模型，驗(yàn)證密鑰和身份認(rèn)證的安全屬性。

圖6 頂層模型最終狀態(tài)

3.4 TLS1.3添加DY敵手模型

Dolev-Yao[6]攻擊模型被認(rèn)為不具有攻破密碼算法的能力，在沒有私鑰的情況下沒有辦法獲知加密消息的內(nèi)容。在此前提下Dolev-Yao模型規(guī)定攻擊者具有可以不被協(xié)議主體察覺的情況下掌握整個(gè)通信網(wǎng)絡(luò)的情況，并攔截和存儲(chǔ)網(wǎng)絡(luò)中的通信消息，同時(shí)攻擊者可以偽造消息，之后以合法協(xié)議參與者的身份發(fā)送消息。整個(gè)協(xié)議的執(zhí)行過程都暴露在攻擊者的監(jiān)視之下。基于此攻擊者采用union類型表示攻擊者擁有的數(shù)據(jù)類型，包括雙方之間明文傳輸?shù)碾S機(jī)數(shù)、協(xié)議版本號(hào)、密鑰套件以及加密傳輸?shù)乃性有畔?。敵手攻擊模型中敵手根?jù)從網(wǎng)絡(luò)中俘獲的參數(shù)來重組消息，構(gòu)造更強(qiáng)的攻擊能力，以協(xié)議參與者的身份發(fā)送消息，達(dá)到竊取網(wǎng)絡(luò)終端信息的目的。圖7和圖8是攻擊者模型。攻擊者通過構(gòu)造信息之后發(fā)送給接收者。

圖7 預(yù)主密鑰傳輸攻擊者模型

圖8 身份認(rèn)證攻擊模型

因?yàn)榉?wù)端在傳輸預(yù)主密鑰的時(shí)候使用了持有的私鑰PR加密，之后將加密的密文和簽名算法作為明文信息再次使用公鑰Aenc加密。攻擊者只能解密獲得被加密的Pre_Shared_Key，之后使用自己的公鑰對(duì)其再次加密之后偽裝成服務(wù)端發(fā)送給客戶端，并不能獲得預(yù)主秘鑰的信息。這樣客戶端將無法解密加密的預(yù)主密鑰，中斷傳輸。

客戶端和服務(wù)端之間的身份認(rèn)證方式是相同的，證書發(fā)送之前使用對(duì)應(yīng)的的私鑰加密，之后對(duì)加密信息再使用公鑰加密，對(duì)應(yīng)的接收端解密獲得證書信息之后查詢證書鏈，驗(yàn)證證書信息是否合法，據(jù)此判斷雙方的身份信息。Dolev-Yao攻擊模型攻擊者截獲加密的證書信息之后，因?yàn)椴痪邆潆p方私鑰能力無法解密證書信息，加密后再次發(fā)送給接收者，接收者在接收到信息之后無法解密出證書信息。會(huì)話建立不成功。

4 協(xié)議安全性分析

基于HCPN模型的TLS1.3握手協(xié)議建模完成之后，分析了TLS1.3握手協(xié)議模型中預(yù)主密鑰Pre_Shared_Key和雙方身份認(rèn)證的安全性，之后在該模型中加入攻擊者模型，通過形式化驗(yàn)證協(xié)議模型是否違背TLS握手協(xié)議規(guī)范的安全屬性。本文不考慮攻擊者作為會(huì)話發(fā)起者的情況，只考慮攻擊者作為協(xié)議會(huì)話的截獲者重放消息或者偽裝成其他實(shí)體發(fā)送消息，并且協(xié)議模型只考慮協(xié)議運(yùn)行的單次會(huì)話的執(zhí)行情況。

下面是CPN Tools生成的TLS1.3握手協(xié)議原模型的狀態(tài)空間報(bào)告和基于Dolev-Yao攻擊模型生成的狀態(tài)空間報(bào)告。基于篇幅原因，這里只分析對(duì)應(yīng)報(bào)告中重要的三種數(shù)據(jù)：統(tǒng)計(jì)數(shù)字分析、有界性分析和活性分析。

(1)TLS1.3握手協(xié)議原模型狀態(tài)空間報(bào)告

表6列舉了CPN Tools仿真得到的狀態(tài)統(tǒng)計(jì)信息，其中State Spcae表示狀態(tài)空間的節(jié)點(diǎn)和連接弧的個(gè)數(shù)，在該CPN模型中，節(jié)點(diǎn)數(shù)為2 194，連接弧為5 073，構(gòu)造該狀態(tài)空間過程在計(jì)算機(jī)上花費(fèi)9 s，Scc Graph為強(qiáng)連接圖，這與狀態(tài)空間的節(jié)點(diǎn)數(shù)和連接弧個(gè)數(shù)相等，說明協(xié)議模型中的數(shù)據(jù)不需要重傳。為了方便研究協(xié)議安全性，在設(shè)計(jì)之初不考慮網(wǎng)絡(luò)重傳問題。

表6 統(tǒng)計(jì)數(shù)字分析

表7是每個(gè)庫所對(duì)應(yīng)的托肯的數(shù)量區(qū)間，庫所Client"clientrandom最多有3個(gè)托肯，最少托肯值為2，庫所Client protocolversionC的托肯的上界是2，下界是0；Server"psk1的托肯上界是1，下屆也是1。從這些庫所的結(jié)果中可以看出該模型中的庫所符合實(shí)際要求。

表7 有界性分析

表8是模型的活性分析表。其中Dead Markings指的是死標(biāo)識(shí)狀態(tài)，在該標(biāo)識(shí)下任何變遷都是非使能的。Dead Transition指的是死變遷，即該變遷在模型中的任何發(fā)生序列中都無法發(fā)生，一般情況下死變遷的出現(xiàn)預(yù)示著模型的設(shè)計(jì)不合理，可以去掉死變遷而不影響模型的動(dòng)態(tài)執(zhí)行。本實(shí)驗(yàn)輸出的結(jié)果顯示不存在死變遷。Live Transition是活變遷，即在任何可達(dá)標(biāo)識(shí)下，該變遷都在一個(gè)可發(fā)生序列中，輸出結(jié)果顯示本實(shí)驗(yàn)?zāi)Ｐ椭胁淮嬖诨钭冞w，因?yàn)樵撃Ｐ痛嬖谒罉?biāo)識(shí)狀態(tài)，所以在該標(biāo)識(shí)下任何變遷都是不能發(fā)生的。也就是在該模型中數(shù)據(jù)傳輸完成的一種狀態(tài)。

表8 狀態(tài)空間報(bào)告—活性分析

(2)基于Dolev-Yao攻模型的狀態(tài)空間報(bào)告

添加Dolev-Yao攻擊模型后輸出的狀態(tài)空間屬性報(bào)告如表9、表10所示。從表中可見不存在死變遷，說明設(shè)計(jì)符合安全性。

表9 有界性分析

表10 活性分析

5 結(jié)論

本文詳細(xì)分析TLS1.3握手協(xié)議過程，歸納了TLS1.3握手協(xié)議內(nèi)容上改進(jìn)的措施，使用CPN Tools建模工具層次化建模了TLS1.3握手協(xié)議中版本選擇以及預(yù)主密鑰傳輸和雙方身份認(rèn)證過程，并計(jì)算模型生成狀態(tài)空間報(bào)告，之后在此模型上添加了Dolev-Yao攻擊模型對(duì)TLS1.3握手協(xié)議預(yù)主密鑰傳輸和身份認(rèn)證過程進(jìn)行了安全性分析。最后通過狀態(tài)空間報(bào)告分析驗(yàn)證了TLS1.3握手協(xié)議預(yù)主密鑰和身份認(rèn)證安全性符合協(xié)議設(shè)計(jì)規(guī)范的要求的安全屬性。不足之處是本文使用的攻擊模型不是強(qiáng)安全攻擊模型，在后續(xù)研究中將使用攻擊能力更強(qiáng)的攻擊模型。