TLS1.3&TLS1.2形式化分析

本博客是對下面博客鏈接上的原文進行梳理+本身在其餘方面資料作個整理

https://blog.csdn.net/andylau00j/article/details/79269499

https://www.cnblogs.com/huanxiyun/articles/6554085.html

   TLS協議在網絡的應用層提供功能 ：加密，認證、消息完整性。（創建一個安全的鏈接，對其中傳輸的數據加密保護，防止中間人嗅探明文；多對數據的完整性進行校驗，防止傳輸的數據被中間人進行篡改，創建一個可信的鏈接，對雙方的真實身份進行驗證）

        

  一個正常的TLS1.3 握手順序是按照下面的順序進行：

• 客戶端發送Client Hello（CH）報文，包含有關密鑰協商以及其餘與TLS鏈接創建有關的擴展給服務端。
• 服務端發送Server Hello（SH）報文，包含有關密鑰協商的擴展返還給客戶端，雙方根據CH和SH的協商結果能夠得出密鑰材料。
• 若是客戶端發送的CH報文不知足服務端的須要（如：不包含服務端支持的DH組件），服務端會發送一個Hello Retry Request報文給客戶端，要求客戶端從新發送符合要求的CH報文。
• 利用密鑰材料和前兩個報文的哈希值，使用HKDF能夠計算出一個handshake_key，此後握手階段的信息受該密鑰保護。
• 服務端發送Encypted Extension（EE）報文，包含其餘與密鑰協商無關的擴展數據給客戶端。
• 若是使用公鑰證書進行身份認證，服務端發送Certificate報文（傳遞本身的證書信息），和Certificate Verify(CV)報文（使用本身的證書私鑰對以前的報文進行HMAC簽名證實本身持有該證書）給客戶端。
• 若是須要對客戶端身份進行認證，服務端還須要發送Certificate Request（CR）報文給對方請求客戶端發送證書。
• 服務端發送Finished報文。代表服務端到客戶端信道的握手階段結束，理論上不得再由該信道發送任何握手報文。
• 若是客戶端收到了服務端的CR報文，返回本身的Certificate報文和CV報文。
• 客戶端發送Finished報文，代表握手階段結束，能夠正式開始會話通信。Finished報文使用會話密鑰對上述全部握手信息進行HMAC簽名，校驗簽名能夠檢驗握手階段的完整性，也能夠驗證雙方是否協商出了一致的密鑰。

TLS1.3最大的特色就是對不一樣的報文使用多種不一樣的祕鑰，TLS1.2中只使用兩種祕鑰，一個事用於完整性校驗，另外一個是用於報文加密，同一個鏈接中不一樣方向的加密祕鑰不同，TLS1.3使用AEAD機制再也不使用MAC_key來進行完整性校驗，同時因爲其餘各類用途的加密須要，TLS1.3的實施過程使用一下幾種key：

    handshake_key     early_traffic_key   resumption_key     exporter_key（導出祕鑰，用戶自定義的其餘用途）

  這些祕鑰都是由以前協商的祕鑰材料計算而出，區別在於HKDF的計算次數不一樣，HKDF計算使用的哈希值不一樣，以會話祕鑰application_key爲例子，以整個握手階段的報文做爲輸入，計算四次HKDF導出最終使用的祕鑰，同時，當加密的報文長度達到必定的長度的時候，雙方發送的KU報文從新計算application_key

數據發送出去以後，recod層會在密報文頭部加上一小段的明文信息來標識解密後明文的長度信息，對方的讓recod 層收到消息以後，經過逆過程解密密文後轉發給上層協議，

同時TLS1.3協議版本容許在末尾添加八字節整數倍的全爲0的二進制數據，對方收到該消息以後，解密從末尾開始去掉0 ，當搜索到第一個不全爲0的八字節的時候結束。

總的歸納：  TLS1.3協議版本 使用的更加 複雜額祕鑰導出過程，加強了最終使用祕鑰的安全性，同時簡化了所使用的加密祕鑰，刪除了RC4  3DES   SHA1  AES-CBC 等加密算法，刪除了加密前壓縮，從新協商等具備的漏洞，精簡了協議 內容，

    在TLS1.2中記錄協議record，佔據一個TLS鏈接的絕大數的數據流量，

