安全協(xié)議的漏洞分析及自動驗證工具.pdf

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

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

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

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