安全协议及其形式化分析研究

安全协议是网络安全的重要基础,形式化分析是保证安全协议具备相应安全性质的有效途径.通过对安全协议进行分类,阐述了各类协议所应具备的安全性质;并基于安全协议进行形式化分析时所作的各种假设,综述和分析了三类典型的安全协议形式化方法,给出了安全协议形式化分析研究的发展趋势.     

军网身份鉴别协议形式化分析

形式逻辑是一种抽象的逻辑证明工具,密码协议的形式逻辑证明技术日趋得到重视,人们采用形式逻辑分析方法发现了许多协议中存在的安全缺陷,它的实用性已经得到了充分证明。本文对目前较为常用的形式逻辑分析方法——BAN逻辑的形式化分析理论进行了介绍,在此基础上对军网身份鉴别协议进行了BAN逻辑描述,并对协议的安全性进行了理论分析与证明。结果为协议能正确传递鉴别双方的信任关系,协议设计上不存在冗余步骤。     

基于Hoare逻辑的密码软件安全性形式化验证方法

为了解决密码软件安全性验证效率和准确率低的问题,提出了基于Hoare逻辑的密码软件安全性形式化验证方法。首先对密码软件的主要性质进行描述,然后通过密码软件运行时随机向量的分析,得到密码软件运行的矩阵表达式,再将其进行线性变换,计算密码软件运行时数据的方差和协方差矩阵,获得密码软件运行时数据矩阵的主成分空间,并对密码软件运行的主成分进行分析;最后,利用密码软件的逻辑模型和软件运行的状态集合对密码软件安全形式化验证的流程进行分析,建立密码软件的运行模型并设置安全属性,并将密码软件运行时出现的故障进行标记和处理,得到密码软件运行的安全结果,从而实现密码软件安全性形式化的验证。实验结果表明,采用该方法对密码软件的安全性进行验证具有较高的效率,且能够准确地验证密码软件的安全。     

一种基于逻辑编程的防火墙规则形式化分析方法

防火墙作为网络安全体系的基础和核心控制设备,其作用的发挥取决于防火墙规则的正确配置.由于防火墙规则配置的复杂性,导致规则间可能存在冲突,使其不能满足安全目标.文章提出一种基于逻辑编程的防火墙规则形式化分析方法,将安全目标与防火墙规则转换为逻辑程序后加载到推理引擎,制订一系列推理规则,通过提出高级查询进行防火墙规则的冲突检测和正确性验证,并对分析结果进行解释.     

NSSK协议改进及其形式化分析

NSSK协议的主要功能是完成身份的双向认证,提出一种新的攻击方法,并给出改进方案,使之具有更强的安全性,最后应用BAN形式化分析改进的协议是成功有效的。     

开放授权协议OAuth2.0的安全性形式化分析

开放授权协议OAuth是云上一个新的开放标准,解决了用户多账号通用和资源共享的问题.文章针对OAuth2.0的协议规范,利用Alice-Bob标记语言和HLPSL协议高级语言对其进行了形式化描述,并借助基于状态空间搜索的安全协议分析工具,分别讨论了通信三方在使用和未使用HTTPS加密的情况下协议的安全性,对于不安全的情况得到了相应的攻击路径.另外,在实际的网络环境中观察分析了OAuth2.0的相应实现,对国内访问量前100名的网站做了统计,发现其中可以作为OAuth2.0协议服务端的网站有63.6％存在安全漏洞,可以作为客户端的网站有90.2％存在安全漏洞,实验结果对规范网络安全环境有重要的作用和意义.     

NS密码协议的模型检测分析

密码协议安全性的分析是网络安全研究领域的一个主要内容,研究人员提出多种形式化方法来分析这个问题.模型检测工具Spin是一个广泛验证并发系统性质的工具,可用来分析密码协议.对Neeclham-Schroeder(NS)协议认证部分进行了详细的分析,结果表明,Spin可成功检测出NS协议的缺陷,并生成攻击的序列.     

基于NPLAB的Kerberos V5协议的形式化分析

安全协议是建立在密码学基础上的协议,提供主体的身份识别和认证、会话密钥的管理和分配等各种安全服务.NPLAB是一款网络通信协议设计软件,它使用HLPSL语言对安全协议进行建模,采用形式化分析方法分析安全协议,并给出其安全性和可能的攻击路径.以KerberosV5协议为例,对NPLAB的使用进行说明,分析协议的安全性.     

