計算機網(wǎng)絡通信協(xié)議驗證技術的有機運用

王文韜

（湖北科技學院，湖北 咸寧 437100）

1 計算機網(wǎng)絡通信協(xié)議的相關概述

1.1 計算機網(wǎng)絡協(xié)議的定義

計算機網(wǎng)絡協(xié)議的本質就是計算機必須遵從的通信規(guī)則。網(wǎng)絡協(xié)議在制定的過程中必須要嚴格按照標準的體系結構執(zhí)行，在科學技術不斷的發(fā)展之中網(wǎng)絡通信標準體系也不斷更新和完善，如今最為常用的標準為TCP/IP協(xié)議組以及ISO兩種標準。通信技術的順利實施就必須要保障其中所有的內容完全遵從于統(tǒng)一的信息交換準則[1]。

1.2 計算機網(wǎng)絡協(xié)議的特性

計算機網(wǎng)絡協(xié)議主要包含如下特性。（1）活動性，在實際中通常表現(xiàn)為進展性和終止性，假如網(wǎng)絡協(xié)議不具備這兩種特性，那么他的活動性也是不存在的。（2）安全性。安全性主要是指協(xié)議在執(zhí)行時發(fā)生活鎖和死鎖等安全問題。例如，出現(xiàn)死鎖現(xiàn)象時，網(wǎng)絡協(xié)議所有的實體都呈現(xiàn)等待狀態(tài)，唯有發(fā)生“某一事件”之后方能夠執(zhí)行下一環(huán)節(jié)的操作。但是，在現(xiàn)實之中便是當網(wǎng)絡協(xié)議處于這種等待情況時，是不可能發(fā)生“某一事件”的，也就是說協(xié)議處于死鎖狀態(tài)之后便不可能通過某一事件解脫。這就類似于網(wǎng)絡協(xié)議一直在接受一個重復的循環(huán)命令，然而其又沒有辦法接受相關的確認信息，因此一直處于一個固定的狀態(tài)。（3）有界性、完整性以及同步性。工作人員要重點檢測網(wǎng)絡協(xié)議中的成分和參數(shù)，還要針對協(xié)議之中有無未解決的問題以及非期待的命令等進行檢驗和檢測。在此期間，假如協(xié)議出現(xiàn)無錯的情況，是否可以保障協(xié)議重新開始并且順利運行下去，這些都是需要重點觀察的部分。

2 計算機網(wǎng)絡通信協(xié)議的主要類型

2.1 局域網(wǎng)使用的通信協(xié)議

TCP/IP作為互聯(lián)網(wǎng)最基礎的協(xié)議，是局域網(wǎng)運用最廣泛的通信協(xié)議，其具備高度的靈活性，可以實現(xiàn)眾多服務器以及工作站的連接。TCP/IP協(xié)議經(jīng)過其帶有的IP地址來對網(wǎng)絡中的詳細位置以及身份給予高效識別[2]。IP地址主要包含如下要素，即節(jié)點和網(wǎng)絡ID。在多網(wǎng)段的背景之下能夠擴展網(wǎng)絡ID，通過子網(wǎng)掩碼管理子網(wǎng)。在連接異種網(wǎng)絡時，人們普遍以一個翻譯者的身份設置網(wǎng)關達到精確翻譯通信協(xié)議的目的，實現(xiàn)網(wǎng)絡相互通信的效果。

2.2 廣域網(wǎng)使用的通信協(xié)議

廣域網(wǎng)的通信協(xié)議存在多種多樣的形式，包含點到點協(xié)議等。廣域網(wǎng)協(xié)議從本質上講就是對不同廣域網(wǎng)介質上的通信進行了明確的界定。

2.3 路由器選擇協(xié)議

路由器選擇協(xié)議主要工作區(qū)間為網(wǎng)絡層，其實現(xiàn)了路徑選擇和交換。路由器選擇協(xié)議主要包含內部路由協(xié)議和外部路由協(xié)議兩種，前者是在系統(tǒng)內部實現(xiàn)路由協(xié)議的交換，后者實現(xiàn)不同自治系統(tǒng)的協(xié)議互換。

3 驗證技術在計算機網(wǎng)絡通信協(xié)議中的主要應用

3.1 Ping程序在網(wǎng)絡協(xié)議中的應用

Ping程序的作用是實施對一幀數(shù)據(jù)的檢測工作，即計算機進行數(shù)據(jù)轉換所需要的時間。假如計算機網(wǎng)絡在正常運行時突然產生問題，ping程序能夠幫助工作人員迅速辨別問題產生的原因。Ping程序的成功執(zhí)行只是為主機與目標主機的連接提供一條成物理路徑并且給予一些相關的參數(shù)。例如，-n可以依賴于自身的力量明確地向目標主機發(fā)送數(shù)據(jù)幀數(shù)。

3.2 基于有限狀態(tài)自動機模型的協(xié)議驗證與分析