Record 協議 — 從應用層接受數據，而且作:

分片，逆向是重組
生成序列號，爲每一個數據塊生成惟一編號，防止被重放或被重排序
壓縮，可選步驟，使用握手協議協商出的壓縮算法作壓縮
加密，使用握手協議協商出來的key作加密/解密
算HMAC，對數據計算HMAC，而且驗證收到的數據包的HMAC正確性
發給tcp/ip，把數據發送給 TCP/IP 作傳輸(或其它ipc機制)。

 下面對TLS協議祕鑰協商的過程的分析 

基於RSA握手和祕鑰交換的客戶端驗證服務器爲示例以下

 

下面是上網的握手過程的時序圖

下面對上面的協商過程解釋：

 （1）Client-Hello   客戶端發送請求，以明文傳輸信息，包含版本信息，加密候選列表，候選算法列表，隨機數，擴展字段等信息，

        客戶端支持加密套件 cipher suite列表，注意，每個加密條件對應前面TLS原理中的四個功能的組合，認證算法Au（身份驗證），祕鑰交換算法 （keyExchange 祕鑰協商），對稱加密算法Enc(信息加密)，信息摘要MAc（完整性驗證）。在TLS1.2 中支持壓縮算法，Client-Hello 中包含壓縮算法列表，用於後後續的壓縮階段使用。另外還有隨機數 randmo_c 用於後續祕鑰的生成。最後還包括擴展字段 extension 支持協議相關算法的參數以及其餘輔助信息。

（2）Server-Hello +Server_cerficate+ server_hello_done

    server_hello 服務端返回協商的信息結果，包括使用的協議版本，選擇的加密套件，以及使用的壓縮算法 隨機數（隨機數用於後續的祕鑰協商）

    server_certificate 服務器端配置對應的證書鏈，用於身份驗證和祕鑰交換

    server_Hellodone 通知客戶端 server_hello 信息發送結束

（3）證書校驗

     客戶端證書的合法性，若是驗證經過纔會進行後續的通訊，合法性驗證主要包括下面的環節：

       證書鏈的可信任、證書是否吊銷、證書是否在有效期內、域名，覈實證書的域名是不是當前訪問的域名相匹配。

（4）Client_key_excahage+ change_chiper_spec+encrypted_handshake_message

       client_key_exchage 合法性驗證經過以後，客戶端計算產生隨機數 pre-master ,並用證書的Pk 加密發送給服務器。

      當客戶端獲取所有的計算協商祕鑰須要的信息： 兩個明文隨機數 Radmon_c 和 Radmon-S 和本身計算產生的 pre-master 計算獲得協商祕鑰

      enc_key=fuc(randmo_C,randmo_s,pre-Master)

      change_chiper_spec,客戶端通知服務器後續的通訊都採用協商的通訊加密祕鑰和加密算法進行加密通訊，

      encrypted_handshake_message 結合前面全部的通訊參數的hash值和其相關的信生成一段數據，採用協商的 session-secret 與算法進行加密以後發送給服務器用於數據與握手驗證

 5）Change_ciper_spec +encrypted_handshake_message

       服務器使用私鑰解密加密的per-master 數據，基於以前交換的兩個明文隨機書卷 Random_c 和 random_S 計算協商祕鑰 enc_key=fuc(randmo_C,randmo_s,pre-Master)

      計算以前所接受信息的hash 值，而後解密客戶端發送 encrypted_handshake_message 驗證數據和祕鑰的正確性

      encrypted_handshake_message驗證完以後，服務器結一樣發送 change_cipher_spec以告知客戶端後續的通訊採用協商祕鑰與算法加密通訊

      encrypted_handshake_message服務器結合當前全部的通訊參數生成一段數據並採用協商祕鑰 session secret 與算法加密併發到客戶端

（6）結束握手

      客戶端計算全部接受到的信息的hash值，並採用協商祕鑰解密 encrypted_handshake_message 驗證服務器發送的數據和祕鑰，驗證經過則完成握手。

（7）加密通訊

   開始使用協商祕鑰與算法進行加密通訊

