共查询到19条相似文献,搜索用时 24 毫秒
1.
网络安全在信息时代非常重要,而网络安全的关键问题之一是安全协议.本文通过串空间模型对KryptoKnight协议进行了分析,得出该协议是安全的.并对串空间模型和BAN逻辑方法进行了比较. 相似文献
2.
随着网络应用的迅速发展,网络安全的问题日益重要.研究下述课题:安全协议的设计原则;安全协议设计中形式化方法的应用;各种形式化分析方法,特别是逻辑分析方法的特点.另外,还探讨了串空间模型在逻辑分析中的应用以及串空间模型指导安全协议形式化设计的可能性. 相似文献
3.
基于串空间的安全协议形式化验证模型及算法 总被引:8,自引:0,他引:8
网络安全在信息时代非常重要,而网络安全的关键问题之一是安全协议。首先介绍了当前安全协议形式化验证的前沿方向--串空间理论,随后阐述了基于该理论设计的自动验证模型--T模型,给出了该模型的算法及描述,并通过验证改进前后的Needham-Schroeder协议来说明T模型的优势。 相似文献
4.
基于串空间的可信计算协议分析 总被引:1,自引:0,他引:1
可信计算技术能为终端、网络以及云计算平台等环境提供安全支撑,其本身的安全机制或者协议应该得到严格的形式化证明.该文基于串空间模型对其远程证明协议进行了分析.首先,扩展了串空间的消息代数和攻击者串,使其能表达可信计算相关的密码学操作,并对衍生的定理进行了证明;并且提出了4个新的认证测试准则,能对协议中的加密、签名、身份生成和哈希等组件进行推理.其次,基于扩展的串空间模型对远程证明协议的安全属性(隐私性、机密性和认证性)进行了抽象和分析.最后,给出了对发现攻击的消息流程,并基于ARM开发板对其中的布谷鸟攻击进行了实现,验证了串空间的分析结果. 相似文献
5.
6.
7.
8.
9.
运用安全协议形式化分析方法中的串空间模型理论,对Natalia Miloslavskaya等人提出的一个双向认证协议进行了分析,发现该协议在认证方面存在缺陷,并对该协议进行了改进,同时用串空间理论证明了改进后的协议的认证正确性. 相似文献
10.
探讨了将串空间模型应用于描述安全协议公平性的方法,并提出串空间模型描述公平协议的一些问题。分析了在描述公平协议时,串空间模型需要进行的几个扩展,包括:描述协议步骤在什么情况可以执行的扩展;描述协议执行过程中角色动态分配的扩展;描述协议步骤同步执行的扩展。应用扩展后的串空间模型对KM协议进行了形式化描述。 相似文献
11.
为了研究Adhoc移动网络路由协议安全性的分析方法,采用串空间理论对Adhoc移动网络路由协议的安全目标进行了形式化描述,提出了Adhoc移动网络路由协议的形式化分析方法,并采用该方法对安全路由协议SRP的安全性进行验证,结果发现了安全路由协议SRP的一个安全漏洞,说明采用串空间理论对Adhoc移动网络路由协议安全性进行分析是有效的。 相似文献
12.
乔海燕 《计算机研究与发展》2008,45(Z1):137-142
使用归纳方法和串空间分别将NSL(Needham-Schroeder-Lowe)协议及其正确性在辅助证明系统Agda中形式化,并比较了这两种安全协议验证法,证明两种方法形式化的正确性和攻击者能力是相同的. 相似文献
13.
Yahalom协议的分析及改进方案 总被引:1,自引:0,他引:1
Yahalom协议及BAN对Yahalom协议的改进协议都存在着安全缺陷.采用串空间模型,运用"理想"和"诚实"作为工具对Yahalom协议的安全性进行了分析并找出了该协议遭受攻击的主要原因,同时提出了Yahalom协议的一种改进方案. 相似文献
14.
首先介绍了当前安全协议形式化验证的前沿方向串空间理论,并运用串空间模型对改进后的Andrew secure RPC协议的机密性进行了形式化分析与验证。 相似文献
15.
操作语义模型是一种用来分析安全协议的新模型,它以操作语义学为基础,结合了多种协议分析模型的优点,能直接分析多个协议的组合问题.本文在对安全协议操作语义模型进行研究的基础上,构建了一个基于结构化操作语义的安全协议分析框架,给出了该框架中的协议规格,协议运行,威胁模型和安全性质等形式化定义.最后,以经典的Needham Schroeder Lowe 协议为例,用该分析框架分析了其机密性和认证性. 相似文献
16.
本文首先介绍了当前安全协议形式化验证的前沿方向串空间理论,并运用串空间模型对改进后的Andrew secure RPC协议进行了形式化分析与验证,然后指出了安全缺陷。 相似文献
17.
为保证移动支付安全、顺利进行,必须采用安全的移动支付协议。针对计算和存储能力有限的移动设备和不可靠的移动环境,选择采用对称加密的轻量级移动支付协议PCMS,使用串空间理论对其建模,进行形式化分析。通过图的方式直观描述协议的执行过程,分析协议安全目标,基于串空间理论的认证测试方法,对该协议的公平性形式化分析。针对PCMS协议不满足公平性,提出增加时间戳来解决,同时增加一个退款子协议完成后续退款操作。结合模型检测工具验证分析,结果表明,改进后的协议满足公平性。 相似文献
18.
通过对串空间模型的扩展,使其具备分析复杂安全协议的能力。利用扩展后的串空间模型,对IEEE802.11i协议中的4步握手协议进行分析,证明4步握手协议达到协议机密性和认证正确性目标的结论。指出在协议可用性分析方面还须继续对分析方法进行扩展研究。 相似文献