擴(kuò)展基于本地會(huì)話的安全協(xié)議驗(yàn)證邏輯分析TLS協(xié)議.pdf

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

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