TLS1 3 TLS1 2形式化分析(二)

2022-06-10 05:18:06 字數 1996 閱讀 9137

1、下面是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證書。

2、作者對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記錄協議旨在提**用程式資料的機密性和完整性,因此,我們將定義編碼下面屬性作為引理:

單方面認證伺服器,

相互認證(可選)

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

握手訊息的向前保密性。

科普 什麼是TLS1 3

tls1.3是一種新的加密協議,它既能提高各地網際網路使用者的訪問速度,又能增強安全性。我們在訪問許多網頁的時候,常常會在瀏覽器的位址列上看到乙個鎖的圖示,並使用 https 代替傳統的 http 這裡的 s 代表著安全。當你連線到乙個https站點時,你和該站點之間的通訊會被加密,這會顯著提高瀏覽...

使用Wireshark分析TLS1 2

概念掃盲 首先,先說下tls是什麼?tls是ssl協議的具體實現,ssl是乙個規範,tls是安裝ssl規範實現的。後面都說ssl tls ssl tls位於應用層和傳輸層之間,應用層還是可以用http telnet等應用層協議,只是應用層的資料不是直接交給tcp,而是由tls管理,tls在頭部增加安...

TLS1 3 握手過程特性的整理

1 密碼協商 tls協議中,密碼協商的過程中client在clienthello中提供四種option 第一 client 支援的加密套件列表,密碼套件裡面中能出現client支援的aead演算法或者hkdf雜湊對,第二 supported group 的擴充套件和 key share的 擴充套件,...