三方密码协议运行模式分析法

在两方密码协议运行模式分析法的基础上 ,利用模型检测的理论结果 ,提出了三方密码协议运行模式分析法 .用这种方法对DavisSwick协议进行了分析 ,成功地验证了此协议的安全性 ,说明了所提出的三方密码协议运行模式分析法的有效性     

安全协议形式化分析理论与方法研究综述

综述目前安全协议形式化分析的理论与方法 ,包括安全协议的分类与模型 ,安全协议形式化分析的 3种典型方法 (基于推理的结构性方法 ,基于攻击的结构性方法 ,基于证明的结构性方法 ) ,安全协议分析的形式化语言 ,安全协议设计的形式化方法 ,以及安全协议形式化分析面临的挑战     

一种混合的安全协议形式化分析技术

分析了模型检测技术和逻辑推证技术的优点与不足,并在此基础上提出了一种混合的形式化分析技术的说明,该技术可提供更为完全的安全协议形式化分析.     

分布式网络环境下密码协议形式模型和安全性

随着互联网的应用和发展,各种类型的安全协议,包括具有多个角色、多种密码运算的复杂密码协议,已广泛应用于分布式系统中解决各种安全需求.在大规模分布式网络环境下,参与协议运行的主体是大数量的甚至是动态的,密码协议运行环境极为复杂,这使得密码协议的安全性描述和分析变得非常复杂.引入了一个新的代数系统刻画具有多种密码运算的消息代数,并提出了一个新的密码协议模型,描述了无边界网络中的攻击模式,通过建立形式语言规范了无边界网络环境下密码协议的运行环境和安全性质 该协议模型描述了一种“协同攻击”模式,并讨论了密码协议的安全性分析约简技术,给出一个新的安全自动分析过程的简要描述.     

安全协议形式化分析的不变式生成技术

给出了应用于不同系统的不变式的概述,分析了彼此之间的关系,进行了分类,并探讨了其未来发展趋势.密码协议的形式化分析日渐引起人们的广泛关注.这导致了不变式生成与描述技术的发展.不变式是对入侵者可知和不可知消息的定义,可用于协议认证和秘密性的证明,从而成为许多协议形式化分析工具和技术的核心     

一种基于Petri网的模型调度方法

针对软件模型的时间约束能力不强以及形式化验证复杂的问题,本文提出一种基于Petri网的形式化模型调度方法,从时间层次上对模型的合理性进行验证与分析.该方法通过构建系统领域模型到Petri网模型的转换规则,利用Petri网的分析验证技术,实现对软件模型的正确性验证,解决了系统建模时存在的问题.应用实例和实验结果验证了该方...     

基于PVS的密码协议形式化规范

给出用PVS对密码协议进行形式化规范的一种方法.该方法以高阶逻辑为规范语言,利用trace模型来描述协议的行为,并假设系统中存在强攻击者和理想加密系统.重要的结构如消息、事件、协议规则等都通过语义编码方式定义.     

安全协议分析的界--综合模型检查与Strand Spaces

Strand Spaces是一种用于分析安全协议的机器证明方法.简要介绍了 Strand Spaces的基本特点,分析了其优劣,提出了构造协议的理想子环的算法,并以此来约束协议入侵者的能力和协议并行运行的次数.将模型检查与 Strand Spaces结合在一起,提出了一种综合分析方法来验证协议的安全特性,该方法可充分发挥模型检查与 Strand Spaces二者的优势.     

移动IPv6协议的形式化描述研究

文章根据RFC3775简单介绍了移动IPv6机制,提出了移动IPv6协议层次化描述方法,把整个移动IPv6协议分为4个层次加以描述,并通过有限状态机建模,为最终抽象测试集的生成奠定了基础。     

安全协议的形式化分析方法初探

安全协议是网络安全的重要因素，但是它并不完善．我们需要用形式化的方法去分析它是否具有相应的安全属性.本文主要分析了三类典型的安全协议形式化分析方法，研究这些方法的基本思想和优缺点．并提出了形式化分析方法中存在的问题及可行的解决办法.     

SSL3.0基本握手协议的运行模式分析

