共查询到17条相似文献,搜索用时 62 毫秒
1.
基于逻辑程序的安全协议验证 总被引:5,自引:1,他引:4
安全协议本质上是分布式并发程序,可以自然地描述为多个子进程的并发合成系统.将安全协议对应的并发合成系统抽象为逻辑程序进行消解,能够对安全协议无穷多个会话的交叠运行进行验证.该文提出了安全协议逻辑程序中逻辑规则的一个分类方法,基于该分类方法提出了安全协议逻辑程序不动点的迭代计算方法.逻辑规则的分类优化了安全协议逻辑程序不动点的迭代计算和安全性质验证过程中的计算.由于安全协议逻辑程序不动点迭代计算过程不一定终止,文中提出了每进行k≥1步安全协议逻辑程序不动点迭代计算验证一次安全性质的验证策略. 相似文献
2.
安全协议验证是网络安全领域中重大课题之一,目前对安全协议进行分析的主流方法是形式化方法。该文对现在常用的几种形式化验证方法进行了概述和分析,最后针对形式化技术在该领域的发展前景提出了自己的见解。 相似文献
3.
安全协议中的形式化验证技术 总被引:1,自引:0,他引:1
伴随着网络和通信的迅速发展,安全已经成为一个备受关注的问题,为确保不同系统的安全,出现了许多的安全协议。文中描述了安全协议验证的形式化需求,并且详细阐述了目前流行的几种形式化的验证技术及各自的优缺点,探讨了形式化验证技术所面临的挑战,指出目前在这方面所做的工作以及有待发展的方向。 相似文献
4.
安全协议的形式化说明、设计及验证 总被引:3,自引:0,他引:3
文中针对形式化技术在安全协议说明、设计和验证三个方面的研究和进展情况进行了详细介绍,分析了它们的原理和优缺点,并对该技术的研究发展前景提出见解。 相似文献
5.
一个安全、原子的电子商务协议及其形式化验证 总被引:11,自引:0,他引:11
电子商务的普及与接受主要取决于下述属性的解决:安全、原子、隐私与匿名,形式化描述和分析是描述电子商务协议并验证它各性的有效方法,面向物理商品交易的电子商务协议需要具备3个属性:安全、原子和隐私,介绍了一个安全、可靠的电子商务协议BEARCAT及其形式化描述,并龙有人侵者的情况下,通过用BAN类型的逻辑证明所期望的属性的方式对协议的强度和正确性作形式化分析。 相似文献
6.
7.
形式化方法能有效检验安全协议的安全性,BAN类逻辑的发展极大地促进了这一领域的研究,但是现有的BAN类逻辑仍然存在许多问题.在分析现有BAN类逻辑的基础上,提出一种新的安全协议形式化验证方法,实现现有BAN类逻辑的验证功能,并使安全协议验证工作简单可行,便于实现机器自动验证.为安全协议形式化验证提供了一种新的途径. 相似文献
8.
介绍了安全协议形式化分析方法,给出了一个自动化分析集成工具。该工具基于模态逻辑实现自动推理,采用可视化框架描述协议体。重点分析了该软件的模块结构和工作原理,可为形式化分析工具的设计和开发提供参考。 相似文献
9.
安全协议的扩展Horn逻辑模型及其验证方法 总被引:5,自引:1,他引:5
分析了Bruno Blanchet和Martin Abadi提出的基于Horn逻辑的安全协议模型及其验证方法,针对它们构造不满足安全性质的安全协议反例的不足,提出了安全协议的扩展Horn逻辑模型和修改版本的安全协议验证方法,使得能够从安全协议的扩展Horn逻辑模型和修改版本的安全协议验证过程中自动构造不满足安全性质的安全协议反例.在基于函数式编程语言Objective Carol开发的安全协议验证工具SPVT中,实现了上述算法,验证了算法的正确性. 相似文献
10.
伴随着网络和通信的迅速发展,安全已经成为一个备受关注的问题,为确保不同系统的安全,出现了许多的安全协议.文中描述了安全协议验证的形式化需求,并且详细阐述了目前流行的几种形式化的验证技术及各自的优缺点,探讨了形式化验证技术所面临的挑战,指出目前在这方面所做的工作以及有待发展的方向. 相似文献
11.
安全协议认证的形式化方法研究 总被引:6,自引:0,他引:6
安全协议认证是网络安全领域中重大课题之一。形式化方法多种多样。该文首先论述了模型检测技术及其在安全协议验证中的应用,然后介绍了各种定理证明方法和定理证明工具,接着讨论其它形式化验证方法,最后论述形式化方法的一些研究方向。 相似文献
12.
形式化方法是确保安全协议设计正确性的重要工具,利用形式化方法已经发现了许多安全协议的设计错误.首次利用形式规约语言Z对RFID安全协议HB进行形式规约, 并对HB协议应该满足的安全性质进行形式化描述,使用Z模式推理从协议及其运行环境两个方面验证了协议的关键安全属性,发现了HB协议在设计方面的缺陷,提出了HB协议的一种改进方法. 相似文献
13.
基于进程代数安全协议验证的研究综述 总被引:14,自引:2,他引:14
安全协议用于实现开放互联网络的通信安全,进程代数是一类使用代数方法研究通信并发系统理论的泛称,基于进程代数的安全协议验证是以进程代数作为安全协议描述语言的安全协议形式化验证方法.描述了基于进程代数的安全协议验证研究的4种主要方法:基于踪迹语义的方法;基于互模拟验证的方法;基于类型理论的方法;基于逻辑程序的方法.并给出了基于进程代数的安全协议验证进一步的研究方向. 相似文献
14.
15.
16.
17.
基于口令的远程身份认证协议是目前认证协议研究的热点。2005年,Sung-Woon Lee等人提出了一个低开销的基于随机数的远程身份认证协议即Lee-Kim-Yoo协议,首先分析了此协议中所存在的安全性缺陷,随后构造了一个基于随机数和Hash函数,并使用智能卡的远程身份认证协议,最后用BAN逻辑对修改后的协议进行了形式化的分析,结果表明修改后的协议能够达到协议的安全目标。 相似文献