计算机网络通信协议验证技术的有机运用

王文韬

（湖北科技学院，湖北 咸宁 437100）

1 计算机网络通信协议的相关概述

1.1 计算机网络协议的定义

计算机网络协议的本质就是计算机必须遵从的通信规则。网络协议在制定的过程中必须要严格按照标准的体系结构执行，在科学技术不断的发展之中网络通信标准体系也不断更新和完善，如今最为常用的标准为TCP/IP协议组以及ISO两种标准。通信技术的顺利实施就必须要保障其中所有的内容完全遵从于统一的信息交换准则[1]。

1.2 计算机网络协议的特性

计算机网络协议主要包含如下特性。（1）活动性，在实际中通常表现为进展性和终止性，假如网络协议不具备这两种特性，那么他的活动性也是不存在的。（2）安全性。安全性主要是指协议在执行时发生活锁和死锁等安全问题。例如，出现死锁现象时，网络协议所有的实体都呈现等待状态，唯有发生“某一事件”之后方能够执行下一环节的操作。但是，在现实之中便是当网络协议处于这种等待情况时，是不可能发生“某一事件”的，也就是说协议处于死锁状态之后便不可能通过某一事件解脱。这就类似于网络协议一直在接受一个重复的循环命令，然而其又没有办法接受相关的确认信息，因此一直处于一个固定的状态。（3）有界性、完整性以及同步性。工作人员要重点检测网络协议中的成分和参数，还要针对协议之中有无未解决的问题以及非期待的命令等进行检验和检测。在此期间，假如协议出现无错的情况，是否可以保障协议重新开始并且顺利运行下去，这些都是需要重点观察的部分。

2 计算机网络通信协议的主要类型

2.1 局域网使用的通信协议

TCP/IP作为互联网最基础的协议，是局域网运用最广泛的通信协议，其具备高度的灵活性，可以实现众多服务器以及工作站的连接。TCP/IP协议经过其带有的IP地址来对网络中的详细位置以及身份给予高效识别[2]。IP地址主要包含如下要素，即节点和网络ID。在多网段的背景之下能够扩展网络ID，通过子网掩码管理子网。在连接异种网络时，人们普遍以一个翻译者的身份设置网关达到精确翻译通信协议的目的，实现网络相互通信的效果。

2.2 广域网使用的通信协议

广域网的通信协议存在多种多样的形式，包含点到点协议等。广域网协议从本质上讲就是对不同广域网介质上的通信进行了明确的界定。

2.3 路由器选择协议

路由器选择协议主要工作区间为网络层，其实现了路径选择和交换。路由器选择协议主要包含内部路由协议和外部路由协议两种，前者是在系统内部实现路由协议的交换，后者实现不同自治系统的协议互换。

3 验证技术在计算机网络通信协议中的主要应用

3.1 Ping程序在网络协议中的应用

Ping程序的作用是实施对一帧数据的检测工作，即计算机进行数据转换所需要的时间。假如计算机网络在正常运行时突然产生问题，ping程序能够帮助工作人员迅速辨别问题产生的原因。Ping程序的成功执行只是为主机与目标主机的连接提供一条成物理路径并且给予一些相关的参数。例如，-n可以依赖于自身的力量明确地向目标主机发送数据帧数。

3.2 基于有限状态自动机模型的协议验证与分析

形式描述技术中一个关键性的形式便是有限状态机FSM，在FDT中扮演了十分重要的角色。可达性分析技术是目前有限状态机运用最为广泛的一项技术[1]。 其力图对协议的可达状态进行检测。可达性分析关键性环节便是产生和检查可达图，检测协议是否正确，其中包含3个核心技术：首先是寻找全部的可达图并且建立可达图；其次是检验协议的正确性；最后是处理状态爆炸现象。普遍来看，所有的转变都能够经过运用系统全局状态达到明确特性的目的，类似于表明此时是不是死锁状态，全部的实体能不能够接收报文等。基于FSM描述的协议验证主要是借助于可达树来发挥作用。其中系统的初始状态为可达树的根。从初始状态开始将全部的转移列举出来，可达数的一个叶节点便是由这些转移的状态空间组成，这个过程也被叫做一次扰动过程。以这些叶节点为中心持续延伸出新的叶节点截止到并未有叶节点产生。可达树上各节点能够实时展现出两个及以上实体协议的互动情况。FSM因为容易操作比较直接的状态被大幅度的运用到实际中，但是其在实现协议验证方面存在诸多不足，一般不适用于复杂的系统。

3.3 基于时序逻辑的协议验证与分析

3.3.1 基于模态逻辑的研究

这种形式的逻辑目前在市场上得到普遍认可的便是在20世纪末期由Burrows M、Abadi M等人发现的BAN逻辑。BAN逻辑在协议初始阶段便明确了系统之中所有相关的知识和信任，经过发送和接收信息来获取新的知识，在推导规则的指引下获得目标信任和知识[2]。假如最后获得的语句集不存在目标信任和知识语句时，那么这个协议极易产生安全危机。由于BAN存在的安全缺陷，后人在此基础上对其进行了改进，获得了“类BAN逻辑”成果，并且发布在IEEE软件工程杂志之上。在此之中，GNY90、AT91逻辑作为其中的一种形式得到了人们的普遍关注。GNY90对原始的BAN逻辑的范围进行了延伸，具体界定了消息认定的规则，比原始的BAN更加的精细化并且覆盖的范围也越来越广。然而其所要遵循的规则高达50个，制约了其实际应用范围和空间。AT91逻辑在计算模式以及形式语言方面具备突出性优势，获得了大众的认可。在AT91的框架基础上，20世纪末期类BAN的逻辑实现了统一，也就是形成了SVO逻辑。MB93逻辑因为加入了集合概念并且因为格式化改写协议方法的独特方式引发了人们的关注。但是本段所述的逻辑形式都不能够满足电子商务协议的需求，这主要是因为信念逻辑必须要在严格的证明之下方能够执行造成的。在这种情况下，Kailar发现了一种新的形式化分析方法，用来分析电子商务中的可追究性，即Kailar逻辑。然而Kailar逻辑在实际中存在不能够判断公平性等不足。

3.3.2 基于代数理论的协议分析

该方式具备本文分析方式所具有的优势，如精密度高以及具备强大的推理功能等。20世纪90年代初期Meadows等人便运用该方式对NRL分析器的推理模型进行延伸，但是并未取得突出性实效。近期以来，该方面的研究得到了业界的广泛关注并且采取了一系列的实际活动，产生了FDR模型检测器。Bruno Dutertre经过长期的研究发明了PVS验证系统。此外，基于代数理论的协议分析还包括Spi演算分析。但是这种方式在存在一定的安全缺陷，在实际应用中存在一定的局限性。

3.3.3 规约证明

规约证明是一种最新被提出的新型的技术，最早被Kemmerer提出。该方式可以实现手动以及自动的自由切换，但是自动证明较之前者还不够成熟比较复杂，需要更深一步的完善和探索。

4 结 论

为保障网络通信协议的可靠性，对其实施有效的验证显得尤为重要，本文介绍了能够在实际中得到有效运用的验证方式，在实际中可以根据具体情况进行选择。唯有如此方能够确保网络通信协议的正常运作，推动整个计算机系统高效工作。