网络协议分析

网络协议分析姓名学号：班级一、实验题目(1)验证数据链路层协议的安全性(2)AB协议(3)GO-BACK-N协议二、实验环境搭载在windows下安装spin，将spin.exe的路径添加到环境变量path中，若电脑有gcc，则直接将其路径写入path，若无则安装Dev-c++，将其内所包含的gcc写入path。然后运行xspin525.tcl，即可启动spin完成实验。三、实验目的1.学习PROMELA语言，并用它描述常见协议并验证。2.练习协议工具spin的使用，并对协议的执行进行模拟。四、编程实现1.数据链路层的协议正确性验证协议条件分为报文应答会出错且丢失，因此信道共有五中形式的信号，即发送的数据信号、ACK信号、NAK信号，丢失信号和出错信号；定义两个信道，用在发送方实体和接收方实体进行数据传送；定义两个进程，分别是发送方进程和接受进程，发送方在接受到错误的信号或ACK序列号不匹配时，进行重传。接收方，收到错误信息时，发送Err，NAK，Mis信号，正确时返回ACK信号。具体程序如下：proctypeSENDER(chanInCh,OutCh){byteSendData;byteSendSeq;byteReceivedSeq;SendData=5-1;do::SendData=(SendData+1)%5;again:if::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!Msg(SendData,SendSeq)::OutCh!Err(0,0)::OutCh!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(chanInCh,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);::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!Ack(ReceivedSeq,0);::OutCh!Err(0,0);ExpectedSeq=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;}init{runSENDER(ReceiverToSender,SenderToReceiver);runRECEIVER(SenderToReceiver,ReceiverToSender);}2.AB协议根据AB协议状态转换图用PROMELA语言进行描述。其中由于S1状态和S3状态发送的信息是一致的，故将两个状态合一。定义两个发送和两个接收进程，分为A发送B接收，B发送A接收。具体程序如下：mtype={Err,a,b};chanSenderToReceiver=[1]of{mtype,byte};chanReceiverToSender=[1]of{mtype,byte};proctypeA_SENDER(chanInCh,OutCh){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(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)-gotoS5::InCh?a(0)-gotoS1::InCh?a(1)-gotoS1fi;S1:if::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)::OutCh!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(1)::OutCh!Err(0)fi;if::InCh?Err(0)-gotoS5::InCh?b(1)-gotoS1::InCh?b(0)-gotoS1fi;}init{atomic{runA_SENDER(ReceiverToSender,SenderToReceiver);runB_RECEIVER(SenderToReceiver,ReceiverToSender);}/*atomic{runB_SENDER(ReceiverToSender,SenderToReceiver);runA_RECEIVER(SenderToReceiver,ReceiverToSender);}*/}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）；（4）如果事件为帧到达，则从物理层接收一个帧，则执行以下步骤。首先检查帧的seq域，若正是期待接收的帧（seq=frame_expected），将帧中携带的分组交给网络层，frame_expected加1；然后检查帧的ack域，若ack落于发送窗口内，表明该序号及其之前所有序号的帧均已正确收到，因此终止这些帧的计时器，修改发送窗口大小及发送窗口下沿值将这些帧去掉，继续执行步骤（7）；（5）如果事件是收到坏帧，继续执行步骤（7）。（6）如果事件是超时，即：next_frame_to_send=ack_expected，从发生超时的帧开始重发发送窗口内的所有帧，后继续执行步骤（7）。（7）若发送窗口大小小于所允许的最大值（MAX-SEQ），则可继续向网络层发送，否则则暂停继续向网络层发送，同时返回互步骤（2）等待。具体程序如下：#defineMaxSeq3#defineWrong(x)x=(x+1)%(MaxSeq)#defineRight(x)x=(x+1)%(MaxSeq+1)#defineinc(x)Right(x)5chanq[2]=[MaxSeq]of{byte,byte};active[2]proctypep5(){byteNextFrame,AckExp,FrameExp,r,s,nbuf,i;chanin,out;in=q[_pid];out=q[1-_pid];xrin;xsout;do::nbufMaxSeq-nbuf++;out!NextFrame,(FrameExp+MaxSeq)%(MaxSeq+1);inc(NextFrame)::q[_pid]?r,s-if::r==FrameExp-printf(MSC:accept%d\n,r)inc(FrameExp)::elsefi;do::((AckExp=s)&&(sNextFrame))||((AckExp=s)&&(NextFrameAckExp))||((sNextFrame)&&(NextFrameAckExp))-nbuf--;inc(AckExp);::else-breakod::timeout-NextFrame=AckExp;printf(MSC:timeout\n);i=1;do::i=nbuf-out!NextFrame,(FrameExp+MaxSeq)%(MaxSeq+1);inc(NextFrame);i++::else-breakod