形式描述技術中一個關鍵性的形式便是有限狀態(tài)機FSM，在FDT中扮演了十分重要的角色。可達性分析技術是目前有限狀態(tài)機運用最為廣泛的一項技術[1]。 其力圖對協(xié)議的可達狀態(tài)進行檢測。可達性分析關鍵性環(huán)節(jié)便是產生和檢查可達圖，檢測協(xié)議是否正確，其中包含3個核心技術：首先是尋找全部的可達圖并且建立可達圖；其次是檢驗協(xié)議的正確性；最后是處理狀態(tài)爆炸現(xiàn)象。普遍來看，所有的轉變都能夠經(jīng)過運用系統(tǒng)全局狀態(tài)達到明確特性的目的，類似于表明此時是不是死鎖狀態(tài)，全部的實體能不能夠接收報文等。基于FSM描述的協(xié)議驗證主要是借助于可達樹來發(fā)揮作用。其中系統(tǒng)的初始狀態(tài)為可達樹的根。從初始狀態(tài)開始將全部的轉移列舉出來，可達數(shù)的一個葉節(jié)點便是由這些轉移的狀態(tài)空間組成，這個過程也被叫做一次擾動過程。以這些葉節(jié)點為中心持續(xù)延伸出新的葉節(jié)點截止到并未有葉節(jié)點產生。可達樹上各節(jié)點能夠實時展現(xiàn)出兩個及以上實體協(xié)議的互動情況。FSM因為容易操作比較直接的狀態(tài)被大幅度的運用到實際中，但是其在實現(xiàn)協(xié)議驗證方面存在諸多不足，一般不適用于復雜的系統(tǒng)。

3.3 基于時序邏輯的協(xié)議驗證與分析

3.3.1 基于模態(tài)邏輯的研究

這種形式的邏輯目前在市場上得到普遍認可的便是在20世紀末期由Burrows M、Abadi M等人發(fā)現(xiàn)的BAN邏輯。BAN邏輯在協(xié)議初始階段便明確了系統(tǒng)之中所有相關的知識和信任，經(jīng)過發(fā)送和接收信息來獲取新的知識，在推導規(guī)則的指引下獲得目標信任和知識[2]。假如最后獲得的語句集不存在目標信任和知識語句時，那么這個協(xié)議極易產生安全危機。由于BAN存在的安全缺陷，后人在此基礎上對其進行了改進，獲得了“類BAN邏輯”成果，并且發(fā)布在IEEE軟件工程雜志之上。在此之中，GNY90、AT91邏輯作為其中的一種形式得到了人們的普遍關注。GNY90對原始的BAN邏輯的范圍進行了延伸，具體界定了消息認定的規(guī)則，比原始的BAN更加的精細化并且覆蓋的范圍也越來越廣。然而其所要遵循的規(guī)則高達50個，制約了其實際應用范圍和空間。AT91邏輯在計算模式以及形式語言方面具備突出性優(yōu)勢，獲得了大眾的認可。在AT91的框架基礎上，20世紀末期類BAN的邏輯實現(xiàn)了統(tǒng)一，也就是形成了SVO邏輯。MB93邏輯因為加入了集合概念并且因為格式化改寫協(xié)議方法的獨特方式引發(fā)了人們的關注。但是本段所述的邏輯形式都不能夠滿足電子商務協(xié)議的需求，這主要是因為信念邏輯必須要在嚴格的證明之下方能夠執(zhí)行造成的。在這種情況下，Kailar發(fā)現(xiàn)了一種新的形式化分析方法，用來分析電子商務中的可追究性，即Kailar邏輯。然而Kailar邏輯在實際中存在不能夠判斷公平性等不足。

3.3.2 基于代數(shù)理論的協(xié)議分析

該方式具備本文分析方式所具有的優(yōu)勢，如精密度高以及具備強大的推理功能等。20世紀90年代初期Meadows等人便運用該方式對NRL分析器的推理模型進行延伸，但是并未取得突出性實效。近期以來，該方面的研究得到了業(yè)界的廣泛關注并且采取了一系列的實際活動，產生了FDR模型檢測器。Bruno Dutertre經(jīng)過長期的研究發(fā)明了PVS驗證系統(tǒng)。此外，基于代數(shù)理論的協(xié)議分析還包括Spi演算分析。但是這種方式在存在一定的安全缺陷，在實際應用中存在一定的局限性。

3.3.3 規(guī)約證明

規(guī)約證明是一種最新被提出的新型的技術，最早被Kemmerer提出。該方式可以實現(xiàn)手動以及自動的自由切換，但是自動證明較之前者還不夠成熟比較復雜，需要更深一步的完善和探索。

4 結 論

為保障網(wǎng)絡通信協(xié)議的可靠性，對其實施有效的驗證顯得尤為重要，本文介紹了能夠在實際中得到有效運用的驗證方式，在實際中可以根據(jù)具體情況進行選擇。唯有如此方能夠確保網(wǎng)絡通信協(xié)議的正常運作，推動整個計算機系統(tǒng)高效工作。