TLS1.3&TLS1.2形式化分析（二）

 一、下面是TLS1.2和TLS1.3握手協議過程 ，明顯的能夠看出存在不一樣 。

 咱們先說TLS1.2的握手過程明顯是比TLS1.3的握手過多了一次。在TLS1.3中捨棄了以前RSA的協商過程，而後基於ECDH算法優化了整個過程，下面說明 ECDH算法的含義：

 固然TLS1.3不光光是優化了者一點，在鏈接恢復過程當中TLS1.3作到了 0-RTT 的過程。   

  在TLS1.2中原有的大量的特性被刪除，包括下面的特性：

     RSA祕鑰傳輸--------不支持向前安全

     RSA密鑰傳輸——不支持前向安全性
     CBC模式密碼——易受BEAST和Lucky 13攻擊
     RC4流密碼——在HTTPS中使用並不安全
     SHA-1哈希函數——建議以SHA-2取而代之
     任意Diffie-Hellman組——CVE-2016-0701漏洞
     輸出密碼——易受FREAK和LogJam攻擊
同時 TLS 1.3版本還存在工做方式的修改：

     新的密碼套件僅在TLS1.3下支持， 一些舊的密碼套件再也不支持。與 TLS1.2相比  TLS1.3加密了更多的握手，減小額握手延遲並採用AEAD 方案，TLS1.3新的握手模式包括初始化的1-RTT （EC）DHE，（預共享祕鑰）PSK模式和PSK-DHE模式。

     新的密碼套件定Tamarin 義方式不一樣，而且沒有詳細規定證書類型（RSA、DSA、ECDSA）或者祕鑰交換機制，（如DHE、或者ECHDE），這對密碼套件的配置會存在影響。在TLS1.3中客戶端提供的key_sahre會對「組」配置產生影響。另外在新的版本中再也不使用DSA證書。

二、做者對TSL1.3的形式化安全分析和證實（使用的是Tamarin  工具）

    根據做者官網上的披露的信息，原做者並無使用 Scyther工具對 TLS1.3作形式化分析，而是使用了Tamarin  這個工具 （功能更增強大，適用於高級分析）能夠自動分析安全協議的工具。

    做者使用的TLS1.3第十版本的協議做爲研究的對象。那me做者的主要貢獻是經過擴展修訂版10的模型合併所需客戶端的延遲機制，發現了一種潛在的攻擊，其中攻擊者可以在PSK回覆握手期間成功的模仿客戶端，做者由此強調了客戶簽名內容中包含更多信息的嚴格的必要性。在以後的發佈的TLS1.3草案中更新了這部分。其中重要的一點就是做者說能夠將10 版本的草案的模型進行擴展到之後的版本模型。這將是長期的。

      Tramarin-proved工具的多字節重寫很是適合用於對TLS1.3協議規範所暗示的複雜轉換系統進行建模，能夠容許分析無線數量的併發的TLS會話的交互。

      做者使用本工具進行分析額時候，首先第一步是構造TLS握手和記錄協議的抽象。而後將其編碼成 Tramarin的規則（也就是使用SPDL語言進行描述形式化協議的一個過程）。規則捕獲忠誠的黨和對手行爲，在合法的客戶端和服務端下，構建的模型規則一般適用於各個消息傳輸相關聯的全部動做，例如咱們的第一個客戶端規則捕獲客戶端生成併發送所必要參數做爲（EC）DHE握手的第一次飛行的一部分，以及在本客戶端中跟蹤，此規則能夠在下面的C_1能夠看見這種機制，該圖表示客戶端在不一樣執行中具備全部選項的並集。（下圖是TLS1.3草案10版本的部分客戶端狀態機制的模型分析）

接下來做者證實TLS1.3（第十版）中聲明的目標和安全屬性

        分析的第二步涉及將所須要的安全屬性編碼爲 Termarin  lemmas.TLS握手協議的目標是容許通訊方的單方或者可選方的相互實體認證，以創建能夠將本身置於鏈接中間的竊聽者和攻擊者不可用的共享祕鑰。TLS記錄協議旨在提供應用程序數據的機密性和完整性，所以，咱們將定義編碼下面屬性做爲引理：

       單方面認證服務器，

       相互認證（可選）

       會話祕鑰和祕鑰的機密性和完善性和完善性的向前保密性。

       握手消息的向前保密性。