[發(fā)明專利]網(wǎng)絡(luò)協(xié)議安全建模方法

無效

• 申請?zhí)枺?/td>: 201210245424.5
• 申請日: 2012-07-16
• 公開（公告）號: CN102780817A
• 公開（公告）日: 2012-11-14
• 發(fā)明（設(shè)計(jì)）人: 李曉紅;謝肖飛;陳世展;饒國政;曹坤宇;韓卓冰
• 申請（專利權(quán)）人: 天津大學(xué)
• 主分類號: H04M1/725
• 分類號: H04M1/725
• 代理公司: 天津市北洋有限責(zé)任專利代理事務(wù)所 12201
• 代理人: 李素蘭

技術(shù)領(lǐng)域

本發(fā)明涉及網(wǎng)絡(luò)安全技術(shù)領(lǐng)域；特別是涉及一種對網(wǎng)絡(luò)協(xié)議的安全缺陷建模技術(shù)。

背景技術(shù)

隨著Internet的不斷發(fā)展，人們對互聯(lián)網(wǎng)的依賴已經(jīng)變得越來越重要。互聯(lián)網(wǎng)作為信息技術(shù)革命的一個重要環(huán)節(jié)，已經(jīng)深深的影響著每個人的工作，學(xué)習(xí)和生活。互聯(lián)網(wǎng)更多的涉及到了金錢利益，隱私，版權(quán)專利，是絕大多數(shù)機(jī)關(guān)企業(yè)單位正常運(yùn)維的關(guān)鍵砝碼。

與此同時，安全問題也越來越得到重視。作為Internet的通信基礎(chǔ)，許多協(xié)議在設(shè)計(jì)過程中僅僅考慮到了通信而忽略了安全問題。因此攻擊者可以利用協(xié)議中存在的缺陷來攻擊系統(tǒng)，從而對用戶造成危害。因此，只有協(xié)議的安全得到保證，才能確保互聯(lián)網(wǎng)的可靠，才能保證用戶的利益。

網(wǎng)絡(luò)協(xié)議的開發(fā)過程包括分析、設(shè)計(jì)、實(shí)現(xiàn)、測試與維護(hù)等階段，設(shè)計(jì)一個安全的協(xié)議非常困難，主要原因在于：協(xié)議本身所具有的微妙性，還有協(xié)議所存在環(huán)境的復(fù)雜性，攻擊者模型的復(fù)雜性以及協(xié)議的高并發(fā)性。現(xiàn)在對網(wǎng)絡(luò)協(xié)議的形式化建模主要有有限狀態(tài)自動機(jī)(FSM)建模，Petri網(wǎng)建模，時態(tài)邏輯建模和通信進(jìn)程演算。有限狀態(tài)自動機(jī)的建模方式是目前最流行的，基本思想是對協(xié)議中的組件狀態(tài)及其狀態(tài)轉(zhuǎn)換進(jìn)行分析，在此基礎(chǔ)上進(jìn)行安全的分析和驗(yàn)證。通過對FSM模型的擴(kuò)展，加入特定屬性來完成協(xié)議信息的補(bǔ)充以達(dá)到特性的建模目的。Petri網(wǎng)是一種描述分布式系統(tǒng)的數(shù)學(xué)建模語言，通常以位置和遷移形式來表述系統(tǒng)所具有的狀態(tài)及狀態(tài)之間的遷移條件。時態(tài)邏輯的網(wǎng)絡(luò)協(xié)議建模是模態(tài)邏輯的擴(kuò)展，它涉及含有時間信息的時間、狀態(tài)及其關(guān)系的命題、謂詞和演算。通信進(jìn)程演算是計(jì)算機(jī)通信系統(tǒng)的基本理論模型，它是許多形式化語言的基礎(chǔ)。

現(xiàn)有的方法主要集中于特定安全協(xié)議與一些特定系統(tǒng)，因此這些方法具有一定的局限性。本發(fā)明針對網(wǎng)絡(luò)協(xié)議，提出了一種基于協(xié)議定義分析與建模的方法。運(yùn)用通信順序進(jìn)程CSP描述協(xié)議本身與所處環(huán)境（用入侵者所表示），并運(yùn)用自動化的驗(yàn)證工具對所建立的模型進(jìn)行安全驗(yàn)證。

