基于GSPM的安全協(xié)議性質(zhì)檢驗(yàn)及其工具實(shí)現(xiàn).pdf

1、隨著網(wǎng)絡(luò)技術(shù)逐步應(yīng)用到許多重要部門，安全協(xié)議是否能達(dá)到所要求的安全目標(biāo)是非常關(guān)鍵的問(wèn)題。借助形式化的方法或者工具是分析和檢驗(yàn)安全協(xié)議性質(zhì)的一個(gè)重要技術(shù)手段。GSPM是這樣一種可以精確刻畫安全協(xié)議的一般模型。本文在GSPM的基礎(chǔ)上，對(duì)安全協(xié)議的性質(zhì)進(jìn)行了研究。主要內(nèi)容如下： ⑴由于類型缺陷漏洞與協(xié)議的消息類型相關(guān)，并且GSPM對(duì)消息類型的匹配規(guī)則過(guò)于嚴(yán)格，導(dǎo)致類型缺陷漏洞無(wú)法通過(guò)該模型進(jìn)行驗(yàn)證，本文通過(guò)對(duì)GSPM語(yǔ)義的修改和對(duì)消息

2、匹配語(yǔ)法做一定的弱化，使GSPM能正確檢測(cè)類型缺陷漏洞。 ⑵在GSPM模型理論的基礎(chǔ)上設(shè)計(jì)了一套分析安全協(xié)議的算法，包括消息推理算法，消息匹配算法和狀態(tài)搜索算法。通過(guò)線性時(shí)序邏輯來(lái)表示安全協(xié)議的性質(zhì)，例如保密性和認(rèn)證性，并根據(jù)線性時(shí)序邏輯的特性設(shè)計(jì)了對(duì)應(yīng)的檢驗(yàn)算法。 ⑶介紹了一個(gè)自主開發(fā)的基于GSPM和上述檢驗(yàn)算法的自動(dòng)驗(yàn)證工具。這一工具能夠?qū)⒂脩糨斎氲陌踩珔f(xié)議及其安全目標(biāo)自動(dòng)翻譯為GSPM語(yǔ)言；再根據(jù)GSPM的模型檢測(cè)