《電子技術(shù)應(yīng)用》
您所在的位置：首頁 > 通信與網(wǎng)絡(luò) > 設(shè)計應(yīng)用 > 基于HCPN模型的TLS1.3協(xié)議安全性分析
基于HCPN模型的TLS1.3協(xié)議安全性分析
網(wǎng)絡(luò)安全與數(shù)據(jù)治理 5期
陳真好1，田學(xué)成2
(1.南京天暢信息技術(shù)有限公司，江蘇 南京211100；2.國電南京自動化股份有限公司，江蘇 南京211100)
摘要： 傳輸層(Transport Layer Security，TLS)協(xié)議是保證網(wǎng)絡(luò)傳輸安全的重要標(biāo)準(zhǔn)協(xié)議，實現(xiàn)了數(shù)據(jù)加密和數(shù)據(jù)完整性以及身份驗證。由于TLS協(xié)議一直存在很多安全漏洞，因此不斷更新。目前最新版本TLS1.3(RFC 8846)已經(jīng)發(fā)布，較之前TLS1.2(RFC 5246)在協(xié)議內(nèi)容上有很大改進(jìn)，提高了安全性和傳輸效率。使用層次著色Petri網(wǎng)(HCPN)的建模方法對TLS1.3握手協(xié)議進(jìn)行建模，同時添加Delov-Yao攻擊模型，并分析了對應(yīng)模型下的狀態(tài)空間報告。實驗結(jié)果表明新發(fā)布的TLS1.3握手協(xié)議預(yù)主密鑰有良好的機密性，并且身份認(rèn)證滿足協(xié)議規(guī)范的安全屬性要求。目前國內(nèi)在協(xié)議形式化分析方法的研究方面很少，本文研究在協(xié)議形式化分析方法上對其他協(xié)議分析具有理論指導(dǎo)意義。
中圖分類號： TN915.08
文獻(xiàn)標(biāo)識碼： A
DOI： 10.19358/j.issn.2097-1788.2022.05.008
引用格式： 陳真好，田學(xué)成. 基于HCPN模型的TLS1.3協(xié)議安全性分析[J].網(wǎng)絡(luò)安全與數(shù)據(jù)治理，2022，41(5)：49-58.
Security analysis of TLS1.3 protocol based on HCPN model
Chen Zhenhao1，Tian Xuecheng2
(1.Nanjing Tianchang Information Technology Co.，Ltd.，Nanjing 211100，China； 2.Guodian Nanjing Automation Co.，Ltd.，Nanjing 211100，China)
Abstract： The Transport Layer Security(TLS) protocol is an important standard protocol for ensuring network transmission security, which realizes data encryption, data integrity, and identity verification. TLS protocol has been updated because there are many security vulnerabilities.Currently, the latest version is TLS1.3(RFC 8846) which has been released. Compared with the previous TLS1.2(RFC 5246), the content of the protocol has been greatly improved, improving security and transmission efficiency. In this paper, a hierarchical colored Petri net(HCPN) modelling method is used to model the TLS1.3 handshake protocol. At the same time, a Delov-Yao attack model is added, and we also analyze the state space report under the corresponding model. Finally,the experimental results show that the newly released pre-master key of the TLS1.3 handshake protocol has good confidentiality, and the identity authentication meets the security attribute requirements of the protocol specification. At present, there are few types of research on formal analysis methods of protocols in China. Therefore,This paper has theoretical guidance significance for other protocol analysis in terms of formal analysis methods of protocols.
Key words : TLS1.3；CPN Tools；TLS1.3 handshake protocol；formal analysis

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ī)范的安全屬性要求。




本文詳細(xì)內(nèi)容請下載：http://theprogrammingfactory.com/resource/share/2000005026




作者信息：

陳真好1，田學(xué)成2

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



微信圖片_20210517164139.jpg

此內(nèi)容為AET網(wǎng)站原創(chuàng)，未經(jīng)授權(quán)禁止轉(zhuǎn)載。