發(fā)明內(nèi)容

基于上述現(xiàn)有技術(shù)存在的問題，本發(fā)明提出了一種網(wǎng)絡(luò)協(xié)議安全建模方法，針對網(wǎng)絡(luò)協(xié)議的安全缺陷，基于協(xié)議規(guī)格描述與進(jìn)程代數(shù)CSP，提出了一種對網(wǎng)絡(luò)協(xié)議分析及其建模的方法。運(yùn)用模型檢測工具對其驗(yàn)證，以便發(fā)現(xiàn)協(xié)議所存在的缺陷。

本發(fā)明提出了一種網(wǎng)絡(luò)協(xié)議安全建模方法，包括以下步驟：

步驟一、針對網(wǎng)絡(luò)協(xié)議的定義包括語法、語義與規(guī)則進(jìn)行抽象得到多個CSP進(jìn)程，由所述進(jìn)程通過進(jìn)程代數(shù)算子得到網(wǎng)絡(luò)協(xié)議基本模型；

步驟二、針對入侵者的內(nèi)容包括語法、語義與規(guī)則進(jìn)行抽象得到多個CSP進(jìn)程，由所述進(jìn)程通過進(jìn)程代數(shù)算子得到入侵者模型；

步驟三、由所述網(wǎng)絡(luò)協(xié)議基本模型與所述入侵者模型，經(jīng)過specModel=P1||P2....||Pn并行運(yùn)算得到相互關(guān)聯(lián)的協(xié)議模型，其中||為CSP并行運(yùn)算算子；P1、P2~Pn分別表示協(xié)議運(yùn)行中各個主體進(jìn)程與入侵者進(jìn)程；

步驟四、運(yùn)用驗(yàn)證工具FDR2對上述步驟三所獲得的協(xié)議模型進(jìn)行協(xié)議性質(zhì)的驗(yàn)證，協(xié)議性質(zhì)是協(xié)議需要滿足的約束，表示為CSP進(jìn)程：property=Ps1||Ps2....||Psn；（其中Ps1、Ps2~Psn分別描述約束的進(jìn)程）；FDR通過驗(yàn)證specModel的狀態(tài)遷移系統(tǒng)是否是property的一個模型來判斷約束性質(zhì)是否滿足；如果不滿足性質(zhì)，得出一個反例路徑，該路徑即是協(xié)議的缺陷。

與現(xiàn)有技術(shù)相比，本發(fā)明通過在設(shè)計(jì)階段對網(wǎng)絡(luò)協(xié)議進(jìn)行形式化的建模，可以準(zhǔn)確的描述協(xié)議，進(jìn)而對協(xié)議模型進(jìn)行驗(yàn)證，可以提早發(fā)現(xiàn)協(xié)議的缺陷。

附圖說明

圖1為現(xiàn)有技術(shù)的協(xié)議入侵模型示意圖；

圖2為本發(fā)明的網(wǎng)絡(luò)協(xié)議安全建模方法的驗(yàn)證和分析步驟流程示意圖；

圖3為本發(fā)明具體實(shí)施例的BGP協(xié)議分析步驟流程示意圖；

圖4為本發(fā)明的網(wǎng)絡(luò)協(xié)議安全建模方法的基于規(guī)則庫的的攻擊路徑發(fā)現(xiàn)步驟流程示意圖；

圖5為本發(fā)明的網(wǎng)絡(luò)協(xié)議安全建模方法的BGP驗(yàn)證結(jié)果示意圖。

具體實(shí)施方式

以下結(jié)合附圖及較佳實(shí)施例，對依據(jù)本發(fā)明提供的具體實(shí)施方式、結(jié)構(gòu)、特征及其功效，詳細(xì)說明如下。

下面結(jié)合附圖對本發(fā)明中的編碼實(shí)現(xiàn)和驗(yàn)證小果進(jìn)行詳述。

如圖1所示，包括協(xié)議的基本模型與入侵者模型。