基于串空间模型的3GPP认证密钥交换协议分析

基于串空间模型理论及认证测试方法形式化分析了第3代伙伴计划(3GPP)认证密钥交换协议,指出了该协议应用于不安全的信道时存在保密性和认证正确性的缺陷,同时给出了对该协议的2个攻击方法.由此提出了一种改进的3GPP认证密钥交换协议以克服原协议存在的缺陷,应用串空间模型理论及认证测试方法形式化证明了该改进协议在不安全的信道上可确保消息的保密性,移动用户和服务网络间的双向认证,以及消息加密密钥和完整性密钥的新鲜性.     

基于串空间的Kao Chow加密协议形式化验证

Kao Chow加密协议是由Kao和Chow提出的,他们利用BAN逻辑证明了该协议的认证性,但没有证明该协议的保密性,而且没有说明协议参与实体间得到的新会话密钥是否一致.事实上,由于BAN逻辑自身的缺陷,它无法用于证明加密协议的保密性.基于此,给出了Kao Chow加密协议的串空间模型,这个模型不仅验证了该协议的认证性,还验证了它的保密性及新会话密钥的一致性.     

基于串空间模型的认证测试方法

串空间模型认证测试方法是定理证明安全协议分析法中最具有代表性的一类.利用串空间模型理论对Needham-Schroeder(N-S)公钥协议中中间人攻击问题进行形式化分析与设计,并对其进行证明.与原有技术相比,该方法更为形式化,协议分析人员可以很方便地进行手动分析,并且更有利于协议分析自动化工具的实现.     

RFID安全协议的数据去同步化攻击

为了分析无线射频识别(RFID)安全协议的数据去同步化攻击问题,对串空间模型进行了扩展,引入了分析RFID安全协议数据去同步化攻击的能力,并给出了数据去同步化攻击的判定定理.在扩展的串空间模型下,对近年来提出的一个基于哈希函数的RFID安全协议和一个无需后端数据库的RFID认证协议进行了分析,发现了针对这2个RFID安全协议的数据去同步化攻击,该攻击破坏了协议的可用性.分别对这2个RFID安全协议进行改进,改进后的RFID安全协议克服了存在的安全隐患,能够抵御数据去同步化攻击.     

用串空间分析路由协议SGSR

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

非否认协议公平性分析的扩展串空间方法

针对在非否认协议公平性的形式化分析中,如何弱化初始假定和避免状态空间爆炸等问题,提出了扩展串空间方法.通过将签名运算引入串空间理论,从而对串空间理论的项集合进行重新定义,进一步通过对子项关系、攻击者迹和自由加密假定的扩展,并结合丛概念,构成了扩展串空间.分析非否认协议的公平性,首先将协议行为归纳为攻击者串、发送者串、接收者串和可信第3方串,以此构造协议的扩展串空间模型,然后结合协议迹和定理证明验证丛中存在发送者串等价于丛中存在接收者串,从而证明非否认协议公平性.通过扩展串空间方法对Zhou-Gollmann协议公平性的分析,得到了与Kailar逻辑和Lanotte自动验证方法相同的结果.与Kailar逻辑相比,扩展串空间方法仅使用自由加密假定,弱化了初始假定;与Lanotte自动验证方法相比,扩展串空间方法无需使用状态空间搜索,避免了状态空间爆炸问题.     

基于串空间的认证协议分析

网络通信的普及和发展使得对网络协议尤其是安全协议的需求日益增长.由于安全要求的多样化以及攻击方式的层出不穷,使得对网络安全协议的形式化分析效率和准确性提出了更高的要求.串空间理论(strand space theory)和模型是当前避免状态爆炸、提高协议形式化分析效率的有效方法.本文通过一个具体的认证协议例子来说明它的特点.     

安全协议形式化分析方法的融合性研究

分析了BAN逻辑和串空间理论的特点与不足.为了弥补二者的不足,提出了一种融合两种理论的形式化分析方法.通过实例分析,证明该分析方法能够将BAN逻辑和串空间的优点互补综合,使安全协议的分析更可靠、稳定、高效.     

基于电子商务单向认证协议的Petri网模型

基于公钥基础设施PKI的安全认证协议是目前电子商务常用的认证协议。根据这个安全认证协议用Petri网协议模型技术构造了单向认证协议的Petri网模型的状态空间。这样就可以进行仿真分析，找到协议的安全漏洞，完善认证协议。     