主要使用运行模式法对简化的SSL3 0基本握手协议进行了形式化分析.通过分析,找到了3种不同的攻击形式,并且对这3种攻击形式进行了深入研究,发现这3种攻击虽然从表面上看都是由于允许不同版本共存的漏洞引起的,但是经过仔细分析攻击的形式,发现这3种攻击是存在差异的.主要是角色欺骗不相同,而这又可能会造成潜在攻击.最后对这个协议进行了改进,从而有效避免了以上3种攻击,提高了协议的安全性     

安全协议:信息安全保障的灵魂——安全协议分析研究现状与发展趋势

信息社会对于信息保障技术手段提出了极大的挑战。安全协议作为信息安全保障的灵魂,越来越凸显出其关键和纽带作用。对安全协议的安全性分析则是信息时代一个重要而无法回避的关键问题。文章通过总结安全协议分析的研究现状与发展趋势,认为我国目前该领域的研究与国外差距较大,加强协议安全性分析研究对我国来说是一个非常迫切的课题。在此基础上,提出了相关对策与建议。     

基于计算模型的安全协议验证软件Crypto Verif研究

目前,对安全协议的自动化证明分为两类：基于符号模型的和基于计算模型的。介绍了基于计算模型的协议证明软件CryptoVerif,介绍了其原理和可证明的安全属性,并使用其证明了一个协议的安全性;最后,指出其不足,为以后的软件改进指出了方向。     

改进型Otway-Rees协议的串空间模型分析

本文在介绍了串空间模型的基本概念和定理的基础上.提出了改进型的Otway-Rees认证协议,然后利用串空间模型的理论和方法,从机密性和可鉴别性两个方面对改进型Otway-Rees协议进行了分析,分析结果表明该改进型协议是安全的.     

基于可信的网上电子支付认证协议研究

针对目前电子商务越来越普遍,现有的网上电子支付认证协议无法满足网络安全需求的问题。提出了一种基于可信的网上电子支付认证协议,该协议融合了PKI安全认证体系,分为电子支付登录协议和电子支付注销协议,把身份验证和签名验证分开两次进行网络安全验证。实验表明,该协议对恶意软件攻击、网络钓鱼以及网络嫁接和中间人攻击都有比较好的安全性能,比目前普遍使用的电子支付认证协议更加有效。     

TLS握手协议的计算模型分析*

本文用BR模型对TLS握手协议进行了计算分析与安全性证明. TLS握手协议作为典型的认证密钥交换协议,可以自然结合到BR认证协议计算模型分析框架当中. 本文对该协议主要通信过程进行了总结、建模和分析,证明当协议所采用的公钥加密函数和消息认证函数均满足计算模型安全性要求时,TLS握手协议在BR计算模型下是安全的.     

基于协议分析的网络入侵检测技术研究

在入侵检测系统中,模式匹配技术是常用的入侵检测分析方法。网络协议分析是网络入侵检测中的一种关键技术,文章对网络层和传输层协议进行分析,最后给出一个例子来说明协议分析的实现过程。     

浅谈计算机仿真中模型的确认与验证

随着一体化仿真技术的提出和发展,人们认识到仿真应该是“建模一实验一分析一建模”这样一个循环体系。在系统仿真中,所构造的仿真模型能否代表系统,这是决定仿真成败的关键。本文对仿真中模型的确认与验证进行了研究。     

对节点位置和能量的无线传感器网络分簇路由协议研究

在无线传感器网络中,分簇路由协议相比于平面路由协议具有一定优势,因此对于分簇路由协议的研究具有重要意义。本文将网络中节点的位置信息与节点的剩余能量相结合,基于LEPS路由协议从工程角度提出一种改进方案E-LEPS路由协议,并讨论了其工作过程。     

基于网络管理协议的目录访问分析和检测

对于网络管理系统来说,重要的是管理员和代理之闻所使用的协议SNMP,它已是网络设备厂商、应用软件开发者及终端用户的首选管理协议,但其安全缺陷对网络构成威胁。本文尝试设计了一种轻量级目录访问协议检测模块与之集成,在方便使用的前提下,尽量避免了网络的安全隐患。