對TLS協議進行形式化分析的思惟導圖

 下面是對 論文形式化工具Scyther 優化實例分析的關於 TSL的整理

   做者對TLS的形式化過程當中的涉及到如何將角色模型轉化成安全模型的並無說明，  只是將TSL.spdl執行的結果 截圖，而後說明TLS是存在安全隱患的，分別在強安全模型和DY模型下面進行了低手的攻擊測試

  另外，  做者對攻擊的軌跡路徑沒有說明。對存在的多種的軌跡路徑只是截了一張圖來簡單的說明 確實存在安全的問題

 

Client Hello

握手第一步是客戶端向服務端發送 Client Hello 消息，這個消息裏包含了一個客戶端生成的隨機數 Random一、客戶端支持的加密套件（Support Ciphers）和 SSL Version 等信息。經過 Wireshark 抓包，咱們能夠看到以下信息：

Wireshark 抓包的用法能夠參考這篇文章

Server Hello

第二步是服務端向客戶端發送 Server Hello 消息，這個消息會從 Client Hello 傳過來的 Support Ciphers 裏肯定一份加密套件，這個套件決定了後續加密和生成摘要時具體使用哪些算法，另外還會生成一份隨機數 Random2。注意，至此客戶端和服務端都擁有了兩個隨機數（Random1+ Random2），這兩個隨機數會在後續生成對稱祕鑰時用到。

Certificate

這一步是服務端將本身的證書下發給客戶端，讓客戶端驗證本身的身份，客戶端驗證經過後取出證書中的公鑰。

Server Key Exchange

若是是DH算法，這裏發送服務器使用的DH參數。RSA算法不須要這一步。

Certificate Request

Certificate Request 是服務端要求客戶端上報證書，這一步是可選的，對於安全性要求高的場景會用到。

Server Hello Done

Server Hello Done 通知客戶端 Server Hello 過程結束。

Certificate Verify

客戶端收到服務端傳來的證書後，先從 CA 驗證該證書的合法性，驗證經過後取出證書中的服務端公鑰，再生成一個隨機數 Random3，再用服務端公鑰非對稱加密 Random3生成 PreMaster Key。

Client Key Exchange

上面客戶端根據服務器傳來的公鑰生成了 PreMaster Key，Client Key Exchange 就是將這個 key 傳給服務端，服務端再用本身的私鑰解出這個 PreMaster Key 獲得客戶端生成的 Random3。至此，客戶端和服務端都擁有 Random1 + Random2 + Random3，兩邊再根據一樣的算法就能夠生成一份祕鑰，握手結束後的應用層數據都是使用這個祕鑰進行對稱加密。爲何要使用三個隨機數呢？這是由於 SSL/TLS 握手過程的數據都是明文傳輸的，而且多個隨機數種子來生成祕鑰不容易被暴力破解出來。客戶端將 PreMaster Key 傳給服務端的過程以下圖所示：

Change Cipher Spec(Client)

這一步是客戶端通知服務端後面再發送的消息都會使用前面協商出來的祕鑰加密了，是一條事件消息。

Encrypted Handshake Message(Client)

這一步對應的是 Client Finish 消息，客戶端將前面的握手消息生成摘要再用協商好的祕鑰加密，這是客戶端發出的第一條加密消息。服務端接收後會用祕鑰解密，能解出來講明前面協商出來的祕鑰是一致的。

Change Cipher Spec(Server)

這一步是服務端通知客戶端後面再發送的消息都會使用加密，也是一條事件消息。

Encrypted Handshake Message(Server)

這一步對應的是 Server Finish 消息，服務端也會將握手過程的消息生成摘要再用祕鑰加密，這是服務端發出的第一條加密消息。客戶端接收後會用祕鑰解密，能解出來講明協商的祕鑰是一致的。

Application Data

到這裏，雙方已安全地協商出了同一份祕鑰，全部的應用層數據都會用這個祕鑰加密後再經過 TCP 進行可靠傳輸。

雙向驗證

前面提到 Certificate Request 是可選的，下面這張圖展現了雙向驗證的過程：

握手過程優化

