网络协议分析

1、网络协议分析姓名学号:班级、实验题目(1) 验证数据链路层协议的安全性(2)AB协议(3)GO-BACK-NB议二、实验环境搭载在windows下安装spin，将spin.exe的路径添加到环境变量path中，若电脑有gcc，则直接将其路径写入path，若无则安装Dev-c+，将其内所包含的gcc写入path。然后运行xspin525.tcl，即可启动spin完成实验。三、实验目的1 .学习PROMELA言，并用它描述常见协议并验证。2 .练习协议工具spin的使用，并对协议的执行进行模拟。四、编程实现1.数据链路层的协议正确性验证协议条件分为报文应答会出错且丢失，因此信道共有五中形式的信号，

2、即发送的数据信号、ACK言号、NAK信号，丢失信号和出错信号；定义两个信道，用在发送方实体和接收方实体进行数据传送；定义两个进程，分别是发送方进程和接受进程，发送方在接受到错误的信号或ACKff列号不匹配时，进行重传。接收方，收到错误信息时，发送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协议根据AB协议状态转换图用PROMEL语言进行描述。其中由于S1状态和S3状态发送的信息是一致的，故将两个状态合一。定义两个发送和两个接收进程，分为A发送B接收，B发送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协议（1）初始化。开网络层允许；ack_expected=0（此时处于发送窗口的下沿）；next_frame_to_send=0，frame_expected=0（初始化正在发送的帧和期待的帧序号）；nbuffered=0（进行发送窗口大小初始化）；（2）等待事件发生（网络层准备好，帧到达，收到坏帧，超时）。（3）如果事件为网络层准备好，则执行以下步骤。从网络层接收一个分组，放入相应的缓冲区；发送窗口大小加1；使用缓冲区中的数据分组、next_frame_to_send和frame_expected构造帧，继续发送；next_frame_to_send加1；跳转（7）；

14、（4）如果事件为帧到达，则从物理层接收一个帧，则执行以下步骤。首先检查帧的seq域，若正是期待接收的帧(seq=frame_expected)，将帧中携带的分组交给网络层，frame_expected加1；然后检查帧的ack域，若ack落于发送窗口内，表明该序号及其之前所有序号的帧均已正确收到，因此终止这些帧的计时器，修改发送窗口大小及发送窗口下沿值将这些帧去掉，继续执行步骤(7)；(5)如果事件是收到坏帧，继续执行步骤(7)。(6)如果事件是超时，即：next_frame_to_send=ack_expected，从发生超时的帧开始重发发送窗口内的所有帧，后继续执行步骤(7)。(7)若发送窗

15、口大小小于所允许的最大值(MAX-SEQ,则可继续向网络层发送，否则则暂停继续向网络层发送，同时返回互步骤(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)