安全協(xié)議形式化分析中認(rèn)證測(cè)試方法的研究.pdf

1、安全協(xié)議是安全共享網(wǎng)絡(luò)資源的機(jī)制和規(guī)范，是構(gòu)建網(wǎng)絡(luò)安全環(huán)境的基石，其安全性對(duì)整個(gè)網(wǎng)絡(luò)環(huán)境的安全起著至關(guān)重要的作用。由于協(xié)議安全屬性的多樣性和微妙性、攻擊者模型的不確定性、協(xié)議運(yùn)行環(huán)境的復(fù)雜性和協(xié)議會(huì)話的高并發(fā)性，安全協(xié)議的設(shè)計(jì)與分析至今仍是一項(xiàng)具有挑戰(zhàn)性的工作。形式化方法的出現(xiàn)有助于精確定義安全協(xié)議的目標(biāo)，準(zhǔn)確描述安全協(xié)議的行為，驗(yàn)證安全協(xié)議是否滿足預(yù)期目標(biāo)。人們?cè)诎踩珔f(xié)議的形式化分析上研究探索了近三十年，但這個(gè)領(lǐng)域仍然遠(yuǎn)未成熟。串空間

2、理論的出現(xiàn)將安全協(xié)議形式化分析推向了一個(gè)新的高度，它以簡(jiǎn)潔、嚴(yán)謹(jǐn)、高效的特點(diǎn)成為近年來(lái)安全協(xié)議形式化領(lǐng)域的研究熱點(diǎn)。在串空間理論上發(fā)展起來(lái)的認(rèn)證測(cè)試方法以挑戰(zhàn)—應(yīng)答機(jī)制為基礎(chǔ)，它充分利用串空間理論中代表事件因果關(guān)系的偏序結(jié)構(gòu)，不僅繼承了傳統(tǒng)串空間模型簡(jiǎn)單直觀、狀態(tài)空間少的優(yōu)點(diǎn)，還簡(jiǎn)化了證明過(guò)程，更符合安全協(xié)議形式化分析的發(fā)展方向。 本文以認(rèn)證測(cè)試方法在協(xié)議形式化分析和協(xié)議輔助設(shè)計(jì)中的應(yīng)用、認(rèn)證測(cè)試?yán)碚摰臄U(kuò)展和改進(jìn)，基于認(rèn)證測(cè)試的

3、協(xié)議自動(dòng)化分析算法的設(shè)計(jì)與實(shí)現(xiàn)為主要內(nèi)容，進(jìn)行了系統(tǒng)深入的研究，取得了如下創(chuàng)新性成果： 1．從協(xié)議分析的角度考慮對(duì)協(xié)議安全構(gòu)成威脅的攻擊類型和攻擊者行為，著重對(duì)最為常見的攻擊形式——重放攻擊進(jìn)行了分類研究。指出了Syverson重放攻擊分類法的不足，按攻擊產(chǎn)生的原因?qū)⒅胤殴舴殖闪宋孱悾槍?duì)每個(gè)類別列出具體的攻擊實(shí)例，并提出抵御該類攻擊的原則性方法。這種新的重放攻擊分類法對(duì)于更好地認(rèn)識(shí)各種攻擊的原理及尋找有效解決措施具有積極的意

4、義。 2．分別使用串空間最小元素方法、理想誠(chéng)實(shí)方法和認(rèn)證測(cè)試方法對(duì)Otway—Rees協(xié)議進(jìn)行分析，總結(jié)了這三種方法進(jìn)行協(xié)議分析的過(guò)程和特點(diǎn)，指出認(rèn)證測(cè)試方法是前兩者的歸納與概括，是理論上的進(jìn)一步深入，其證明過(guò)程更簡(jiǎn)潔高效。使用認(rèn)證測(cè)試方法對(duì)X．509三消息協(xié)議進(jìn)行保密性和認(rèn)證性分析，指出該協(xié)議存在的問(wèn)題及可能受到的攻擊；對(duì)協(xié)議加以改進(jìn)，并使用認(rèn)證測(cè)試方法證明了改進(jìn)協(xié)議的正確性。 3．結(jié)合協(xié)議設(shè)計(jì)一般原則和J．D．Gut

5、tman的協(xié)議設(shè)計(jì)思想，闡述了將認(rèn)證測(cè)試方法用于輔助協(xié)議設(shè)計(jì)的可行性，提出了基于認(rèn)證測(cè)試的通用協(xié)議設(shè)計(jì)思想。將協(xié)議設(shè)計(jì)過(guò)程分解為五個(gè)步驟，詳細(xì)討論了對(duì)稱密鑰體制和不對(duì)稱密鑰體制下構(gòu)造認(rèn)證測(cè)試的方法。并使用該方法設(shè)計(jì)了一個(gè)新的雙向認(rèn)證密鑰協(xié)商協(xié)議，擴(kuò)展了認(rèn)證測(cè)試方法的應(yīng)用范圍。 4．將基于認(rèn)證測(cè)試的安全協(xié)議形式化分析過(guò)程標(biāo)準(zhǔn)化，解決了“認(rèn)證測(cè)試方法的證明過(guò)程過(guò)于依賴分析人員的主觀判斷”和“認(rèn)證測(cè)試元素出現(xiàn)位置可能不唯一”的問(wèn)題，使

6、得認(rèn)證測(cè)試的應(yīng)用過(guò)程更嚴(yán)謹(jǐn)規(guī)范，有利于自動(dòng)化分析工具的實(shí)現(xiàn)。使用標(biāo)準(zhǔn)化方法對(duì)BAN—Yahalom協(xié)議進(jìn)行分析，找到了針對(duì)該協(xié)議的一個(gè)已知攻擊的更普遍形式。 5．分析了認(rèn)證測(cè)試方法中“測(cè)試元素不能是任何常規(guī)結(jié)點(diǎn)消息組成元素的真子項(xiàng)”這一局限性產(chǎn)生的根本原因，指出了Perrig和Song改進(jìn)方案的漏洞，提出的新認(rèn)證測(cè)試?yán)碚撚行黄屏苏J(rèn)證測(cè)試定理無(wú)法分析多重加密協(xié)議的局限性，并通過(guò)理論證明和實(shí)例分析說(shuō)明了新認(rèn)證測(cè)試定理的正確性，進(jìn)一

7、步擴(kuò)展了認(rèn)證測(cè)試方法的應(yīng)用范圍。 6．針對(duì)“認(rèn)證測(cè)試?yán)碚摬荒茏R(shí)別類型缺陷攻擊”的不足，結(jié)合強(qiáng)制類型檢查思想，將消息項(xiàng)的類型和檢查機(jī)制引入認(rèn)證測(cè)試方法，使得認(rèn)證測(cè)試方法可以根據(jù)應(yīng)用需求檢測(cè)出不同層次的類型缺陷攻擊。并以O(shè)tway—Rees、AndrewRPC和Woo—Lam改進(jìn)協(xié)議的分析為例，確認(rèn)了這一改進(jìn)的成功。 7．根據(jù)認(rèn)證測(cè)試?yán)碚摰纳鲜鋈c(diǎn)改進(jìn)，模擬手工證明過(guò)程，設(shè)計(jì)了一個(gè)基于認(rèn)證測(cè)試的協(xié)議自動(dòng)化分析算法ATAPA并