网络协议分析
姓名
学号：
班级
一、实验题目
(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
{