2022年网络协议分析 .pdf

《2022年网络协议分析 .pdf》由会员分享，可在线阅读，更多相关《2022年网络协议分析 .pdf（15页珍藏版）》请在淘文阁 - 分享文档赚钱的网站上搜索。

1、网络协议分析姓名学号：班级名师资料总结 - - -精品资料欢迎下载 - - - - - - - - - - - - - - - - - - 名师精心整理 - - - - - - - 第 1 页，共 15 页 - - - - - - - - - 一、实验题目(1) 验证数据链路层协议的安全性(2)AB 协议(3)GO-BACK-N协议二、实验环境搭载在 windows 下安装 spin ， 将 spin.exe的路径添加到环境变量path中，若电脑有 gcc，则直接将其路径写入path，若无则安装 Dev-c+，将其内所包含的gcc 写入 path 。然后运行 xspin525.tcl，即可启动

2、spin 完成实验。三、实验目的 1. 学习 PROMELA语言，并用它描述常见协议并验证。 2. 练习协议工具 spin 的使用，并对协议的执行进行模拟。四、编程实现 1.数据链路层的协议正确性验证协议条件分为报文应答会出错且丢失，因此信道共有五中形式的信号，即发送的数据信号、ACK信号、 NAK信号，丢失信号和出错信号；定义两个信道，用在发送方实体和接收方实体进行数据传送；定义两个进程， 分别是发送方进程和接受进程，发送方在接受到错误的信号或 ACK序列号不匹配时，进行重传。接收方，收到错误信息时，发送 Err ，NAK ，Mis 信号，正确时返回ACK信号。具体程序如下：proctype

3、 SENDER(chan InCh,OutCh) 名师资料总结 - - -精品资料欢迎下载 - - - - - - - - - - - - - - - - - - 名师精心整理 - - - - - - - 第 2 页，共 15 页 - - - - - - - - - byte SendData; byte SendSeq; byte ReceivedSeq; SendData=5-1; do :SendData=(SendData+1)%5; again: if :OutCh!Msg(SendData,SendSeq) :OutCh!Msg(SendData,SendSeq) :OutCh!M

4、sg(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; 名师资料总结 - -

5、-精品资料欢迎下载 - - - - - - - - - - - - - - - - - - 名师精心整理 - - - - - - - 第 3 页，共 15 页 - - - - - - - - - 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!=SendS

6、eq)- end2: goto again fi fi; progress: SendSeq=1-SendSeq; od; proctype RECEIVER(chan InCh,OutCh) byte ReceivedData; byte ReceivedSeq; byte ExpectedData; byte ExpectedSeq; do :InCh?Msg(ReceivedData,ReceivedSeq)- if :(ReceivedSeq=ExpectedSeq)- 名师资料总结 - - -精品资料欢迎下载 - - - - - - - - - - - - - - - - - - 名

7、师精心整理 - - - - - - - 第 4 页，共 15 页 - - - - - - - - - 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(Receiv

8、edSeq,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!=Expect

9、edSeq)- 名师资料总结 - - -精品资料欢迎下载 - - - - - - - - - - - - - - - - - - 名师精心整理 - - - - - - - 第 5 页，共 15 页 - - - - - - - - - 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,SenderToRece

10、iver); run RECEIVER(SenderToReceiver,ReceiverToSender); 2.AB 协议根据 AB协议状态转换图用PROMELA 语言进行描述。其中由于S1状态和 S3状态发送的信息是一致的，故将两个状态合一。定义两个发送和两个接收进程，分为A发送 B接收，B发送 A接收。具体程序如下：名师资料总结 - - -精品资料欢迎下载 - - - - - - - - - - - - - - - - - - 名师精心整理 - - - - - - - 第 6 页，共 15 页 - - - - - - - - - mtype = Err,a,b; chan Sender

11、ToReceiver = 1 of mtype,byte; chan ReceiverToSender = 1 of mtype,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 S1 fi; S1: if :OutCh!a(1) :OutCh!Err(0) fi; if :InCh?Err(0)- goto S5 名师资料总结 - - -精品资料欢迎下载 - -

12、- - - - - - - - - - - - - - - - 名师精心整理 - - - - - - - 第 7 页，共 15 页 - - - - - - - - - :InCh? b(1)- goto S1 :InCh?b(0)- goto S1 fi; proctype B_RECEIVER(chan InCh, OutCh) if :InCh?Err(0)- goto S5 :InCh?a(0) - goto S1 :InCh?a(1)- goto S1 fi; S5: if :OutCh!b(0) :OutCh!Err(0) fi; if :InCh?Err(0)- goto S5 :

13、InCh?a(0) - goto S1 :InCh?a(1)- goto S1 fi; S1: if 名师资料总结 - - -精品资料欢迎下载 - - - - - - - - - - - - - - - - - - 名师精心整理 - - - - - - - 第 8 页，共 15 页 - - - - - - - - - :OutCh!b(1) :OutCh!Err(0) fi; if :InCh?Err(0)- goto S5 :InCh?a(1)- goto S1 :InCh?a(0)- goto S1 fi; proctype B_SENDER(chan InCh, OutCh) S5: i

