网络协议分析
姓名
学号：
班级
一、实验题目
(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
::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);
}
/* 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（初始化正在发送的帧和期待的帧序号）；
nbuffered = 0（进行发送窗口大小初始化）；
（2）等待事件发生（网络层准备好，帧到达，收到坏帧，超时）。
（3）（3）如果事件为网络层准备好，则执行以下步骤。
（4） 从网络层接收一个分组，放入相应的缓冲区；发送窗口大小加1；使用缓冲区中的数据分组、next_frame_to_send和 frame_expected构造帧，继续发送；next_frame_to_send加1；跳转（7）；
（5）（4）如果事件为帧到达，则从物理层接收一个帧，则执行以下步骤。
（6）首先检查帧的seq域，若正是期待接收的帧（seq = frame_expected），将帧中携带的分组交给网络层，frame_expected加1；
（7）然后检查帧的ack域，若ack落于发送窗口内，表明该序号及其之前所有序号的帧均已正确收到，因此终止这些帧的计时器，修改发送窗口大小及发送窗口下沿值将这些帧去掉，继续执行步骤（7）；
（8）（5）如果事件是收到坏帧，继续执行步骤（7）。
（9）（6）如果事件是超时，即：next_frame_to_send = ack_expected，从发生超时的帧开始重发发送窗口内的所有帧，后继续执行步骤（7）。
（10）（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 q[2] = [MaxSeq] of { byte, byte };
active [2] proctype p5()
{
byte NextFrame, AckExp, FrameExp, r, s, nbuf, i;
chan in, out;
in = q[_pid];
out = q[1-_pid];
xr in; xs out;
do
:: nbuf < MaxSeq ->
nbuf++;
out!NextFrame , (FrameExp + MaxSeq) % (MaxSeq + 1);
inc(NextFrame)
:: q[_pid]?r,s ->
if
:: r == FrameExp ->
printf(\"MSC: accept %d\\n\
inc(FrameExp)
:: else
fi;
do
:: ((AckExp <= s) && (s < NextFrame))||((AckExp <= s) && (NextFrame < AckExp))||((s < NextFrame) && (NextFrame < AckExp)) ->nbuf--;
inc(AckExp);
:: else -> break
od
:: timeout ->
NextFrame = AckExp;
printf(\"MSC: timeout\\n\");
i = 1;
do
:: i <= nbuf ->
out!NextFrame , (FrameExp + MaxSeq) % (MaxSeq + 1);
inc(NextFrame);
i++
:: else -> break
od
