网络协议分析 姓名 学号： 班级 一、实验题目 (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信号。具体程序如下：

proctype SENDER(chan InCh,OutCh) { 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!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 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)-> 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.AB协议 根据AB协议状态转换图用PROMELA语言进行描述。其中由于S1状态和S3状态发送的信息是一致的，故将两个状态合一。定义两个发送和两个接收进程，分为A发送B接收，B发送A接收。具体程序如下：

mtype = {Err,a,b};

chan SenderToReceiver = [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 ::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 ::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 S1 fi; }

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 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 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 ::InCh?Err(0)-> goto S5 ::InCh?b(0)-> goto S1 ::InCh?b(1)-> goto S1 fi; S1: if