网络协议的形式化分析
网络协议的形式化分析【1】
摘 要：随着形式化方法和技术的日趋完善，网络协议的开发已逐步从非形式化描述、手工方法实现过渡到已形式化描述技术为基础，渗透到网络协议分析、综合、测试等各环节的软件工程方法。
本文从网络协议的基本要素、协议的形式化模型介绍了网络协议，并从协议的性质描述、不变性分析、可达性分析、基于有序二叉判决图的符号模型检验对网络协议进行了形式化设计与验证，最后进行了测试。
关键词：网络协议 形式化分析 符号模型检验
协议一词最早出现在通信系统，协议历史拥有像通信一样古老的历史。
从古至今，人们一直都在不断的探索研究，怎样才能建立一个能够在快速在远距离上传输信息的系统。
如果想要实现信息在远距离间传递，不光需要硬件设备，也就是发送和接收信号的设备，还需要建立一整套能够规定信号所代表的意义以及传递接收信号方式的规则、标准或者约定，这个规则就是协议。
1 网络协议的基本要素
一套完整的，能够确保计算机网络可以顺利进行数据通信的网络协议要包括下边的五点基本要素：(1)协议所提供的服务。
(2)对协议运行环境所进行的假设。
(3)用来实现协议的消息词汇。
(4)对该词汇中每个消息的编码。
(5)用来控制消息一致性的过程规则。
实现计算机之间高度自动化数据通信的网络协议，一般都会极其复杂。
借鉴对复杂系统问题分析研究的思想，分层结构对于理解和设计网络协议有着重要的作用。
“七层”协议结构模型是目前网络协议的标准体系结构，也成为了网络协议开发的基础。
2 协议的形式化模型
协议分析和设计其中一项核心技术就是形式化模型。
网络协议的形式化规格可以在形式化模型的基础上实现，从而为协议的形式化分析与验证、协议综合、协议测试、以及协议实现等提供良好的基础。
形式化模型包括以下几点。
2.1 协议的有限状态机模型
有限状态机包括有限状态集、输入集和状态转移规则集;有限状态集，用于描述系统中的不同状态;输入集用于表征系统所接收的不同输入信息;状态转移规则集用于表述系统在接收不同输入下从一个状态转移到另外一个状态的规则。
2.2 Petri网模型
Petri网是一种适合于并发、异步、分布式系统描述与分析的图形数学工具。
Petri网已成为网络协议分析和设计的典型形式模型之一。
它作为系统描述和分析的工具，除了具有静态结构外，还包括了描述系统动态行为的机制。
这一特征是通过允许位置中包含令牌，令牌可以依据迁移的引发而重新分布来实现的。
2.3 协议的时态逻辑模型
时态逻辑是模态逻辑的扩充，它涉及含有时间信息的事件、状态及其关系的命题、谓词和演算。
要描述一个协议，首先要标识系统中的个体常量，定义变量，表达命题、谓词函数。
以下为命题与谓词的表达。
(1)个体常量m0，m1表示序号为0，1的报文;any表示无序号的任意报文;ack0，ack1表示序号为0，1的认可报文。
(2)个体变量m代表m0，m1，any;ack代表ack0，ack1;seq代表0，1序号;a代表原子行动或事件。
(3)谓词at(a)开始一个协议行动或事件。
2.4 通信进程演算模型
通信进程演算是计算机通信系统的基本理论模型，它也是许多形式化语言的基础。
通信进程演算的基本成分是事件与进程，而进程是通过顺序、选择和并行三个基本算子来定义的。
一般用大写字母来表示进程，用小写字母来表示事件。
3 协议的形式化设计与验证
协议的设计验证是对协议的功能和性能进行校验的过程，是保证协议开发质量的必要环节。
协议形式化验证首先需要对协议性质进行系统的语言描述，然后基于协议的形式模型或者形式语言进行描述，通过适当的技术对协议性质进行分析校验。
3.1 协议的性质描述
设计网络协议的目的就是设计出的协议要满足功能和性能。
一方面，协议本身应用问题的特征性对协议的功能和性能具有特殊的要求;另外一方面，协议的功能和性能所拥有的协议的性质，是独立于问题的一般性要求。
协议的性质包括活性、安全性、一致性、完备性、可恢复性和有界性六方面。
(1)活性就是指无死锁性，如果在协议运行时候发生一些好事，就叫协议的活性，像发生预定的事情，能够到达指定的协议状态，可以进行应该进行的协议活动等都是协议的好事情。
协议的终止性和进展性两反面可以体现协议的`活性。
也就是说具有终止性和进展性的协议就拥有活性。
如果协议能够在从任何一状态下开始运行都能正确的到达终止状态，就是协议的终止性。
终止状态在某些情况下也会和初始状态是同一个。
所以协议总能从初始状态开始运行然后正确的回到初始状态，并可反复运行，这就是协议的可重复性，即可重复性=终止性+进展性=活动性。
(2)安全性就是没有坏的事情出现在协议运行的时候。
像不可接收事件、不可进一步向前的状态、错误的行动、错误的条件、变量值越界等都是坏的事情。
坏事情一般会导致死锁和活锁两种情况发生。
(3)一致性就是指协议的服务行为和协议行为保持一致。
像协议需要为用户提供的所要求的业务和不用提供用户没有要求提供的业务都体现了协议的一致性。
(4)完备性，协议拥有完全符合协议环境各种要求的性质，也就是在考虑了用户要求、用户特点、通道性质、工作模式等各种潜在影响因素之后构建的协议构造，同时兼备考虑各种错误事件以及异常情况的处理。
(5)可恢复性是指当协议出现差错后，协议本身能否在有限的步骤内返回到正常状态下执行。
可恢复性是和可重复性相关联的一个性质。
(6)有界性是与协议中的变量和参数有关的一个性质，用来衡量协议中的变量和参数是否超过其限定值。
3.2 不变性分析
系统不变性是某一逻辑公式表达的系统性质的永真性，它不随系统的状态变化或执行序列而改变。
系统不变性分析实际包含两个任务。
第一是分析系统应该具有的不变性质，并用逻辑公式来表示，第二个任务是分析系统的执行，证明该逻辑公式成立。
3.3 可达性分析
可达性分析是试图产生和检查协议所有部分的可达状态，进而检验基于状态或者基于状态序列的协议性质。
所谓可达状态是指协议从初始状态开始经历有限次转换之后可达到的状态，所有可达状态构成了系统状态空间。
可达性分析算法是用来生成并检验一个特定的初始状态可达的所有状态算法。
3.4 基于有序二叉判决图的符号模型检验
符号模型检验是采用紧凑的信息压缩形式来隐式表示系统可达状态和要求证明性质的逻辑公式的模型检验。
有序二叉判决图是隐式、高效率表示状态空间的一种数据结构。
基于有序二叉判决图的符号模型检验是分析验证协议系统的有效技术。
基于有序二叉判决图实现的模型检验算法能有效地避免状态爆炸的问题，使得验证系统适用的系统规模扩大，现已能对具有多达1020个状态的系统进行验证。
基于有序二叉判决图的符号模型验证主要考虑以下几个方面：状态的布尔公式表示;状态转移关系的布尔公式表示;Kripke结构的布尔公式表示;CTL公式在布尔公式表示的Kripke结构上的解释。
现用QBF公式表示Kripke结构，并把用这些符号表示的Kripke结构上的CTL算子用QBF上的算子来描述。
实际上，因为逻辑连接词在CTL*和QBF上有着相同的意义，所以只需要刻画算子EN，而其它的CTL*的算子可以通过EN和逻辑运算的函数不动点进行描述。
4 网络协议的测试
测试是保证网络协议质量的一个重要手段，是协议实现过程中的一种实验活动。
尽管测试并不能完全证明协议实现的正确性，但是在系统的测试活动检查下，可以把协议在实现过程中出错的概率降低到实际应用可以接受的程度。
相对而言，基于有限状态机模型的协议测试方法有比较高的错误覆盖率。
然而，在实际中，协议规格的状态机模型并不满足对有限状态机的假设，即便满足，相应的测试生成算法也太复杂，生成的测试序列也太长，测试成本太高。
随时着各种各样的有限状态机规格的广泛使用，借助于软件数据流测试的思想，基于数据流的协议测试序列生成方法相应得到了研究应用。
数据流测试通常基于有向数据流图。
在理想情况下，测试所有可能的输入数据将提供最完全的程序行为信息，而在实际测试中，通常选择一个可以代表整个输入域的子集。
5 结语
形式化方法是基于严密的、数学上的形式机制的系统研究方法。
客观地讲，有了数学的应用，就有了形式化的方法。
迄今为止，形式化方法成功地应用于空中交通管制系统、铁路信号系统、核电站控制系统、通信系统、医疗监护系统、硬件电路等诸多领域。
网络协议的形式化分析和设计正在向完善化、系统化、自动化和标准化方向发展。
参考文献
[1] 鲁来凤，吴振强，马*峰.基于PCL的改进型Helsinki协议的形式化分析[J].华中科技大学学报(自然科学版)，2011(4).
[2] 王惠斌.安全认证协议的设计与分析[D].解放军信息工程大学，2010.
无线网络安全协议的形式化分析【2】
摘 要：传统的有线网络由于受到环境等条件的制约，在各方面都存在着亟需解决的问题，那么，发展可行的无线通信网络技术也就成为网络发展的必然趋势。
本文对无线网络安全协议的形式化方法进行了全面的概述，分析了无线网络的安全威胁以及具体表现，着重探讨了无线网络安全协议的形式化分析方法。
关键词：无线网络安全;形式化分析;安全协议
中图分类号：TP393.08
随着科学技术的迅速发展，网络得到了较大的发展空间，由于传统的有线网络随着网络应用的不断发展，难以适应现代化社会的需求，因此逐渐被无线网络替代，在丰富了人们生活的同时也给人们带来了更为便捷的服务。
但是随着无线网络的发展，也将面临着网络安全问题。
1 无线网络安全协议的形式化方法综述
1.1 无线网络安全协议
无线网络的发展随着社会经济的迅速发展，得到了较大的发展空间，并且随着无线网络的不断发展，针对于无线网络的一个个新的标准和技术也在不断的出现，在某一开放系统中由于主体数量比较大，而两个互不相识的主体希望进行安全通信，那么，它们之间就必须要建立一个安全的通信渠道，而建立了安全通信渠道的两个主体之间必须要运行某种安全协议，以此来完成双方互相认证的功能，当然还应该建立秘钥任务。
而无线网络安全协议也就是针对于无线网络而言的安全信道，按照自己的功能可以将安全协议分为可以将其分为三类，首先是认证协议，这主要是提供给一个参与方关于其通信对方身份的一定确信度的一种方式，认证协议包含了实体认证协议、消息认证协议等其他协议，并且认证协议主要是用来防止假冒、否认等相关攻击的。
其次是认证及秘钥交换协议，这主要是为了给身份已经被确认的参与方建立一个共享秘密，目前这种方式是网络通信中最为普遍的一种安全协议。
最后是秘钥交换协议，这种协议是在参与协议的两个实体之间，或者是多个实体之间建立的共享秘密，尤其是这些秘密可以作为对称秘钥，用于加密、消息认真以及实体认证等多种密码学用途[1]。
1.2 安全协议的形式化方法
针对于安全协议形式化分析，我们可以将其分为计算机安全方法，以及计算机复杂性方法两大类，而计算机安全方法，又可以称之为基于符号理论的形式化方法，它主要是强调自动化机器的描述和分析，但是，由于这种方法存在不可预测性和复杂性，所以这种方法主要是由于攻击者具有指数规模的可能操作集，会导致状态爆炸的问题，计算机安全方法还可以进一步分类：模态逻辑方法、模型监测方法等。
计算机复杂性方法，也可以称之为证明安全方法，其主要思想是通过归纳推理，而计算机复杂性方法中应用较为广泛的是CK模型和UC模型。
2 无线网络的安全威胁和具无线网络的具体表现
无线网络的应用较大程度的扩大了无线网用户的自由程度，并且无线网络还具有安装时间短，更改网络结构方便灵活，灵活增加用户等等其他的优点，而最为重要的是它还可以提供无线覆盖范围内的安全功能漫游服务等特点。
但是，与此同时无线网络也面临着一些严峻地新的挑战，而其中最为关键的环节就是无线网络的安全性，而由于无线网络主要是通过无线电波在空中进行数据传输的，在数据发射机覆盖的区域内，基本上所有的无线用户都能够接收到这些数据，也就是说用户只需要具有相同的接收频率，那么用户就能够获取所传递的相关信息。
并且由于无线移动设备在存储能力，以及计算能力等其他的方面都存在一定的局限性，也就导致在有线环境下，许多安全方案以及安全技术并不能够直接的在无线环境中应用，比如：防火墙通过无线电波进行的网络通信并不具备一定的相关作用，而任何人在特定的区域范围内都能够截获或者是插入网络数据，导致无线网络面临着一些安全威胁{2]。
而针对于安全威胁，我们可以将其分为故意威胁和偶然威胁这两种形式，而故意威胁又可以进一步分为主动故意威胁和被动故意威胁，无线网络安全威胁，主要表现在以下几个方面。
首先，攻击者伪装成为合法的用户，通过无线接入非法访问网络资源，从而给无线网络带来安全威胁，这是最为普遍的一种威胁;其次是针对无线连接或者是无线设备实施的拒绝服务攻击;第三是恶意实体可能得到合法用户的隐私，然后对无线网络进行非法入侵;第四，恶意用户可能通过无线网络，将其自动连接到自己想要攻击的网络上去，并采取相关方法实施对特定的网络进行攻击。
此外还有很多种威胁，比如：手持设备容易丢失，从而泄露敏感信息。
3 无线网络安全协议的形式化分析的具体方法
安全协议主要是采用密码技术来保障通信各方之间安全交换信息的一个规则序列，其主要目的就是在通信各方之间提供认证或为新的会话分配会话密钥，目前分析安全协议的形式化方法主要有三种，即：推理构造法，这种方法主要是基于知识和信念推理的模态逻辑，比如K3P逻辑等其他逻辑;再有就是攻击构造法，这种方法从协议的初始状态开始，对合法的主体和一个攻击者所有可能执行的路径进行全方面的搜索，以此来找到协议可能存在的问题;此外还有证明构造法，证明构造法集成了上述两种方法的思想和技术。
对于无线网络安全协议的形式化分析方法，笔者认为，可以从以下三个方面进行分析。
第一，基于逻辑证明的协议分析。
BNA逻辑，这种方法最早用于认证和秘钥交换协议的形式化方法，它的出现极大地激发了研究人员对于这一领域的广泛兴趣，BAN逻辑中的证明构造是非常简洁的，并且它还比较容易完成，但是，应用BNA逻辑分析只是一个协议，从具体的协议到逻辑表达式的抽象过程都是比较困难的。
BNA逻辑的语法中区分了主体、秘钥以及时鲜值这三种密码要素，并且BNA逻辑可以对WAI的认证模型进行有效的分析，但通过相关研究表明，WAI并不能够有效地实现全部的认证以及秘钥协商目标，这主要是由于WAI中存在着诸多的安全问题，比如：无法提供身份保护、缺乏私钥验证等，这就表明WAPI无法提供足够级别的安全保护{3]。
第二，攻击类型以及安全密码协议形式化的分析。
在任何一个开放性的无线网络环境中，网络管理人员必须要全方位地考虑到对攻击者存在，主要是由于攻击者可能实施各种攻击，对一些具有价值的文件和网络系统进行破坏，要处理这种安全问题就必须要积极的采取一定的措施。
认证协议主要是建立在密码基础上的，而它的主要目的就是为了能够有效地证明所声称的某种属性，认证协议的主要攻击者判定是依靠有没有授权，并且企图获益的攻击者或共谋者。
在一般情况下，进行分析认证协议的时，主要采用的是假设底层密码算法比较完善的方式，并不考虑其可能存在的弱点，认证协议典型的攻击主要有消息攻击、中间人攻击以及平行会话攻击等其他形式。
第三，基于CK模型的协议形式化分析。
CK模型的协议形式化，其主要目标是通过模块化的方法来设计和分析秘钥交换协议，以此来简化协议的设计和安全分析，首先必须要将秘钥协商协议定义在理想的模型之中，之后再采用不可区分性来定义理想模型中的安全性，然后再通过相关方法将协议编译成现实模型中的协议，CK模型采用了相关方法对WAPI的安全性进行了分析，并指出WAPI中存在的安全缺陷。
4 结束语
综上所述，无线网络给人们的生活和工作等方面带来了较大的便利性，但是由于无线网络具有开放性和无线终端的移动性等特点，导致在有限网络环境下的一些安全方案无法直接应用。
采用形式化分析方法能够有效的研究出无线网络的安全保障技术，从而促进我国网络技术的发展。
参考文献：
[1]宁向延，张顺颐.网络安全现状与技术发展[J]，南京邮电大学学报(自然科学版)，2012(05).
[2]李浩.无线网络技术难点分析及安全方法探讨[J]，技术与市场，2014(07).
【网络协议的形式化分析】相关文章：
社会网络分析网络传播论文10-13
关于网络暴力的伦理分析论文10-14
风险分析网络安全论文10-14
网络传销的特点与治理对策分析论文03-29
关于网络财务报告现存问题的分析11-23
虚拟网络的主要技术浅析的研究分析论文10-15
分析网络小说流行性07-02
分析房地产网络营销12-08
药品网络营销分析论文07-11
网络营销分析论文范文07-11