网络通信协议形式化描述与验证技术的研究

首先概述当今常用的协议模型技术；然后重点剖析基于ＦＳＭ、Ｐｅｔｒｉ网和ＴＬ模型的协议形式化描述与验证技术的研究现状；最后介绍了一种最新协议描述技术－Ｚ协议技术。此外，本文还对这四种协议形式化技术各自的特点发表了作者的观点。     

协议描述和验证的基本方法

简要说明了协议描述和验证的基本概念，示例地介绍构造实现描述和协议验证的基本思想，最后以Ｐｅｔｒｉ网形式给出了ＡＢ协议一例。     

网络协议工程中的Petri网技术

按照OSI／RM模型的层次,论述了Petri网在网络协议工程中的研究进展情况,并从协议描述、协议验证与分析的角度给出了基于Petri网的协议工程的基本方法,最后用有色Petri网对数据链路层的Stop-and-Wait通信协议进行描述分析．     

基于着色petri网的安全协议验证方法

设计安全协议时，协议的安全性验证是消除安全协议脆弱性和不精确性的关键步骤，验证安全协议的模型和工具有很多．提出了一种基于着色petri网的安全协议验证方法．通过采用该方法对一个STS协议进行了分析，证明了这种方法的有效性，并根据分析结果给出了改进后的STS协议．     

安全协议的形式化验证技术研究

对安全协议形式化验证方法所应用的技术进行了研究，总结了当前安全协议的各种形式化验证方法的特点，指出今后一段时期内安全协议形式化验证技术的研究方向．     

基于不同形式化模型的网络通信协议验证技术的分析与比较

协议是数据通信、计算机网络等分布式系统的灵魂。协议设计、开发的复杂性的增加导致了协议工程技术的出现，该文主要介绍了协议工程活动中的协议验证与分析阶段。阐述了验证技术的目的与方法，分析了当今常用的协议模型技术，重点介绍了基于FMS、Petri网、以及时序逻辑TL模型的协议验证技术。     

MOT在DRM广播系统中的应用

简单介绍DRM标准规范和MOT协议，详细地描述了多媒体传输在DRM广播系统中的具体实现方法，并通过实验验证其可行性。     

ISO/OSI运输层协议的形式描述

通信协议的形式描述是协议实现、正确性验证和一致性测试的基础．本文用一种混合式模型对ＩＳＯ／ＯＳＩ的运输层协议进行了形式描述，为协议的实现打下基础     

基于Petri网的协议辅助设计工具的实现

研究了一种基于Ｐｅｔｒｉ网的协议辅助设计工具Ｐｅｔｏｎ的实现细节。该研究是对计算机辅助协议工程（ＣＡＰＥ）方法学的一种有益的尝试．     

计算机网络通信协议的一种形式化描述技术

针对目前绝大多数形式化描述技术在处理协议的活性等方面存在的不足,提出一种新的基于公平性假设的时态逻辑技术描述协议,并给出ＡＢ协议的形式化描述实例。     

一种有效的分布式构件交互性质验证方法

目的在基于构件的分布式系统开发过程中,更大程度地消除对构件交互风格和交互协议描述与验证产生的所谓的状态爆炸现象。方法提出一种有效的基于π-演算的构件交互协议验证方法——状态约减验证算法,在模型组合之前,将与性质定义无关的状态剥离,然后再进行模型组合。结果用标记转移系统证明了该验证算法的有效性,采用π-演算描述的同步请求/响应交互模型作为例证,证明上述算法比传统算法更有效。结论该算法缩小了组合模型的状态空间,提高了验证效率。     

A VERIFICATION METHOD FOR COMMUNICATION PROTOCOLS MODELED AS COMMUNICATING EXTENDED FINITE─STATE MAC

本文建立了用于表述含有无限值状态成分的通讯协议机的抽象模型，给出了基于该模型的形式检证法，试制了检证系统．该检证法不需要假定信道的有界性．对于给定的通信协议，检证系统将判定其对指定状态的可到达性．做为检证例，从ＯＳＩ参照模型中抽出了大同步点设置功能单位，就“无死锁”、“无传输错误”等性质进行了实际检证     

一种安全协议的形式化验证方法

BAN(Burrows,Abadi and Needham)类逻辑可以辅助设计、分析和验证网络和分布式系统中的安全协议。介绍BAN逻辑的产生、成分和分析步骤，指出BAN逻辑的缺陷，由此而产生的改进BAN逻辑和现状，并对BAN类逻辑作全面的回顾与展望，得出：BAN类逻辑仍然是密码协议分析和设计的主要工具，但理想化步骤是BAN类逻辑的致命缺陷的结论。展望了BAN类逻辑研究。对未来协议的形式化分析工作具有指导意义。     

基于EPR粒子对的信息签名协议

研究了利用Einstein-Podolsky-Rosen (EPR)对的纠缠特性进行量子数字签名的方案,提出了一个基于测量结果比较的签名协议以及一个基于隐形传态的签名协议. 在基于测量结果比较的签名协议中,通信双方测量各自的EPR并将测量结果与消息M进行比较可以实现M的签名和验证,同时通过量子单向函数来保证协议的安全. 在基于隐形传态的签名协议中,消息发送者将M通过隐形传态传递给接收者来实现对M签名并验证,其安全性由量子隐形传态的物理特性来保证. 这两种协议均可以脱离可信赖的第三方,且通信过程中不需要密钥,具有无条件安全性.     

UPPAAL环境下通讯协议的自动验证

对UPPAAL环境下通讯协议的规范验证方法进行研究,在此基础上,利用一组时间自动机模型模拟一个具有严格时间限制的网络通讯协议,并对其正确性进行自动验证.     

基于认证测试的通用安全协议设计方法

以认证测试方法为基础,提出了一种通用的安全协议形式化设计方法,使用该方法对Needham-Schroeder(NS)公钥协议进行了重新设计.最后通过认证测试方法证明了重新设计的NS协议能够满足安全协议的保密性、身份认证和数据认证的要求,并且有效避免了原NS协议存在的中间人攻击问题.     

基于SPIN的SAS协议和NS公钥协议分析

给出SPIN模型检测协议的验证步骤,使用其分析验证SAS协议的安全属性和数据流行为属性,以及NS公钥协议的机密性和认证性.结果成功发现SAS协议数据流的缺陷和NS公钥协议的攻击路径.     

用串空间分析路由协议SGSR

用形式化方法分析安全协议是协议分析的有效手段,近年来,出现了众多的研究方法.串空间模型是一种新兴的形式化分析工具,其中,"理想"和"诚实"两个概念简化了分析协议的步骤.首次利用串空间理论对由徐兰芳提出的一种安全的Ad Hoc网络路由协议SGSR进行分析,并分析了它的认证性和机密性,结果证明此协议能够达到协议的目标。