若是每次重連都要從新握手仍是比較耗時的，因此能夠對握手過程進行優化。從下圖裏咱們看到 Client Hello 消息裏還附帶了上一次的 Session ID，服務端接收到這個 Session ID 後若是能複用就再也不進行後續的握手過程。

除了上述的 Session 複用，SSL/TLS 握手還有一些優化技術，例如 False Start、Session Ticket 等

參考文獻：

[1] File O P. Network Infrastructure for Ethernet/IP: Introduction and Considerations[J]. ODVA Publication PUB00035R0, 2007.  
[2]EtherNet/IP:Industrial Protocol White Paper   Institute of Electrical and Electronic Engineers,
[3] File O P. Securing EtherNet/IPTM Networks: Introduction and Considerations[J]. ODVA Publication PUB00269R1.1, 2011.
[4] File O P. Common Industrial protocol CIPTM and the family of CIP networks: Introduction and Considerations[J]. ODVA Publication PUB00123R1,2016(引用的部分是隱士和顯示傳輸的兩種方式)
[5]Jack Visoky, Joakim Wiberg, Nancy Cam-Winget. Presented at the ODVA 2018 Industry Conference & 18th Annual Meeting October 10, 2018 Stone Mountain, Georgia, USA.   TLS `1.3對CIP的影響
[6]Brian Batke, Joakim Wiberg&Dennis Dube.CIP Security Phase1 Secure Transport for EtherNet/IP.Presented at the ODVA 2015 Industry Conference&17th Annual Meeting  ---TLS和DLTS安全性能的介紹
[7] A. Ginter, 「The Top 20 Cyber Attacks Against Industrial Control Systems,」  https://ics-cert.us-cert.gov/sites/default/files/ICSJWGArchive/ QNL DEC 17/Waterfall top-20-attacks-article-d2%20- %20Article S508NC.pdf.   [8] 馮濤,魯曄,方君麗.工業以太網協議脆弱性與安全防禦技術綜述[J]. 通訊學報, 2017(S2). [9]Ryan Grandgenett ,Robin Gandhi,William Mahoney. Exploitation of Allen Bradley's implementation  of etherNet/IP for denial of service against industrial control systems  -----漏洞 [10]Sheffer Y, Holz R, Saint-Andre P. Summarizing known attacks on transport layer security (TLS) and datagram TLS (DTLS)[R]. 2015.  [11]Sheffer Y, Holz R, Saint-Andre P. Recommendations for Secure Use of Transport Layer Security (TLS) and Datagram Transport Layer Security (DTLS)[R]. 2015.  [12]Rescorla E. The transport layer security (TLS) protocol version 1.3[R]. 2018.  [13] Song D X . Athena: a New Efficient Automatic Checker for Security Protocol Analysis[C]// IEEE Workshop on Computer Security Foundations. IEEE Computer Society, 1999. ------  算法 [14] Cremers C J F , Mauw S . Operational Semantics of Security Protocols[C]// International Conference on Scenarios: Models. Springer-Verlag, 2005.   ------Spdl 語言 [15]韓旭，陸思奇&程慶豐.形式化工具Scyther優化與實例分析 [16]陸思奇，程慶豐&趙進華.安全協議形式化分析工具比較研究 [17]魏成坤, 劉向東, 石兆軍. OAuth2.0協議的安全性形式化分析[J]. 計算機工程與設計, 2016, 37(7):1746-1751. [18] Cremers C .Scyther User manual [19] MEMBER, IEEE, Dolev D , et al. On the Security of Public Key Protocols[J]. IEEE Transactions on Information Theory, 2003, 29(2):198-208.   --------Dolev -Yao模型 [19]Cremers C ,HorvatM , 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). IEEE Computer Society, 2016. [20]Cremers C J F . The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols[C]// Computer Aided Verification, 20th International Conference, CAV 2008, Princeton, NJ, USA, July 7-14, 2008, Proceedings. Springer-Verlag, 2008. -------  介紹了Scyther的功能能夠性能 [21]Krawczyk H , Paterson K G , Wee H . On the Security of the TLS Protocol: A Systematic Analysis[J]. 2013.   [23] Rescorla E, Modadugu N. Datagram transport layer security version 1.2[R]. 2012.