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