一种无线传感器网络中基于簇的安全协议

在SPINS,SECOS协议的基础上,提出了基于簇的安全协议(cluster-based security protocol,CBSP).CBSP中安全的簇首选举及基于组播认证的密钥更新机制,有效提高了簇及密钥管理的安全性,减少了节点及网络资源消耗.利用串空间模型对协议进行形式化分析,验证了其正确性.CBSP中基于簇的入侵检测机制有效地抵御了外部节点的攻击.基于IDS的更新响应机制减少了簇首和密钥更新周期,进一步优化了CBSP.仿真结果显示,CBSP能很好地适应无线传感器网络特性,当网络遭受选择转发攻击时,CBSP能有效抵御攻击,减少资源损耗.     

混合UDP-TCP协议在PDA浏览器设计中的应用

在PDA（个人数字助理）中浏览器的设计中,由于无线网络延迟大、带宽窄,所以基于TCP协议的HTTP应用并不是理想的传输协议。但使用UDP作为短会话时的传输层协议,而对于有大量数据需要传输时则使用TCP作为传输层的协议,这样的混合协议可以很好的解决数据传输的问题。     

IPComp协议在IPv6中的研究与实现

实际应用中,当对IP数据包应用AH或ESP协议时,会导致传输的IP数据包长度增加,加重网络负载,数据包被再次分段,增大数据传输的时延等问题。介绍了使用IPComp协议对经过IPsec处理的数据包进行压缩的方法,并实现了在支持IPv6协议的Linux平台下数据包经IPComp协议压缩后的数据传输。     

网络协议描述和验证技术的分析与比较

随着计算机网络与分布式系统的发展，通信协议的设计和实现的复杂性的增加导致了协议程技术的出现．讨论协议形式描述与验证技术的目的与方法，重点介绍了基于FMS、通信演算系统以及Petri网协议验证技术的特点及其优点．     

局域网中的TCP/IP通信协议

介绍了通信协议的分类以及TCP/IP通信协议的概念及组成,分析了常用通信协议的特点、性能和必要的配置方法.     

实时CORBA的可插拔协议的研究

为了满足实时应用的QoS需求,在实时ORB的实现中引入了可插拔协议技术.然后,在通用ORB协议互操作体系结构基础上,以成熟的实时中间件产品TAO为参考,讨论在实时CORBA中可插拔协议的体系结构框架及其实现的模式.     

一个基于模态逻辑的安全协议度量方法

为将量化分析方法引入安全协议分析中,以模态逻辑方法为基础定义了协议度量方法,并形式化地给出度量协议内容对协议安全目标满足度的参数和方法,同时在此基础上,进一步地给出了对安全协议冗余进行度量及化简的方法。应用该方法对实例协议进行分析,直接描述各协议内容的贡献度,显示冗余内容对目标实现的无效作用,从而可以安全化简。量化分析在安全协议形式化分析中的应用是本方法的主要特点,它具有模态逻辑方法的优点及缺陷。     

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

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

采用P4的数据平面NAT-DP技术方案

针对协议转换（network address translation protocol translation,NAT PT）技术服务于 IPv4和IPv6节点之间的通信,无法实现多协议节点之间的数据包通信,缺乏协议扩展功能的问题,提出一种基于P4的网络地址 可编程数据平面协议转换（network address translation programmable data plane protocol translation,NAT DP）技术方案。该方案运用可编程协议无关报文处理语言完成解析器、控制流和匹配动作表的定义,实现多协议数据包在数据平面的解析、协议转换与重组。实验结果表明,该技术方案可以有效解决NAT PT的协议扩展性问题,并使管理员在数据平面实现协议转换机制的可重配置。     

基于协议状态分析的入侵检测系统

提出了一种基于协议状态分析的入侵检测方法,不仅充分利用了协议的状态信息,而且考虑了相邻的数码包的内容状态,构造出协议状态序列,通过状态转换来检测入侵,有效地完成网络各层协议的分析,提高了检测的全面性、准确性和效率,实验结果表明是可行的。     

KERMIT通信协议的一种改进方案

针对日趋国际标准化的KERMT通信协议的一些不足,提出了一种改进方案,使其在文件传输中断时,能够从中断处迅速恢复传输,保证无差错无重复地正常工作。