- 相關(guān)推薦
網(wǎng)絡(luò)協(xié)議的形式化分析
網(wǎng)絡(luò)協(xié)議的形式化分析【1】
摘 要:隨著形式化方法和技術(shù)的日趨完善,網(wǎng)絡(luò)協(xié)議的開發(fā)已逐步從非形式化描述、手工方法實(shí)現(xiàn)過渡到已形式化描述技術(shù)為基礎(chǔ),滲透到網(wǎng)絡(luò)協(xié)議分析、綜合、測試等各環(huán)節(jié)的軟件工程方法。
本文從網(wǎng)絡(luò)協(xié)議的基本要素、協(xié)議的形式化模型介紹了網(wǎng)絡(luò)協(xié)議,并從協(xié)議的性質(zhì)描述、不變性分析、可達(dá)性分析、基于有序二叉判決圖的符號模型檢驗(yàn)對網(wǎng)絡(luò)協(xié)議進(jìn)行了形式化設(shè)計(jì)與驗(yàn)證,最后進(jìn)行了測試。
關(guān)鍵詞:網(wǎng)絡(luò)協(xié)議 形式化分析 符號模型檢驗(yàn)
協(xié)議一詞最早出現(xiàn)在通信系統(tǒng),協(xié)議歷史擁有像通信一樣古老的歷史。
從古至今,人們一直都在不斷的探索研究,怎樣才能建立一個(gè)能夠在快速在遠(yuǎn)距離上傳輸信息的系統(tǒng)。
如果想要實(shí)現(xiàn)信息在遠(yuǎn)距離間傳遞,不光需要硬件設(shè)備,也就是發(fā)送和接收信號的設(shè)備,還需要建立一整套能夠規(guī)定信號所代表的意義以及傳遞接收信號方式的規(guī)則、標(biāo)準(zhǔn)或者約定,這個(gè)規(guī)則就是協(xié)議。
1 網(wǎng)絡(luò)協(xié)議的基本要素
一套完整的,能夠確保計(jì)算機(jī)網(wǎng)絡(luò)可以順利進(jìn)行數(shù)據(jù)通信的網(wǎng)絡(luò)協(xié)議要包括下邊的五點(diǎn)基本要素:(1)協(xié)議所提供的服務(wù)。
(2)對協(xié)議運(yùn)行環(huán)境所進(jìn)行的假設(shè)。
(3)用來實(shí)現(xiàn)協(xié)議的消息詞匯。
(4)對該詞匯中每個(gè)消息的編碼。
(5)用來控制消息一致性的過程規(guī)則。
實(shí)現(xiàn)計(jì)算機(jī)之間高度自動(dòng)化數(shù)據(jù)通信的網(wǎng)絡(luò)協(xié)議,一般都會(huì)極其復(fù)雜。
借鑒對復(fù)雜系統(tǒng)問題分析研究的思想,分層結(jié)構(gòu)對于理解和設(shè)計(jì)網(wǎng)絡(luò)協(xié)議有著重要的作用。
“七層”協(xié)議結(jié)構(gòu)模型是目前網(wǎng)絡(luò)協(xié)議的標(biāo)準(zhǔn)體系結(jié)構(gòu),也成為了網(wǎng)絡(luò)協(xié)議開發(fā)的基礎(chǔ)。
2 協(xié)議的形式化模型
協(xié)議分析和設(shè)計(jì)其中一項(xiàng)核心技術(shù)就是形式化模型。
網(wǎng)絡(luò)協(xié)議的形式化規(guī)格可以在形式化模型的基礎(chǔ)上實(shí)現(xiàn),從而為協(xié)議的形式化分析與驗(yàn)證、協(xié)議綜合、協(xié)議測試、以及協(xié)議實(shí)現(xiàn)等提供良好的基礎(chǔ)。
形式化模型包括以下幾點(diǎn)。
2.1 協(xié)議的有限狀態(tài)機(jī)模型
有限狀態(tài)機(jī)包括有限狀態(tài)集、輸入集和狀態(tài)轉(zhuǎn)移規(guī)則集;有限狀態(tài)集,用于描述系統(tǒng)中的不同狀態(tài);輸入集用于表征系統(tǒng)所接收的不同輸入信息;狀態(tài)轉(zhuǎn)移規(guī)則集用于表述系統(tǒng)在接收不同輸入下從一個(gè)狀態(tài)轉(zhuǎn)移到另外一個(gè)狀態(tài)的規(guī)則。
2.2 Petri網(wǎng)模型
Petri網(wǎng)是一種適合于并發(fā)、異步、分布式系統(tǒng)描述與分析的圖形數(shù)學(xué)工具。
Petri網(wǎng)已成為網(wǎng)絡(luò)協(xié)議分析和設(shè)計(jì)的典型形式模型之一。
它作為系統(tǒng)描述和分析的工具,除了具有靜態(tài)結(jié)構(gòu)外,還包括了描述系統(tǒng)動(dòng)態(tài)行為的機(jī)制。
這一特征是通過允許位置中包含令牌,令牌可以依據(jù)遷移的引發(fā)而重新分布來實(shí)現(xiàn)的。
2.3 協(xié)議的時(shí)態(tài)邏輯模型
時(shí)態(tài)邏輯是模態(tài)邏輯的擴(kuò)充,它涉及含有時(shí)間信息的事件、狀態(tài)及其關(guān)系的命題、謂詞和演算。
要描述一個(gè)協(xié)議,首先要標(biāo)識系統(tǒng)中的個(gè)體常量,定義變量,表達(dá)命題、謂詞函數(shù)。
以下為命題與謂詞的表達(dá)。
(1)個(gè)體常量m0,m1表示序號為0,1的報(bào)文;any表示無序號的任意報(bào)文;ack0,ack1表示序號為0,1的認(rèn)可報(bào)文。
(2)個(gè)體變量m代表m0,m1,any;ack代表ack0,ack1;seq代表0,1序號;a代表原子行動(dòng)或事件。
(3)謂詞at(a)開始一個(gè)協(xié)議行動(dòng)或事件。
2.4 通信進(jìn)程演算模型
通信進(jìn)程演算是計(jì)算機(jī)通信系統(tǒng)的基本理論模型,它也是許多形式化語言的基礎(chǔ)。
通信進(jìn)程演算的基本成分是事件與進(jìn)程,而進(jìn)程是通過順序、選擇和并行三個(gè)基本算子來定義的。
一般用大寫字母來表示進(jìn)程,用小寫字母來表示事件。
3 協(xié)議的形式化設(shè)計(jì)與驗(yàn)證
協(xié)議的設(shè)計(jì)驗(yàn)證是對協(xié)議的功能和性能進(jìn)行校驗(yàn)的過程,是保證協(xié)議開發(fā)質(zhì)量的必要環(huán)節(jié)。
協(xié)議形式化驗(yàn)證首先需要對協(xié)議性質(zhì)進(jìn)行系統(tǒng)的語言描述,然后基于協(xié)議的形式模型或者形式語言進(jìn)行描述,通過適當(dāng)?shù)募夹g(shù)對協(xié)議性質(zhì)進(jìn)行分析校驗(yàn)。
3.1 協(xié)議的性質(zhì)描述
設(shè)計(jì)網(wǎng)絡(luò)協(xié)議的目的就是設(shè)計(jì)出的協(xié)議要滿足功能和性能。
一方面,協(xié)議本身應(yīng)用問題的特征性對協(xié)議的功能和性能具有特殊的要求;另外一方面,協(xié)議的功能和性能所擁有的協(xié)議的性質(zhì),是獨(dú)立于問題的一般性要求。
協(xié)議的性質(zhì)包括活性、安全性、一致性、完備性、可恢復(fù)性和有界性六方面。
(1)活性就是指無死鎖性,如果在協(xié)議運(yùn)行時(shí)候發(fā)生一些好事,就叫協(xié)議的活性,像發(fā)生預(yù)定的事情,能夠到達(dá)指定的協(xié)議狀態(tài),可以進(jìn)行應(yīng)該進(jìn)行的協(xié)議活動(dòng)等都是協(xié)議的好事情。
協(xié)議的終止性和進(jìn)展性兩反面可以體現(xiàn)協(xié)議的活性。
也就是說具有終止性和進(jìn)展性的協(xié)議就擁有活性。
如果協(xié)議能夠在從任何一狀態(tài)下開始運(yùn)行都能正確的到達(dá)終止?fàn)顟B(tài),就是協(xié)議的終止性。
終止?fàn)顟B(tài)在某些情況下也會(huì)和初始狀態(tài)是同一個(gè)。
所以協(xié)議總能從初始狀態(tài)開始運(yùn)行然后正確的回到初始狀態(tài),并可反復(fù)運(yùn)行,這就是協(xié)議的可重復(fù)性,即可重復(fù)性=終止性+進(jìn)展性=活動(dòng)性。
(2)安全性就是沒有壞的事情出現(xiàn)在協(xié)議運(yùn)行的時(shí)候。
像不可接收事件、不可進(jìn)一步向前的狀態(tài)、錯(cuò)誤的行動(dòng)、錯(cuò)誤的條件、變量值越界等都是壞的事情。
壞事情一般會(huì)導(dǎo)致死鎖和活鎖兩種情況發(fā)生。
(3)一致性就是指協(xié)議的服務(wù)行為和協(xié)議行為保持一致。
像協(xié)議需要為用戶提供的所要求的業(yè)務(wù)和不用提供用戶沒有要求提供的業(yè)務(wù)都體現(xiàn)了協(xié)議的一致性。
(4)完備性,協(xié)議擁有完全符合協(xié)議環(huán)境各種要求的性質(zhì),也就是在考慮了用戶要求、用戶特點(diǎn)、通道性質(zhì)、工作模式等各種潛在影響因素之后構(gòu)建的協(xié)議構(gòu)造,同時(shí)兼?zhèn)淇紤]各種錯(cuò)誤事件以及異常情況的處理。
(5)可恢復(fù)性是指當(dāng)協(xié)議出現(xiàn)差錯(cuò)后,協(xié)議本身能否在有限的步驟內(nèi)返回到正常狀態(tài)下執(zhí)行。
可恢復(fù)性是和可重復(fù)性相關(guān)聯(lián)的一個(gè)性質(zhì)。
(6)有界性是與協(xié)議中的變量和參數(shù)有關(guān)的一個(gè)性質(zhì),用來衡量協(xié)議中的變量和參數(shù)是否超過其限定值。
3.2 不變性分析
系統(tǒng)不變性是某一邏輯公式表達(dá)的系統(tǒng)性質(zhì)的永真性,它不隨系統(tǒng)的狀態(tài)變化或執(zhí)行序列而改變。
系統(tǒng)不變性分析實(shí)際包含兩個(gè)任務(wù)。
第一是分析系統(tǒng)應(yīng)該具有的不變性質(zhì),并用邏輯公式來表示,第二個(gè)任務(wù)是分析系統(tǒng)的執(zhí)行,證明該邏輯公式成立。
3.3 可達(dá)性分析
可達(dá)性分析是試圖產(chǎn)生和檢查協(xié)議所有部分的可達(dá)狀態(tài),進(jìn)而檢驗(yàn)基于狀態(tài)或者基于狀態(tài)序列的協(xié)議性質(zhì)。
所謂可達(dá)狀態(tài)是指協(xié)議從初始狀態(tài)開始經(jīng)歷有限次轉(zhuǎn)換之后可達(dá)到的狀態(tài),所有可達(dá)狀態(tài)構(gòu)成了系統(tǒng)狀態(tài)空間。
可達(dá)性分析算法是用來生成并檢驗(yàn)一個(gè)特定的初始狀態(tài)可達(dá)的所有狀態(tài)算法。
3.4 基于有序二叉判決圖的符號模型檢驗(yàn)
符號模型檢驗(yàn)是采用緊湊的信息壓縮形式來隱式表示系統(tǒng)可達(dá)狀態(tài)和要求證明性質(zhì)的邏輯公式的模型檢驗(yàn)。
有序二叉判決圖是隱式、高效率表示狀態(tài)空間的一種數(shù)據(jù)結(jié)構(gòu)。
基于有序二叉判決圖的符號模型檢驗(yàn)是分析驗(yàn)證協(xié)議系統(tǒng)的有效技術(shù)。
基于有序二叉判決圖實(shí)現(xiàn)的模型檢驗(yàn)算法能有效地避免狀態(tài)爆炸的問題,使得驗(yàn)證系統(tǒng)適用的系統(tǒng)規(guī)模擴(kuò)大,現(xiàn)已能對具有多達(dá)1020個(gè)狀態(tài)的系統(tǒng)進(jìn)行驗(yàn)證。
基于有序二叉判決圖的符號模型驗(yàn)證主要考慮以下幾個(gè)方面:狀態(tài)的布爾公式表示;狀態(tài)轉(zhuǎn)移關(guān)系的布爾公式表示;Kripke結(jié)構(gòu)的布爾公式表示;CTL公式在布爾公式表示的Kripke結(jié)構(gòu)上的解釋。
現(xiàn)用QBF公式表示Kripke結(jié)構(gòu),并把用這些符號表示的Kripke結(jié)構(gòu)上的CTL算子用QBF上的算子來描述。
實(shí)際上,因?yàn)檫壿嬤B接詞在CTL*和QBF上有著相同的意義,所以只需要刻畫算子EN,而其它的CTL*的算子可以通過EN和邏輯運(yùn)算的函數(shù)不動(dòng)點(diǎn)進(jìn)行描述。
4 網(wǎng)絡(luò)協(xié)議的測試
測試是保證網(wǎng)絡(luò)協(xié)議質(zhì)量的一個(gè)重要手段,是協(xié)議實(shí)現(xiàn)過程中的一種實(shí)驗(yàn)活動(dòng)。
盡管測試并不能完全證明協(xié)議實(shí)現(xiàn)的正確性,但是在系統(tǒng)的測試活動(dòng)檢查下,可以把協(xié)議在實(shí)現(xiàn)過程中出錯(cuò)的概率降低到實(shí)際應(yīng)用可以接受的程度。
相對而言,基于有限狀態(tài)機(jī)模型的協(xié)議測試方法有比較高的錯(cuò)誤覆蓋率。
然而,在實(shí)際中,協(xié)議規(guī)格的狀態(tài)機(jī)模型并不滿足對有限狀態(tài)機(jī)的假設(shè),即便滿足,相應(yīng)的測試生成算法也太復(fù)雜,生成的測試序列也太長,測試成本太高。
隨時(shí)著各種各樣的有限狀態(tài)機(jī)規(guī)格的廣泛使用,借助于軟件數(shù)據(jù)流測試的思想,基于數(shù)據(jù)流的協(xié)議測試序列生成方法相應(yīng)得到了研究應(yīng)用。
數(shù)據(jù)流測試通常基于有向數(shù)據(jù)流圖。
在理想情況下,測試所有可能的輸入數(shù)據(jù)將提供最完全的程序行為信息,而在實(shí)際測試中,通常選擇一個(gè)可以代表整個(gè)輸入域的子集。
5 結(jié)語
形式化方法是基于嚴(yán)密的、數(shù)學(xué)上的形式機(jī)制的系統(tǒng)研究方法。
客觀地講,有了數(shù)學(xué)的應(yīng)用,就有了形式化的方法。
迄今為止,形式化方法成功地應(yīng)用于空中交通管制系統(tǒng)、鐵路信號系統(tǒng)、核電站控制系統(tǒng)、通信系統(tǒng)、醫(yī)療監(jiān)護(hù)系統(tǒng)、硬件電路等諸多領(lǐng)域。
網(wǎng)絡(luò)協(xié)議的形式化分析和設(shè)計(jì)正在向完善化、系統(tǒng)化、自動(dòng)化和標(biāo)準(zhǔn)化方向發(fā)展。
參考文獻(xiàn)
[1] 魯來鳳,吳振強(qiáng),馬*峰.基于PCL的改進(jìn)型Helsinki協(xié)議的形式化分析[J].華中科技大學(xué)學(xué)報(bào)(自然科學(xué)版),2011(4).
[2] 王惠斌.安全認(rèn)證協(xié)議的設(shè)計(jì)與分析[D].解放軍信息工程大學(xué),2010.
無線網(wǎng)絡(luò)安全協(xié)議的形式化分析【2】
摘 要:傳統(tǒng)的有線網(wǎng)絡(luò)由于受到環(huán)境等條件的制約,在各方面都存在著亟需解決的問題,那么,發(fā)展可行的無線通信網(wǎng)絡(luò)技術(shù)也就成為網(wǎng)絡(luò)發(fā)展的必然趨勢。
本文對無線網(wǎng)絡(luò)安全協(xié)議的形式化方法進(jìn)行了全面的概述,分析了無線網(wǎng)絡(luò)的安全威脅以及具體表現(xiàn),著重探討了無線網(wǎng)絡(luò)安全協(xié)議的形式化分析方法。
關(guān)鍵詞:無線網(wǎng)絡(luò)安全;形式化分析;安全協(xié)議
中圖分類號:TP393.08
隨著科學(xué)技術(shù)的迅速發(fā)展,網(wǎng)絡(luò)得到了較大的發(fā)展空間,由于傳統(tǒng)的有線網(wǎng)絡(luò)隨著網(wǎng)絡(luò)應(yīng)用的不斷發(fā)展,難以適應(yīng)現(xiàn)代化社會(huì)的需求,因此逐漸被無線網(wǎng)絡(luò)替代,在豐富了人們生活的同時(shí)也給人們帶來了更為便捷的服務(wù)。
但是隨著無線網(wǎng)絡(luò)的發(fā)展,也將面臨著網(wǎng)絡(luò)安全問題。
1 無線網(wǎng)絡(luò)安全協(xié)議的形式化方法綜述
1.1 無線網(wǎng)絡(luò)安全協(xié)議
無線網(wǎng)絡(luò)的發(fā)展隨著社會(huì)經(jīng)濟(jì)的迅速發(fā)展,得到了較大的發(fā)展空間,并且隨著無線網(wǎng)絡(luò)的不斷發(fā)展,針對于無線網(wǎng)絡(luò)的一個(gè)個(gè)新的標(biāo)準(zhǔn)和技術(shù)也在不斷的出現(xiàn),在某一開放系統(tǒng)中由于主體數(shù)量比較大,而兩個(gè)互不相識的主體希望進(jìn)行安全通信,那么,它們之間就必須要建立一個(gè)安全的通信渠道,而建立了安全通信渠道的兩個(gè)主體之間必須要運(yùn)行某種安全協(xié)議,以此來完成雙方互相認(rèn)證的功能,當(dāng)然還應(yīng)該建立秘鑰任務(wù)。
而無線網(wǎng)絡(luò)安全協(xié)議也就是針對于無線網(wǎng)絡(luò)而言的安全信道,按照自己的功能可以將安全協(xié)議分為可以將其分為三類,首先是認(rèn)證協(xié)議,這主要是提供給一個(gè)參與方關(guān)于其通信對方身份的一定確信度的一種方式,認(rèn)證協(xié)議包含了實(shí)體認(rèn)證協(xié)議、消息認(rèn)證協(xié)議等其他協(xié)議,并且認(rèn)證協(xié)議主要是用來防止假冒、否認(rèn)等相關(guān)攻擊的。
其次是認(rèn)證及秘鑰交換協(xié)議,這主要是為了給身份已經(jīng)被確認(rèn)的參與方建立一個(gè)共享秘密,目前這種方式是網(wǎng)絡(luò)通信中最為普遍的一種安全協(xié)議。
最后是秘鑰交換協(xié)議,這種協(xié)議是在參與協(xié)議的兩個(gè)實(shí)體之間,或者是多個(gè)實(shí)體之間建立的共享秘密,尤其是這些秘密可以作為對稱秘鑰,用于加密、消息認(rèn)真以及實(shí)體認(rèn)證等多種密碼學(xué)用途[1]。
1.2 安全協(xié)議的形式化方法
針對于安全協(xié)議形式化分析,我們可以將其分為計(jì)算機(jī)安全方法,以及計(jì)算機(jī)復(fù)雜性方法兩大類,而計(jì)算機(jī)安全方法,又可以稱之為基于符號理論的形式化方法,它主要是強(qiáng)調(diào)自動(dòng)化機(jī)器的描述和分析,但是,由于這種方法存在不可預(yù)測性和復(fù)雜性,所以這種方法主要是由于攻擊者具有指數(shù)規(guī)模的可能操作集,會(huì)導(dǎo)致狀態(tài)爆炸的問題,計(jì)算機(jī)安全方法還可以進(jìn)一步分類:模態(tài)邏輯方法、模型監(jiān)測方法等。
計(jì)算機(jī)復(fù)雜性方法,也可以稱之為證明安全方法,其主要思想是通過歸納推理,而計(jì)算機(jī)復(fù)雜性方法中應(yīng)用較為廣泛的是CK模型和UC模型。
2 無線網(wǎng)絡(luò)的安全威脅和具無線網(wǎng)絡(luò)的具體表現(xiàn)
無線網(wǎng)絡(luò)的應(yīng)用較大程度的擴(kuò)大了無線網(wǎng)用戶的自由程度,并且無線網(wǎng)絡(luò)還具有安裝時(shí)間短,更改網(wǎng)絡(luò)結(jié)構(gòu)方便靈活,靈活增加用戶等等其他的優(yōu)點(diǎn),而最為重要的是它還可以提供無線覆蓋范圍內(nèi)的安全功能漫游服務(wù)等特點(diǎn)。
但是,與此同時(shí)無線網(wǎng)絡(luò)也面臨著一些嚴(yán)峻地新的挑戰(zhàn),而其中最為關(guān)鍵的環(huán)節(jié)就是無線網(wǎng)絡(luò)的安全性,而由于無線網(wǎng)絡(luò)主要是通過無線電波在空中進(jìn)行數(shù)據(jù)傳輸?shù)模跀?shù)據(jù)發(fā)射機(jī)覆蓋的區(qū)域內(nèi),基本上所有的無線用戶都能夠接收到這些數(shù)據(jù),也就是說用戶只需要具有相同的接收頻率,那么用戶就能夠獲取所傳遞的相關(guān)信息。
并且由于無線移動(dòng)設(shè)備在存儲能力,以及計(jì)算能力等其他的方面都存在一定的局限性,也就導(dǎo)致在有線環(huán)境下,許多安全方案以及安全技術(shù)并不能夠直接的在無線環(huán)境中應(yīng)用,比如:防火墻通過無線電波進(jìn)行的網(wǎng)絡(luò)通信并不具備一定的相關(guān)作用,而任何人在特定的區(qū)域范圍內(nèi)都能夠截獲或者是插入網(wǎng)絡(luò)數(shù)據(jù),導(dǎo)致無線網(wǎng)絡(luò)面臨著一些安全威脅{2]。
而針對于安全威脅,我們可以將其分為故意威脅和偶然威脅這兩種形式,而故意威脅又可以進(jìn)一步分為主動(dòng)故意威脅和被動(dòng)故意威脅,無線網(wǎng)絡(luò)安全威脅,主要表現(xiàn)在以下幾個(gè)方面。
首先,攻擊者偽裝成為合法的用戶,通過無線接入非法訪問網(wǎng)絡(luò)資源,從而給無線網(wǎng)絡(luò)帶來安全威脅,這是最為普遍的一種威脅;其次是針對無線連接或者是無線設(shè)備實(shí)施的拒絕服務(wù)攻擊;第三是惡意實(shí)體可能得到合法用戶的隱私,然后對無線網(wǎng)絡(luò)進(jìn)行非法入侵;第四,惡意用戶可能通過無線網(wǎng)絡(luò),將其自動(dòng)連接到自己想要攻擊的網(wǎng)絡(luò)上去,并采取相關(guān)方法實(shí)施對特定的網(wǎng)絡(luò)進(jìn)行攻擊。
此外還有很多種威脅,比如:手持設(shè)備容易丟失,從而泄露敏感信息。
3 無線網(wǎng)絡(luò)安全協(xié)議的形式化分析的具體方法
安全協(xié)議主要是采用密碼技術(shù)來保障通信各方之間安全交換信息的一個(gè)規(guī)則序列,其主要目的就是在通信各方之間提供認(rèn)證或?yàn)樾碌臅?huì)話分配會(huì)話密鑰,目前分析安全協(xié)議的形式化方法主要有三種,即:推理構(gòu)造法,這種方法主要是基于知識和信念推理的模態(tài)邏輯,比如K3P邏輯等其他邏輯;再有就是攻擊構(gòu)造法,這種方法從協(xié)議的初始狀態(tài)開始,對合法的主體和一個(gè)攻擊者所有可能執(zhí)行的路徑進(jìn)行全方面的搜索,以此來找到協(xié)議可能存在的問題;此外還有證明構(gòu)造法,證明構(gòu)造法集成了上述兩種方法的思想和技術(shù)。
對于無線網(wǎng)絡(luò)安全協(xié)議的形式化分析方法,筆者認(rèn)為,可以從以下三個(gè)方面進(jìn)行分析。
第一,基于邏輯證明的協(xié)議分析。
BNA邏輯,這種方法最早用于認(rèn)證和秘鑰交換協(xié)議的形式化方法,它的出現(xiàn)極大地激發(fā)了研究人員對于這一領(lǐng)域的廣泛興趣,BAN邏輯中的證明構(gòu)造是非常簡潔的,并且它還比較容易完成,但是,應(yīng)用BNA邏輯分析只是一個(gè)協(xié)議,從具體的協(xié)議到邏輯表達(dá)式的抽象過程都是比較困難的。
BNA邏輯的語法中區(qū)分了主體、秘鑰以及時(shí)鮮值這三種密碼要素,并且BNA邏輯可以對WAI的認(rèn)證模型進(jìn)行有效的分析,但通過相關(guān)研究表明,WAI并不能夠有效地實(shí)現(xiàn)全部的認(rèn)證以及秘鑰協(xié)商目標(biāo),這主要是由于WAI中存在著諸多的安全問題,比如:無法提供身份保護(hù)、缺乏私鑰驗(yàn)證等,這就表明WAPI無法提供足夠級別的安全保護(hù){3]。
第二,攻擊類型以及安全密碼協(xié)議形式化的分析。
在任何一個(gè)開放性的無線網(wǎng)絡(luò)環(huán)境中,網(wǎng)絡(luò)管理人員必須要全方位地考慮到對攻擊者存在,主要是由于攻擊者可能實(shí)施各種攻擊,對一些具有價(jià)值的文件和網(wǎng)絡(luò)系統(tǒng)進(jìn)行破壞,要處理這種安全問題就必須要積極的采取一定的措施。
認(rèn)證協(xié)議主要是建立在密碼基礎(chǔ)上的,而它的主要目的就是為了能夠有效地證明所聲稱的某種屬性,認(rèn)證協(xié)議的主要攻擊者判定是依靠有沒有授權(quán),并且企圖獲益的攻擊者或共謀者。
在一般情況下,進(jìn)行分析認(rèn)證協(xié)議的時(shí),主要采用的是假設(shè)底層密碼算法比較完善的方式,并不考慮其可能存在的弱點(diǎn),認(rèn)證協(xié)議典型的攻擊主要有消息攻擊、中間人攻擊以及平行會(huì)話攻擊等其他形式。
第三,基于CK模型的協(xié)議形式化分析。
CK模型的協(xié)議形式化,其主要目標(biāo)是通過模塊化的方法來設(shè)計(jì)和分析秘鑰交換協(xié)議,以此來簡化協(xié)議的設(shè)計(jì)和安全分析,首先必須要將秘鑰協(xié)商協(xié)議定義在理想的模型之中,之后再采用不可區(qū)分性來定義理想模型中的安全性,然后再通過相關(guān)方法將協(xié)議編譯成現(xiàn)實(shí)模型中的協(xié)議,CK模型采用了相關(guān)方法對WAPI的安全性進(jìn)行了分析,并指出WAPI中存在的安全缺陷。
4 結(jié)束語
綜上所述,無線網(wǎng)絡(luò)給人們的生活和工作等方面帶來了較大的便利性,但是由于無線網(wǎng)絡(luò)具有開放性和無線終端的移動(dòng)性等特點(diǎn),導(dǎo)致在有限網(wǎng)絡(luò)環(huán)境下的一些安全方案無法直接應(yīng)用。
采用形式化分析方法能夠有效的研究出無線網(wǎng)絡(luò)的安全保障技術(shù),從而促進(jìn)我國網(wǎng)絡(luò)技術(shù)的發(fā)展。
參考文獻(xiàn):
[1]寧向延,張順頤.網(wǎng)絡(luò)安全現(xiàn)狀與技術(shù)發(fā)展[J],南京郵電大學(xué)學(xué)報(bào)(自然科學(xué)版),2012(05).
[2]李浩.無線網(wǎng)絡(luò)技術(shù)難點(diǎn)分析及安全方法探討[J],技術(shù)與市場,2014(07).
【網(wǎng)絡(luò)協(xié)議的形式化分析】相關(guān)文章:
網(wǎng)絡(luò)經(jīng)濟(jì)對企業(yè)的影響分析10-05
網(wǎng)絡(luò)傳銷的特點(diǎn)與治理對策分析論文10-09
經(jīng)濟(jì)神經(jīng)網(wǎng)絡(luò)活動(dòng)分析的論文10-09
網(wǎng)絡(luò)道德與現(xiàn)實(shí)社會(huì)道德關(guān)系分析10-08
分析網(wǎng)絡(luò)小說流行性09-30
分析房地產(chǎn)網(wǎng)絡(luò)營銷10-08
校園網(wǎng)基本網(wǎng)絡(luò)搭建及網(wǎng)絡(luò)安全設(shè)計(jì)分析10-08