網(wǎng)絡(luò)協(xié)議分析

1、網(wǎng)絡(luò)協(xié)議分析姓名學(xué)號:班級、實(shí)驗(yàn)題目(1) 驗(yàn)證數(shù)據(jù)鏈路層協(xié)議的安全性(2)AB協(xié)議(3)GO-BACK-NB議二、實(shí)驗(yàn)環(huán)境搭載在windows下安裝spin，將spin.exe的路徑添加到環(huán)境變量path中，若電腦有g(shù)cc，則直接將其路徑寫入path，若無則安裝Dev-c+，將其內(nèi)所包含的gcc寫入path。然后運(yùn)行xspin525.tcl，即可啟動spin完成實(shí)驗(yàn)。三、實(shí)驗(yàn)?zāi)康? .學(xué)習(xí)PROMELA言，并用它描述常見協(xié)議并驗(yàn)證。2 .練習(xí)協(xié)議工具spin的使用，并對協(xié)議的執(zhí)行進(jìn)行模擬。四、編程實(shí)現(xiàn)1.數(shù)據(jù)鏈路層的協(xié)議正確性驗(yàn)證協(xié)議條件分為報(bào)文應(yīng)答會出錯且丟失，因此信道共有五中形式的信號，

2、即發(fā)送的數(shù)據(jù)信號、ACK言號、NAK信號，丟失信號和出錯信號；定義兩個信道，用在發(fā)送方實(shí)體和接收方實(shí)體進(jìn)行數(shù)據(jù)傳送；定義兩個進(jìn)程，分別是發(fā)送方進(jìn)程和接受進(jìn)程，發(fā)送方在接受到錯誤的信號或ACKff列號不匹配時，進(jìn)行重傳。接收方，收到錯誤信息時，發(fā)送Err,NAKMis信號，正確時返回ACK言號。具體程序如下：proctypeSENDER(chanInCh,OutCh)byteSendData;byteSendSeq;byteReceivedSeq;SendData=5-1;do:SendData=(SendData+1)%5;again:if:OutCh!Msg(SendData,SendSeq

3、):OutCh!Msg(SendData,SendSeq):OutCh!Msg(SendData,SendSeq):OutCh!Msg(SendData,SendSeq):OutCh!Msg(SendData,SendSeq):OutCh!Msg(SendData,SendSeq):OutCh!Msg(SendData,SendSeq):OutCh!Msg(SendData,SendSeq):OutCh!Msg(SendData,SendSeq):OutCh!Msg(SendData,SendSeq):OutCh!Msg(SendData,SendSeq):OutCh!Err(0,0):Out

4、Ch!Mis(0,0)fi;if:timeout->gotoagain:InCh?Mis(0,0)->gotoagain:InCh?Err(0,0)->gotoagain:InCh?Nak(ReceivedSeq,0)->gotoagain:InCh?Ack(ReceivedSeq,0)->if:(ReceivedSeq=SendSeq)->gotoprogress:(ReceivedSeq!=SendSeq)->end2:gotoagainfifi;progress:SendSeq=1-SendSeq;od;proctypeRECEIVER(chan

5、InCh,OutCh)byteReceivedData;byteReceivedSeq;byteExpectedData;byteExpectedSeq;do:InCh?Msg(ReceivedData,ReceivedSeq)->if:(ReceivedSeq=ExpectedSeq)->assert(ReceivedData=ExpectedData);progress:ExpectedSeq=1-ExpectedSeq;ExpectedData=(ExpectedData+1)%5;if:OutCh!Mis(0,0):OutCh!Ack(ReceivedSeq,0);:Out

6、Ch!Ack(ReceivedSeq,0);:OutCh!Ack(ReceivedSeq,0);:OutCh!Ack(ReceivedSeq,0);:OutCh!Ack(ReceivedSeq,0);:OutCh!Ack(ReceivedSeq,0);:OutCh!Ack(ReceivedSeq,0);:OutCh!Ack(ReceivedSeq,0);:OutCh!Ack(ReceivedSeq,0);:OutCh!Ack(ReceivedSeq,0);:OutCh!Ack(ReceivedSeq,0);:OutCh!Ack(ReceivedSeq,0);:OutCh!Err(0,0);Ex

7、pectedSeq=1-ExpectedSeq;ExpectedData=(ExpectedData+4)%5;fi:(ReceivedSeq!=ExpectedSeq)->if:OutCh!Mis(0,0);:OutCh!Nak(ReceivedSeq,0);:OutCh!Err(0,0);fifi:InCh?Err(0,0)->OutCh!Nak(ReceivedSeq,0);:InCh?Mis(0,0)->skip;od;initrunSENDER(ReceiverToSender,SenderToReceiver);runRECEIVER(SenderToReceiv

8、er,ReceiverToSender);2.AB協(xié)議根據(jù)AB協(xié)議狀態(tài)轉(zhuǎn)換圖用PROMEL語言進(jìn)行描述。其中由于S1狀態(tài)和S3狀態(tài)發(fā)送的信息是一致的，故將兩個狀態(tài)合一。定義兩個發(fā)送和兩個接收進(jìn)程，分為A發(fā)送B接收，B發(fā)送A接收。具體程序如下：mtype=Err,a,b;chanSenderToReceiver=1ofmtype,byte;chanReceiverToSender=1ofmtype,byte;proctypeA_SENDER(chanInCh,OutCh)S5:if:OutCh!a(0):OutCh!Err(0)fi;if:InCh?Err(0)->gotoS5:InCh?

