安全協(xié)議的漏洞分析及自動(dòng)驗(yàn)證工具.pdf

1、網(wǎng)絡(luò)時(shí)代的今天，多種服務(wù)于互聯(lián)網(wǎng)應(yīng)用的網(wǎng)絡(luò)安全協(xié)議紛紛誕生；由安全協(xié)議設(shè)計(jì)上的漏洞引發(fā)的安全問題也越來(lái)越引起人們的重視。復(fù)雜的網(wǎng)絡(luò)環(huán)境使攻擊者可以利用通信協(xié)議自身的缺陷來(lái)實(shí)施各種各樣的攻擊，也給確保協(xié)議的安全性帶來(lái)較大難度。 安全協(xié)議形式化分析技術(shù)的提出，將協(xié)議的安全性問題轉(zhuǎn)化為數(shù)學(xué)問題，采用數(shù)學(xué)證明的手段來(lái)代替直覺的判定，近年來(lái)已逐步被公認(rèn)為解決安全問題的合理方案。國(guó)內(nèi)外先后出現(xiàn)了多種模型和研究方法。 本文主要從漏洞分

2、析的角度，對(duì)安全協(xié)議形式化方法做了一些探索。首先通過對(duì)安全協(xié)議缺陷的觀察和整理，從形式化角度將所有的安全問題歸納為六大漏洞，即身份認(rèn)證漏洞、假冒攻擊漏洞、保密數(shù)據(jù)泄漏漏洞、新鮮性漏洞、類型攻擊漏洞和攻擊者不當(dāng)?shù)美┒?。能否完善解決這六大漏洞的檢測(cè)與判定，可作為安全協(xié)議形式化模型是否完備的參考標(biāo)準(zhǔn)。 接著，通過對(duì)“一般安全協(xié)議模型（GSPM）”的增強(qiáng)與完善，將新鮮性漏洞和類型攻擊漏洞的驗(yàn)證引入該模型，并分別給予實(shí)例研究。一般安全協(xié)

3、議模型本身已是較為成熟的一個(gè)安全協(xié)議形式化模型，但由于缺乏時(shí)間上的語(yǔ)義，并不能解決新鮮性漏洞問題。另一方面，由于類型缺陷漏洞與協(xié)議中通信的消息類型相關(guān)，而一般安全協(xié)議模型對(duì)消息類型的匹配檢測(cè)規(guī)則過于嚴(yán)格，導(dǎo)致了類型缺陷漏洞也無(wú)法通過該模型進(jìn)行驗(yàn)證。通過在模型中加入時(shí)間語(yǔ)義和新鮮性的定義，并對(duì)消息匹配語(yǔ)法做了一定的弱化，使一般安全協(xié)議模型能正確檢測(cè)新鮮性漏洞及類型缺陷漏洞，系統(tǒng)功能上更加完善。 安全協(xié)議的形式化方法雖然有效，但是由

4、于數(shù)學(xué)建模的困難以及證明中的大計(jì)算量，純手工的驗(yàn)證過程并不是理想的途徑，效率和準(zhǔn)確率都難以保證。本文的第三個(gè)要點(diǎn)就是針對(duì)這個(gè)問題，完成了一個(gè)基于一般安全協(xié)議模型的自動(dòng)驗(yàn)證工具。這一工具能夠?qū)⒂脩糨斎氲陌踩珔f(xié)議及其安全目標(biāo)自動(dòng)翻譯為GSPM語(yǔ)言，也即自動(dòng)建模；再根據(jù)GSPM的模型檢測(cè)規(guī)則，選用特定的狀態(tài)搜索算法，通過自動(dòng)計(jì)算，判斷出安全目標(biāo)是否滿足，并將可能的漏洞以攻擊路徑的方式提供給用戶。在協(xié)議的輸入形式上，采用了XML這種通用性和可讀