14、f :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 名师资料总结 - - -精品资料欢迎下载 - - - - - - - - - - - - - - - - - - 名师精心整理 - - - - - - - 第 9 页，共 15 页 - - - - - - - - - :OutCh!b(1) :OutCh!Err(0) fi; if :InCh?Err(0)- goto S5 :InCh?a(1)- goto S1 :InCh?a

15、(0)- goto S1 fi; proctype A_RECEIVER(chan InCh, OutCh) if :InCh?Err(0)- goto S5 :InCh?b(0)- goto S1 :InCh?b(1)- goto S1 fi; S5: if :OutCh!a(0) :OutCh!Err(0) fi; if 名师资料总结 - - -精品资料欢迎下载 - - - - - - - - - - - - - - - - - - 名师精心整理 - - - - - - - 第 10 页，共 15 页 - - - - - - - - - :InCh?Err(0)- goto S5 :InC

16、h?b(0)- goto S1 :InCh?b(1)- goto S1 fi; S1: if :OutCh!a(1) :OutCh!Err(0) fi; if :InCh?Err(0)- goto S5 :InCh? b(1)- goto S1 :InCh?b(0)- goto S1 fi; init atomic run A_SENDER(ReceiverToSender,SenderToReceiver); run B_RECEIVER(SenderToReceiver, ReceiverToSender); 名师资料总结 - - -精品资料欢迎下载 - - - - - - - - - -

17、 - - - - - - - - 名师精心整理 - - - - - - - 第 11 页，共 15 页 - - - - - - - - - /* atomic run B_SENDER(ReceiverToSender,SenderToReceiver); run A_RECEIVER(SenderToReceiver, ReceiverToSender); */ 3.GO-BACK-N协议（1）初始化。开网络层允许； ack_expected = 0（此时处于发送窗口的下沿）； next_frame_to_send = 0，frame_expected = 0（初始化正在发送的帧和期待的帧序

18、号）； nbuffered = 0（进行发送窗口大小初始化）；（2）等待事件发生（网络层准备好，帧到达，收到坏帧，超时）。（3）如果事件为网络层准备好，则执行以下步骤。从网络层接收一个分组，放入相应的缓冲区；发送窗口大小加1 ； 使 用 缓 冲 区 中 的 数 据 分 组 、 next_frame_to_send和frame_expected 构造帧，继续发送； next_frame_to_send加 1；跳转（7）；（4）如果事件为帧到达，则从物理层接收一个帧，则执行以下步骤。名师资料总结 - - -精品资料欢迎下载 - - - - - - - - - - - - - - - - - - 名

19、师精心整理 - - - - - - - 第 12 页，共 15 页 - - - - - - - - - 首先检查帧的 seq 域， 若正是期待接收的帧（seq = frame_expected ） ，将帧中携带的分组交给网络层，frame_expected 加 1；然后检查帧的 ack 域，若 ack 落于发送窗口内， 表明该序号及其之前所有序号的帧均已正确收到， 因此终止这些帧的计时器， 修改发送窗口大小及发送窗口下沿值将这些帧去掉，继续执行步骤（7）；（5）如果事件是收到坏帧，继续执行步骤（7）。（6）如果事件是超时，即： next_frame_to_send = ack_expected

20、，从发生超时的帧开始重发发送窗口内的所有帧，后继续执行步骤（7） 。（7）若发送窗口大小小于所允许的最大值（MAX-SEQ），则可继续向网络层发送，否则则暂停继续向网络层发送，同时返回互步骤（2）等待。具体程序如下：#define MaxSeq 3 #define Wrong(x) x = (x+1) % (MaxSeq) #define Right(x) x = (x+1) % (MaxSeq + 1) #define inc(x) Right(x) 5 chan q2 = MaxSeq of byte, byte ; active 2 proctype p5() 名师资料总结 - - -精

21、品资料欢迎下载 - - - - - - - - - - - - - - - - - - 名师精心整理 - - - - - - - 第 13 页，共 15 页 - - - - - - - - - byte NextFrame, AckExp, FrameExp, r, s, nbuf, i; chan in, out; in = q_pid; out = q1-_pid; xr in; xs out; do : nbuf nbuf+; out!NextFrame , (FrameExp + MaxSeq) % (MaxSeq + 1); inc(NextFrame) : q_pid?r,s -

22、if : r = FrameExp - printf(MSC: accept %dn, r) inc(FrameExp) : else fi; do : (AckExp = s) & (s NextFrame)|(AckExp = s) & (NextFrame AckExp)|(s NextFrame) & (NextFrame nbuf-; 名师资料总结 - - -精品资料欢迎下载 - - - - - - - - - - - - - - - - - - 名师精心整理 - - - - - - - 第 14 页，共 15 页 - - - - - - - - - inc(AckExp); : else - break od : timeout - NextFrame = AckExp; printf(MSC: timeoutn); i = 1; do : i out!NextFrame , (FrameExp + MaxSeq) % (MaxSeq + 1); inc(NextFrame); i+ : else - break od 名师资料总结 - - -精品资料欢迎下载 - - - - - - - - - - - - - - - - - - 名师精心整理 - - - - - - - 第 15 页，共 15 页 - - - - - - - - -