9、b(0)->gotoS1:InCh?b(1)->gotoS1fi;S1:if:OutCh!a(1):OutCh!Err(0)fi;if:InCh?Err(0)->gotoS5:InCh?b(1)->gotoS1:InCh?b(0)->gotoS1fi;proctypeB_RECEIVER(chanInCh,OutCh)if:InCh?Err(0)->gotoS5:InCh?a(0)->gotoS1:InCh?a(1)->gotoS1fi;S5:if:OutCh!b(0):OutCh!Err(0)fi;if:InCh?Err(0)->goto

10、S5:InCh?a(0)->gotoS1:InCh?a(1)->gotoS1fi;:OutCh!b(1):OutCh!Err(0)fi;if:InCh?Err(0)->gotoS5:InCh?a(1)->gotoS1:InCh?a(0)->gotoS1fi;proctypeB_SENDER(chanInCh,OutCh)S5:if:OutCh!b(0):OutCh!Err(0)fi;if:InCh?Err(0)->gotoS5:InCh?a(0)->gotoS1:InCh?a(1)->gotoS1fi;S1: if:OutCh!b(1):OutC

11、h!Err(0)fi;if:InCh?Err(0)->gotoS5:InCh?a(1)->gotoS1:InCh?a(0)->gotoS1fi;proctypeA_RECEIVER(chanInCh,OutCh)if:InCh?Err(0)->gotoS5:InCh?b(0)->gotoS1:InCh?b(1)->gotoS1fi;S5:if:OutCh!a(0):OutCh!Err(0)fi;if:InCh?Err(0)->gotoS5:InCh?b(0)->gotoS1:InCh?b(1)->gotoS1fi;S1:if:OutCh!a

12、(1):OutCh!Err(0)fi;if:InCh?Err(0)->gotoS5:InCh?b(1)->gotoS1:InCh?b(0)->gotoS1fi;initatomicrunA_SENDER(ReceiverToSender,SenderToReceiver);runB_RECEIVER(SenderToReceiver,ReceiverToSender);/*atomicrunB_SENDER(ReceiverToSender,SenderToReceiver);runA_RECEIVER(SenderToReceiver,ReceiverToSender);*

13、/3.GO-BACK-N協(xié)議（1）初始化。開網(wǎng)絡(luò)層允許；ack_expected=0（此時處于發(fā)送窗口的下沿）；next_frame_to_send=0，frame_expected=0（初始化正在發(fā)送的幀和期待的幀序號）；nbuffered=0（進(jìn)行發(fā)送窗口大小初始化）；（2）等待事件發(fā)生（網(wǎng)絡(luò)層準(zhǔn)備好，幀到達(dá)，收到壞幀，超時）。（3）如果事件為網(wǎng)絡(luò)層準(zhǔn)備好，則執(zhí)行以下步驟。從網(wǎng)絡(luò)層接收一個分組，放入相應(yīng)的緩沖區(qū)；發(fā)送窗口大小加1；使用緩沖區(qū)中的數(shù)據(jù)分組、next_frame_to_send和frame_expected構(gòu)造幀，繼續(xù)發(fā)送；next_frame_to_send加1；跳轉(zhuǎn)（7）；

14、（4）如果事件為幀到達(dá)，則從物理層接收一個幀，則執(zhí)行以下步驟。首先檢查幀的seq域，若正是期待接收的幀(seq=frame_expected)，將幀中攜帶的分組交給網(wǎng)絡(luò)層，frame_expected加1；然后檢查幀的ack域，若ack落于發(fā)送窗口內(nèi)，表明該序號及其之前所有序號的幀均已正確收到，因此終止這些幀的計(jì)時器，修改發(fā)送窗口大小及發(fā)送窗口下沿值將這些幀去掉，繼續(xù)執(zhí)行步驟(7)；(5)如果事件是收到壞幀，繼續(xù)執(zhí)行步驟(7)。(6)如果事件是超時，即：next_frame_to_send=ack_expected，從發(fā)生超時的幀開始重發(fā)發(fā)送窗口內(nèi)的所有幀，后繼續(xù)執(zhí)行步驟(7)。(7)若發(fā)送窗

15、口大小小于所允許的最大值(MAX-SEQ,則可繼續(xù)向網(wǎng)絡(luò)層發(fā)送，否則則暫停繼續(xù)向網(wǎng)絡(luò)層發(fā)送，同時返回互步驟(2)等待。具體程序如下：#defineMaxSeq3#defineWrong(x)x=(x+1)%(MaxSeq)#defineRight(x)x=(x+1)%(MaxSeq+1)#defineinc(x)Right(x)5chanq2=MaxSeqofbyte,byte;active2proctypep5()byteNextFrame,AckExp,FrameExp,r,s,nbuf,i;chanin,out;in=q_pid;out=q1-_pid;xrin;xsout;do:nbuf<MaxSeq->nbuf+;out!NextFrame,(FrameExp+MaxSeq)%(MaxSeq+1);inc(NextFrame):q_pid?r,s->if:r=FrameExp->printf("MSC:accept%dn",r)inc(FrameExp):elsefi;do:(AckExp<=s)&&(s<NextFrame)|(AckExp<=s)&&(NextFrame<AckExp)