擴展基于本地會話的安全協(xié)議驗證邏輯分析TLS協(xié)議.pdf

1、安全協(xié)議是保證網(wǎng)絡(luò)安全的重要技術(shù)之一，但安全協(xié)議自身的缺陷，往往會導(dǎo)致很嚴(yán)重的安全問題。如何驗證安全協(xié)議能否實現(xiàn)其安全目標(biāo)，成了研究中的熱點問題。近年來，導(dǎo)師蘇開樂教授提出了一種基于本地會話的安全協(xié)議驗證邏輯(LLS)，能有效的對協(xié)議的安全性進行分析。由于該理論是一個全新的理論，需要對其進行擴展，以使其能分析更多的協(xié)議。 傳輸層安全協(xié)議(TLS，transport layer security)是由IETF在SSL3.0的基礎(chǔ)上

2、提出的互聯(lián)網(wǎng)標(biāo)準(zhǔn)，得到了廣泛的應(yīng)用，其安全性的分析有很高的研究價值。 本文針對對稱密鑰協(xié)商協(xié)議的分析，在LLS邏輯的基礎(chǔ)上進行了擴展。本文在LLS邏輯最核心的(n，1)-secrecy定理中加入了對協(xié)商密鑰的分析，針對協(xié)商密鑰協(xié)議要認(rèn)證的安全規(guī)范增加了公理，并對擴展的部分做了證明。隨后，本文使用擴展后的LLS邏輯分析了TLS協(xié)議的安全性。本文首先分析了認(rèn)證密鑰協(xié)商協(xié)議的實現(xiàn)目標(biāo)，包括實體認(rèn)證、密鑰認(rèn)證、密鑰確認(rèn)、消息完整性等，然