陳真好，田學(xué)成

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

0 引言

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

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

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

1.1 密鑰建立方式

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

表1 TLS1.3密碼套件

TLS1.3握手協(xié)議在協(xié)議算法上較之前有很大改變，因為靜態(tài)的RSA算法不提供向前安全(Perfect Forward Secrecy，PFS)[2]，容易被攻擊者竊聽通信消息獲取服務(wù)器私鑰，所以在TLS1.3中被棄用，TLS1.3不再支持密鑰的壓縮算法，同時刪除了很多已存在安全隱患的算法。目前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é)議過程中重點分析了密鑰協(xié)商和身份認(rèn)證的安全屬性。

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

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

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

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

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

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

2.1 著色Petri的定義

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

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

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

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

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

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

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

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

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

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

定義2層次化CPN模型HCPN是四元組HCPN=(S，SM，PS，F(xiàn)S)[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是子模塊函數(shù)，用關(guān)聯(lián)替代變遷和對應(yīng)的CP-nets子模塊。

PS：用于定義端口關(guān)聯(lián)關(guān)系，?t∈Tsub，PS(t)?其中Psock(t)為替代變遷所在模塊的端口庫所為與替代變遷關(guān)聯(lián)的CP-nets模塊所對應(yīng)的庫所，并且對所有的(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")＜＞成立。一個庫所融合集中的所有庫所實質(zhì)上為同一個庫所。

2.2 CPN Tools屬性特征

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

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

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

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

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

TLS1.3協(xié)議規(guī)范中制定了協(xié)議的降級保護(hù)[13]，通過增加確定的擴展結(jié)構(gòu)，保持與之前版本的兼容性，避免未升級的通信服務(wù)端和中間件因為不能解釋而拒絕響應(yīng)服務(wù)，這使得新的功能被移值到擴展結(jié)構(gòu)中。如果含有擴展字段support_version則表示采用TLS1.3連接方式[3]。LTS1.3握手協(xié)議密鑰的建立是通過多個輸入密鑰結(jié)合創(chuàng)建實際工作的密鑰材料實現(xiàn)的[14]。所以可以將復(fù)雜的密鑰算法抽象成特定的函數(shù)替換。為了簡化整個握手的過程，將不參加密鑰建立和認(rèn)證的參數(shù)不計入形式化分析過程，根據(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ù)主密鑰計算過程指定私鑰PR使用函數(shù)Sign對消息簽名，公鑰PU使用函數(shù)Versign驗證簽名，公鑰PU使用函數(shù)Anec對消息加密，私鑰PR使用函數(shù)Adec對消息解密?？蛻舳税l(fā)送的ClientHello消息和服務(wù)端發(fā)送的ServerHello消息都是明文傳輸。之后從服務(wù)端發(fā)送的消息都開始加密傳輸。服務(wù)端在發(fā)送Pre_Shared_Key時使用非對稱算法加密：

EncryptedEx=Anec(Pre_Shared_Key，PU(k_rsa))

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

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

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

SignedCerficateS=Sign(ServerCerficate，PR(Signkey))

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

ServerCerficate=Versign(SignedCerficate，PU(Signkey))

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

SignedCerficateC=Sign(ClientCerficate，PR(Signkey))

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

ServerCerficate=Versign(SignedCerficateC，PU(Signkey))

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

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

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

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

根據(jù)CPN ML語言，定義模型中要使用的數(shù)據(jù)類型的顏色集，因為TLS1.3協(xié)議復(fù)雜性，定義的顏色集較多，這里只列舉部分重要的相關(guān)顏色集定義。對明文傳輸?shù)腃lientHello和ServerHello消息使用乘積(product)類型顏色集定義，而對于后續(xù)加密的消息則使用記錄(record)類型顏色集定義。為了避免CPN模型狀態(tài)空間爆炸問題，限定了隨機數(shù)ClientRandom和ServerRandom的范圍為4～6，同時定義了客戶端支持的協(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)證過程。實驗的主要目的是驗證預(yù)主密鑰和身份認(rèn)證的安全性。

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

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

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

圖3 節(jié)點Sever端實體層模型

Client實體層模型中客戶端首先發(fā)送密鑰交換材料，定義變遷clientrandom表示隨機數(shù)，限定了隨機 數(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實體層模型反映服務(wù)端的實現(xiàn)細(xì)節(jié)，從客戶端接收密鑰材料，并根據(jù)自己支持的協(xié)議版本和密鑰套件來選擇建立主秘鑰使用的協(xié)議版本和相關(guān)算法。使用布爾(bool)類型判斷雙方之間協(xié)商的協(xié)議版本是否為TLS1.3，如果為真，則繼續(xù)后續(xù)的會話過程。為之后完成預(yù)主密鑰傳輸和雙方身份認(rèn)證建立基礎(chǔ)。

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

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

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

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

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

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

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

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

3.4 TLS1.3添加DY敵手模型

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

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

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

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

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

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

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

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

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

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

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

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

表7 有界性分析

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

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

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

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

表9 有界性分析

表10 活性分析

5 結(jié)論

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