共查询到19条相似文献,搜索用时 140 毫秒
1.
针对认证测试基础理论在协议主体串参数一致性分析方面,因形式化判定规则不足所产生的分析复杂度较高和自动化程度较低问题,通过对消息组件结构的形式化,以及认证测试结构的共性分析,基于认证测试基础理论对认证测试结构进行形式化建模;在认证测试结构模型上,运用协议主体密钥的认证测试构造规则,分析协议主体串在不同类型参数上满足一致性的条件,在明确参数一致性判定规则的同时,给出协议主体串参数一致性分析的形式化方法。协议分析实践表明,该方法较传统方法不仅具有简洁高效、易于自动化实现的优点,而且能够准确定位协议缺陷并给出相应的修正方案。 相似文献
2.
3.
介绍了wi—Fi联盟的WPS标准并给出了对应的攻击方法——暴力破解攻击,使用CPN对WPS协议及改进协议进行形式化分析并证明AP限制重新发起连接认证的次数为3次时,原协议可完全被攻破而给出的改进协议成功概率仅约为3/10^8。 相似文献
4.
无线射频识别(RFID)是物联网中的一种非接触式的自动识别技术,被广泛运用于构建物物互联的RFID系统。RCIA是一种超轻量级RFID双向认证协议,提供高安全性并声称能抵御去同步攻击。形式化方法是安全协议分析的有力手段。运用模型检测工具SPIN对RCIA协议的认证性及一致性进行验证,结果表明RCIA协议存在去同步攻击漏洞。针对此漏洞,提出基于密钥同步机制的修补方案,对RCIA协议进行了改进。对改进后的协议进行形式化分析与验证,结果表明改进后的RCIA协议具有更高的安全性。提出的协议抽象建模方法对此类超轻量级RFID双向认证协议形式化分析具有重要借鉴意义;提出的基于密钥同步机制的漏洞修补方案,被证明能有效抵御去同步漏洞,可适用于此类超轻量级RFID双向认证协议的设计和分析。 相似文献
5.
6.
通过分析文献[1]中Wang提出的一个匿名移动无线认证方案中的Hand-Off认证协议,发现了其存在安全漏洞,无法抵抗中间人发起的重放攻击,针对该协议存在的安全漏洞对原协议进行了改进,改进后的协议可以安全的实现用户与机站之间的身份认证,并可以有效地抵抗中间人发起的重放攻击。 相似文献
7.
8.
安全协议是现代网络安全的基础,密码协议的安全性证明是一个挑战性的问题。事件逻辑是一种描述分布式系统中状态迁移的形式化方法,用于刻画安全协议的形式化描述,是定理证明的基础。用事件序语言、事件类和一个表示随机数、密钥、签名和密文的原子类,给出身份认证协议可以被形式化定义和强认证性证明理论。利用该理论对增加时间戳的Needham-Schroeder协议安全性进行证明,证明改进的Needham-Schroeder协议是安全的。此理论适用于类似复杂协议形式化分析与验证。 相似文献
9.
运用安全协议形式化分析方法中的串空间模型理论,对Natalia Miloslavskaya等人提出的一个双向认证协议进行了分析,发现该协议在认证方面存在缺陷,并对该协议进行了改进,同时用串空间理论证明了改进后的协议的认证正确性. 相似文献
10.
11.
认证测试是一种用于证明安全协议认证属性的新方法,该方法能够简化协议认证属性的证明过程,但其局限性是无法应用于认证测试元素被多重加密的情况.指出Perrig和Song提出的认证测试改进方案在多个方面所存在的问题.在此基础上提出新的改进方案,并进行了形式化证明.新的认证测试定理突破了认证测试元素在整个协议消息中不能被加密的限制,扩展了认证测试理论的应用范围. 相似文献
12.
基于认证测试的安全协议分析 总被引:9,自引:0,他引:9
认证测试是一种新型的在Strand空间模型基础上发展而来的安全协议分析与辅助设计技术,可用于大部分协议的关联属性的分析;但是与Strand空间模型一样,它主要用于协议正确性证明,在协议为何不正确以及如何进行改进这个问题上处理分析能力较弱.在认证测试概念的基础上,结合逻辑分析的优点,提出了增强型认证测试EAT(enhanced authentication test)和Correspondence函数等概念来对安全协议进行关联属性的分析,很好地解决了这一问题与原有技术相比,该方法更为形式化,协议分析人员可以很方便地进行手动分析,并且更有利于协议分析自动化工具的实现. 相似文献
13.
14.
采用认证测试方法对X.509协议的认证正确性进行了分析,该方法比BAN逻辑分析得到的结论更具体,比传统串空间理论构造集合寻找M-minimal元素的方法更为简单直观。然后针对分析结论提出了改进协议,并使用认证测试方法证明了改进协议在保持数据保密性完整性的同时,也能实现认证的正确性。 相似文献
15.
在应用中,当关键原子值发生多次形式转换时,需要进行多次认证测试。鉴于此,本文引入了关键分量(Key Component)的概念,提出了多重认证测试(Multiple Authentication Test)方法。使用该方法重新设计了Woo-Lam协议,通过两个“挑战-响应”回合,确保主体角色的非对称性和响应者对发起者的身份认证。设计出的Woo-Lain协议不仅避免了原协议经认证测试方法改进后存在的缺少主体标识的缺陷,而且避免了Abadi和Buttyan等人分别对原协议改进后存在的两个重放攻击。 相似文献
16.
Hua GuoAuthor Vitae Chang XuAuthor VitaeYi MuAuthor Vitae Zhoujun LiAuthor Vitae 《Computers & Electrical Engineering》2012,38(3):563-572
Designing elliptic curve password-based authenticated key agreement (ECPAKA) protocols for wireless mobile communications is a challenging task due to the limitation of bandwidth and storage of the mobile devices. Some well-published ECPAKA protocols have been proved to be insecure. We notice that until now none of the existing ECPAKA protocols for wireless mobile communication is provided any formal security analysis. In this paper, we propose a novel protocol and conduct a formal security analysis on our protocol. Compared with other ECPAKA protocol, our protocol meets all basic security properties and is the first ECPAKA protocol with formal security proof for wireless communication. We also explore the suitability of the novel protocol for 3GPP2 specifications and improve the A-Key (Authentication Key) distribution for current mobile cellular systems. 相似文献
17.
18.
网络的飞速发展,使得安全问题日益突出,而身份认证协议则是安全性的基础。目前国际上的热点是安全协议的形式化验证。文章从两个角度介绍安全协议形式化验证的方法:证明与证伪。对其各自特点进行比较与分析。 相似文献