面向嵌入式系统的IPSec形式化建模

为了满足嵌入式系统在网络通信环境下的一些安全需求,通过考察嵌入式开发的系统环境,对比现存的一些网络安全问题的解决方法,采用选取适用的IPSec(网络层安全协议)模块,并使用形式化语言对其进行描述,以给有此类安全需求的嵌入式开发提供一个形式化的IPSec模型.同时,在协议的开发过程中引入形式化的方法也有利于保证协议的一致性.     

用于通信网络协议开发的形式化方法

阐述了在开发通信网络协议中遇到的困难，提出用协议工程的方法来开发通信网络协议。介绍了协议工程、形式化方法及核心技术形式描述技术和几个应用较广泛、较常见的形式化方法，即SDL、ESTELLE、Petri网、LOT0s，并给出了对这些形式化方法的分析和评价。     

基于ASN.1的应用层协议的描述与开发

本文介绍了一种采用形式化描述语言ASN.1对应用层协议进行描述与开发的方法,协议的ASN.1描述具有简洁、可读性好、精确和无二义性等特点。在基于ASN.1的开发环境下对应用层协议的开发具有高效、可靠和易于维护等优点,解决了目前应用层协议开发中存在的许多问题。     

通信协议工程学进展

本文讨论通信协议工程学中的协议开发生命周期,协议的典型开发阶段,其中包括协议形式描述、协议验证、协议实现、协议一致性测试,以及主要研究方向。     

基于B方法的TCP协议形式化研究

协议的规格说明主要是以自然语言描述的,对其进行形式化的目的是精确描述协议,减少开发人员对协议规格说明理解的偏差.B方法可产生简明、精确、无歧义且可证明的规格说明.适合对协议进行形式化描述和一致性测试.本文详细地介绍了使用B方法对TCP协议进行形式化,并据此生成了测试用例,提高了TCP协议一致性测试的质量和可靠性.     

基于事件逻辑的改进Needham-Schroeder协议安全性证明

安全协议是现代网络安全的基础,密码协议的安全性证明是一个挑战性的问题。事件逻辑是一种描述分布式系统中状态迁移的形式化方法,用于刻画安全协议的形式化描述,是定理证明的基础。用事件序语言、事件类和一个表示随机数、密钥、签名和密文的原子类,给出身份认证协议可以被形式化定义和强认证性证明理论。利用该理论对增加时间戳的Needham-Schroeder协议安全性进行证明,证明改进的Needham-Schroeder协议是安全的。此理论适用于类似复杂协议形式化分析与验证。     

PPP协议一致性测试集生成方法研究

测试集的生成方法是一致性测试技术的核心.介绍了形式化描述技术在测试集生成过程中的应用,针对PPP协议介绍其协议实现时的状态迁移.使用形式化描述语言SDL对PPP协议进行形式化描述,并以此为基础生成测试集,这些测试集能有效地应用于PPP功能实现模块.     

基于编译技术的协议解析方法

在过程工业的控制中存在着大量的通信协议，这些协议的结构差别很大。要进行上层应用开发，必须对这些协议进行解析和处理。该文讨论了用形式化描述的方法对协议进行描述，实现了与协议无关的协议解析和处理，从而避免了针对不同通信协议均要编写相应的解析和处理程序，使协议的解析和处理具有更好的灵活性和普适性。     

基于协议形式化描述的网络增值服务开发方法与技术

增值服务是在原有网络的软硬件基础之上进行的功能开发，它在不影响原系统功能的前提下实现功能附加，使网络功能得到增值．本文引入形式化描述技术，提出了基于协议形式化描述的网络增值服务开发方法，并通过对文件传输协议的描述讨论了该方法的具体应用．最后总结了该方法在实际网络增值开发中的应用技术．     

一个安全协议形式化分析工具的研究

介绍了安全协议形式化分析方法,给出了一个自动化分析集成工具。该工具基于模态逻辑实现自动推理,采用可视化框架描述协议体。重点分析了该软件的模块结构和工作原理,可为形式化分析工具的设计和开发提供参考。     

