网络协议分析样本.doc

网络协议分析样本 网络协议分析本文档所提供的信息仅供参考之用，不能作为科学依据，请勿模仿。 文档如有不当之处，请联系本人或网站删除。 网络协议分析姓名学号:班级本文档所提供的信息仅供参考之用，不能作为科学依据，请勿模仿。 文档如有不当之处，请联系本人或网站删除。 一、实验题目 (1)验证数据链路层协议的安全性B (2)AB协议 (3)GO-BACK-N N协议 二、实验环境搭载在在s windows装下安装spin有，若电脑有g，则直接将其路径写入path，若无则安装Dev-c+，将其内所包含的c g写入path。 ，即可启动n spin完成实验。 三、实验目的，并用它描述常见协议并验证。 ，并对协议的执行进行模拟。 四、编程实现本文档所提供的信息仅供参考之用，不能作为科学依据，请勿模仿。 文档如有不当之处，请联系本人或网站删除。 协议条件分为报文应答会出错且丢失，因此信道共有五中形式的信号，即发送的数据信号、K ACK信号、K NAK信号，丢失信号和出错信号；定义两个信道，用在发送方实体和接收方实体进行数据传送；定义两个进程，分别是发送方进程和接受进程，发送方在接受到错误的信号或A AKCK序列号不匹配时，进行重传。 接收方，收到错误信息时，发送Err，NAK，s Mis信号，正确时返回K ACK信号。 具体程序如下:proctype SENDER(chan InCh,OutCh)byte SendData;byte SendSeq;byte ReceivedSeq;SendData=5-1;do:SendData=(SendData+1)%5;again:if:OutCh!Msg(SendData,SendSe q):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-goto again:InCh?Mis(0,0)-goto again:InCh?Err(0,0)-goto again:InCh?Nak(ReceivedSeq,0)-goto again本文档所提供的信息仅供参考之用，不能作为科学依据，请勿模仿。 文档如有不当之处，请联系本人或网站删除。 :InCh?Ack(ReceivedSeq,0)-if:(ReceivedSeq=SendSeq)-goto progress:(ReceivedSeq!=SendSeq)-end2:goto againfi fi;progress:SendSeq=1-SendSeq;od;proctyp eRECEIVER(chan InCh,OutCh)byte ReceivedData;byte ReceivedSeq;byte ExpectedData;byte ExpectedSeq;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);fi fi:InCh?Err(0,0)-OutCh!Nak(ReceivedSeq,0);:InCh?Mis(0,0)-skip;od;init本文档所提供的信息仅供参考之用，不能作为科学依据，请勿模仿。 文档如有不当之处，请联系本人或网站删除。 run SENDER(ReceiverToSender,SenderToReceiver);run RECEIVER(SenderToReceiver,ReceiverToSender);2.B AB协议根据据B AB协议状态转换图用A PROMELA语言进行描述。 其中由于1S1状态和3S3状态发送的信息是一致的，故将两个状态合一。 定义两个发送和两个接收进程，分为A A发送B B接收，B B发送A A接收。 具体程序如下:mtype=Err,a,b;chan SenderToReceiver=1ofmtype,byte;chan ReceiverToSender=1ofmtype,byte;proctype A_SENDER(chan InCh,OutCh)S5:if本文档所提供的信息仅供参考之用，不能作为科学依据，请勿模仿。 文档如有不当之处，请联系本人或网站删除。 :OutCh!a (0):OutCh!Err (0)fi;if:InCh?Err (0)-goto S5:InCh?b (0)-goto S1:InCh?b (1)-goto S1fi;S1:if:OutCh!a (1):OutCh!Err (0)fi;if:InCh?Err (0)-goto S5:InCh?b (1)-goto S1:InCh?b (0)-goto S1fi;本文档所提供的信息仅供参考之用，不能作为科学依据，请勿模仿。 文档如有不当之处，请联系本人或网站删除。 proctype B_RECEIVER(chan InCh,OutCh)if:InCh?Err (0)-goto S5:InCh?a (0)-goto S1:InCh?a (1)-goto S1fi;S5:if:OutCh!b (0):OutCh!Err (0)fi;if:InCh?Err (0)-goto S5:InCh?a (0)-goto S1:InCh?a (1)-goto S1本文档所提供的信息仅供参考之用，不能作为科学依据，请勿模仿。 文档如有不当之处，请联系本人或网站删除。 fi;S1:if:OutCh!b (1):OutCh!Err (0)fi;if:InCh?Err (0)-goto S5:InCh?a (1)-goto S1:InCh?a (0)-goto S1fi;proctype B_SENDER(chan InCh,OutCh)S5:if:OutCh!b (0):OutCh!Err (0)本文档所提供的信息仅供参考之用，不能作为科学依据，请勿模仿。 文档如有不当之处，请联系本人或网站删除。 fi;if:InCh?Err (0)-goto S5:InCh?a (0)-goto S1:InCh?a (1)-goto S1fi;S1:if:OutCh!b (1):OutCh!Err (0)fi;if:InCh?Err (0)-goto S5:InCh?a (1)-goto S1:InCh?a (0)-goto S1fi;本文档所提供的信息仅供参考之用，不能作为科学依据，请勿模仿。 文档如有不当之处，请联系本人或网站删除。 proctype A_RECEIVER(chan InCh,OutCh)if:InCh?Err (0)-goto S5:InCh?b (0)-goto S1:InCh?b (1)-goto S1fi;S5:if:OutCh!a (0):OutCh!Err (0)fi;if:InCh?Err (0)-goto S5:InCh?b (0)-goto S1:InCh?b (1)-goto S1fi;S1:if本文档所提供的信息仅供参考之用，不能作为科学依据，请勿模仿。 文档如有不当之处，请联系本人或网站删除。 :OutCh!a (1):OutCh!Err (0)fi;if:InCh?Err (0)-goto S5:InCh?b (1)-goto S1:InCh?b (0)-goto S1fi;initatomicrun A_SENDER(ReceiverToSender,SenderToReceiver);run B_RECEIVER(SenderToReceiver,ReceiverToSender);本文档所提供的信息仅供参考之用，不能作为科学依据，请勿模仿。 文档如有不当之处，请联系本人或网站删除。 /*atomicrun B_SENDER(ReceiverToSender,SenderToReceiver);run A_RECEIVER(SenderToReceiver,ReceiverToSender);*/ （11）初始化。 开网络层允许；ack_expected=0（此时处于发送窗口的下沿）；next_frame_to_send=0，frame_expected=0（初始化正在发送的帧和期待的帧序号）；nbuffered=0（进行发送窗口大小初始化）； （22）等待事件发生（网络层准备好，帧到达，收到坏帧，超时）。 （33）如果事件为网络层准备好，则执行以下步骤。 从网络层接收一个分组，放入相应的缓冲区；发送窗口大小加11；使用缓冲区中的数据分组、next_frame_to_send和本文档所提供的信息仅供参考之用，不能作为科学依据，请勿模仿。 文档如有不当之处，请联系本人或网站删除。 d frame_expected构造帧，继续发送；d next_frame_to_send加加11；跳转 （77）；（44。 ）如果事件为帧到达，则从物理层接收一个帧，则执行以下步骤。 首先检查帧的q seq域，若正是期待接收的帧（seq=frame_expected），将帧中携带的分组交给网络层，d frame_expected加加11；然后检查帧的k ack域，若k ack落于发送窗口内，表明该序号及其之前所有序号的帧均已正确收到，因此终止这些帧的计时器，修改发送窗口大小及发送窗口下沿值将这些帧去掉，继续执行步骤 （77）； （55）如果事件是收到坏帧，继续执行步骤 （77）。 （66）如果事件是超时，即:next_frame_to_send=ack_expected，从发生超时的帧开始重发发送窗口内的所有帧，后继续执行步骤（77。 ）。 （77）若发送窗口大小小于所允许的最大值（MAX-SEQ），则可继续向网络层发送，否则则暂停继续向网络层发送，同时返回互步骤 （22）等待。 具体程序如下:#define MaxSeq33#define Wrong(x)x=(x+1)%(MaxSeq)#define Right(x)x=(x+1)%(MaxSeq+1)本文档所提供的信息仅供参考之用，不能作为科学依据，请勿模仿。 文档如有不当之处，请联系本人或网站删除。 #de fineinc(x)Right(x)55chan q2=MaxSeqofbyte,byte;active2proctype p5()byte NextFrame,AckExp,FrameExp,r,s,nbuf,i;chan in,out;in=q_pid;out=q1-_pid;xr in;xs out;do:nbufnbuf+;out!NextF rame,(FrameExp+MaxSeq)%(MaxSeq+1);inc(NextFrame):q_pid?r,s-本文档所提供的信息仅供参考之用，不能作为科学依据，请勿模仿。