一种形式化分析安全协议的新模型

串空间是安全协议形式化分析的一种新模型．利用次序关系的理论证明了借助串空间模型进行安全协议形式化分析的一个重要结论．通过构造入侵者串的方法,针对Woo-Lam协议提出了一个入侵者串空间模型,同时利用此入侵者串空间模型分析了该协议存在的缺陷,说明了改进后的Woo-Lam协议可克服此缺陷．与现有安全协议形式化分析方法相比较,串空间模型不仅具有简洁直观的优点,而且还可避免状态空间爆炸的问题．     

概率论在Isabelle/HOL中的形式化

基于测度论在Isabelle/HOL/Isar中形式化了概率论,给出了概率空间在Isabelle/HOL中的形式化定义,形式化验证了概率测度的主要性质。形式化验证了测度扩张定理,为在Isabelle/HOL中构造各种概率空间、形式化验证概率算法和概率系统奠定了基础。     

密码协议分析工具--BAN逻辑及其缺陷

在介绍密码协议分析工具——ＢＡＮ逻辑的基础上,研究和分析了ＢＡＮ逻辑在初始假设、理想化步骤、语义和探测协议违规运行等方面所存在的缺陷,并用实际例子具体说明了这些缺陷,最后指出了ＢＡＮ逻辑改进的方向．     

认证协议形式分析的讨论

ＭａｏＷｅｎｂｏ提出了对一种认证协议进行分析时更形式化的ＢＡＮ逻辑，文中对该逻辑进行了分析，并通过举例指出了其局限性．     

安全协议及其形式化分析研究

安全协议是网络安全的重要基础，形式化分析是保证安全协议具备相应安全性质的有效途径。通过对安全协议进行分类，阐述了各类协议所应具备的安全性质；并基于安全协议进行形式化分析时所作的各种假设，综述和分析了三类典型的安全协议形式化方法，给出了安全协议形式化分析研究的发展趋势。     

平衡决策树分类精度与规则简易性研究

本文从实用的角度分析了C4.5算法的不足,提出了平衡决策树分类精度和分类规则简易性的观点。在此基础上,提出一个借助遗传算法进行属性组合寻优、进而实现决策树分类精度与规则简易性平衡的决策树优化算法,并为此设计了一个适应度函数。     

工程网络可靠性分析的网络简化方法

针对含关节点的工程网络可靠性分析,提出了1种冗余子网消除技术。这种简化技术利用关节点进行冗余子网识别和删除,因此网络可靠性可以在精简网络上快速计算。选取USAir97数据集的部分网络进行试验。试验结果表明,利用冗余子网消除技术,可大量降低网络可靠性的计算时间,从而提高网络可靠性分析算法的性能。     

TMN协议的形式化分析

利用运行模式分析法对TMN协议进行了全面的分析，发现了对它的10类19种攻击形式．根据攻击的具体形式和攻击中入侵者的目的对这些攻击进行了归类．结合已知攻击发现，在文中定义的小系统上运行模式分析法对TMN协议的分析是有效的．     

可信计算密码支撑平台中的密钥管理技术研究

介绍了可信计算密码支撑平台中的密钥的分类和结构,着重分析了支持可信计算密码支撑平台的TSM的密钥结构和管理形式.对现有平台密钥管理存在的问题,提出了利用Rootkit 技术加强平台保护的方案.测试结果表明新方法可提高密钥管理的安全性.     

一种双方不可否认密码协议

分析了已有的国内外各种不可否认协议,针对它们存在的共同缺点,提出一个更为完善的密码协议：可运行在不安全信道上实现交易的公平性与通信双方的不可否认性;避免了可信第三方与通信方共享密钥,且保证传递数据的机密性与收发方交易的隐私权;尽量减少可信第三方的工作量和负担,避免了其可能成为系统瓶颈的问题. 协议是安全有效的.     

主动规则的终止性分析

针对主动规则终止性分析方法的局限性,介绍一种主动数据库规则终止性分析的新方法,此方法采用演化图来模拟规则静态处理过程并考虑到激活图和惰化图。最后给出算法来检验规则终止性,并证明算法的正确性。