基于时态逻辑的协议RSL形式化描述

研究以RAISE规范语言(RSL)描述时态逻辑中always算子、sometimes算子和until算子的方法以及对复合时态算子的描述方法,提出在时态逻辑模型基础上用RSL对协议进行形式化描述的步骤,以AB协议为示例,给出其基于时态逻辑模型的RSL描述,从而证明该描述模型有利于协议验证和协议测试用例生成的自动实现。     

基于输入/输出动作的协议形式化描述和测试用例生成方法

通信协议的形式化描述及在其基础之上的协议测试用例生成,一直是协议工程的重要研究内容。为此尝试将RSL引入协议形式化描述：首先探讨了一种基于输入/输出动作模型的协议形式化描述方法;随后对基于RSL描述的协议测试技术展开了讨论,提出了一种基于输入/输出动作的协议测试序列生成法则以及基于此法则的测试用例生成方法,并对使用该方法生成的测试用例的性质进行了讨论。     

RSL应用于协议形式化描述的研究

在RSL形式语言的基础上扩充了时间描述机制，使其能够描述协议的实时性；并且根据该语言的特点．提出了一种面向对象的FSM模型(OOFSM)，该模型将面向对象技术与FSM相结合．既可以有效地解决当构造复杂协议时FSM所面临的状态爆炸问题，又可以使所描述的协议具有可重用性、可组装性且易于维护；最后给出了一个实例说明OOFSM的建模过程．并用扩充的RSL进行了形式化描述。     

RSL在协议形式化描述中的应用研究

将RSL引入协议工程，探讨了对协议进行形式化描述的一条新途径。为RSL扩充了时间描述机制，讨论了基于两类基本模型（状态模型和进程模型）的协议描述方法及一般描述步骤。以示例方式给出了RIP路由简化算法的RSL形式化描述。与其他方法相比，扩充后的RSL描述能力强，描述手段灵活，能更有效地支持验证、测试等后续阶段的工作。     

基于RSL的协议形式化描述与验证方法

讨论使用RAISE规范语言（RSL）描述6种协议元素的方法。在RSL描述的基础上,借助操作符的运算规则、并行扩展规则和同步会合事件隐藏规则,对协议的相关性质进行验证,以一个简化的停止等待协议规范的描述和验证实例证明,与其他形式化方法相比,RSL表现出较强的描述能力。     

基于CFSM的协议形式化技术研究

本文主要了基于通信有限状态机的协议形式化技术。     

网络协议形式化模型的分析与应用

网络协议的形式化模型是协议分析和设计的核心技术之一。论文在简要分析当前的几种常用网络协议形式化模型之后,指出时序逻辑作为网络协议形式化模型的独特优越性,然后给出用一种线性时序逻辑MPTL描述IGMP协议的具体实例。     

密码协议安全性证明系统解析器的设计与实现*

可证明安全性是密码协议安全性评估的重要依据,但手写安全性证明容易出错且正确性难以判定,利用计算机辅助构造游戏序列进而实现自动化证明是当前一种可行的方法。为此提出一种基于进程演算的密码协议形式化描述模型,定义了描述密码协议安全性证明中攻击游戏的语法规则,并借助工具LEX和YACC,设计出解析器程序,将密码协议及其安全性的形式化描述解析为自动化安全性证明系统的初始数据结构,并用实例来说明这种方法的可行性。     

Cryptographic protocol security analysis based on bounded constructing algorithm

1 Introduction 1.1 Background Cryptographic protocols have been used to provide security services for many applications on the open communication environment. More and more cryptographic protocols will be designed to solve the increasing security requirem…     

安全协议的关联性研究

关联性是安全协议的基本特征，该文提出了协议相关性的分析方法，从主体认证关联、消息间关联、消息内部关联 3个角度分析了协议的相关特征，阐述了相关性的概念和关联规则构建方法，构建了基于关联性的协议描述模型，为安全协议的形式化分析提供了新的思路。