共查询到20条相似文献,搜索用时 328 毫秒
1.
互联网的迅速发展引起人们对协议安全性的关注,现在国际上流行安全协议的分析方法集中在形式化验证方面,其中BAN逻辑是一种方法。本文通过使用BAN逻辑证明Otway Rees协议的安全性,同时也得出BAN逻辑在证明协议安全性方面的一些缺陷。 相似文献
2.
为了增强通讯网络安全性,研究者致力于通讯协议的形式化分析与验证。 Abdelmajid 在 Kerberos 协议中添加用户物理位置作为新的认证因素得到改进协议,并用改进 BAN 逻辑说明改进协议的安全性。针对添加用户物理位置这一因素进一步完善后的协议 Kerberos *,结合可识别性和管辖性构造一种新的管辖规则,运用改进 GNY 逻辑对协议 Ker-beros *进行安全性分析。分析结果表明,协议 Kerberos *是安全的,运用改进 GNY 逻辑证明过程比改进 BAN 逻辑更详细、更严谨,此方法可运用于其它类似协议形式化分析。 相似文献
3.
4.
5.
6.
用BAN逻辑方法分析SSL3.0协议 总被引:4,自引:1,他引:3
形式化分析密码协议渐渐成为密码学中一个发展的新方向,因为形式化方法的确能检测出密码协议中的漏洞。BAN逻辑是目前使用最广泛的。文章介绍了BAN逻辑和SSL3.0协议,并给出了用BAN逻辑分析SSL3.0协议的详细过程。 相似文献
7.
认证协议的形式化分析* 总被引:5,自引:5,他引:0
认证协议的设计是一项十分困难的工作。国际标准化组织(ISO)一直致力于不同环境的认证协议标准的制定.本文研究用BAN逻辑形式化地分析认证协议的方法,指出BAN逻辑分析并非总是推导出正确的结论.在此基础上,本文讨论了认证协议的设计原则以及改进BAN逻辑的设想. 相似文献
8.
在分析了几种现有的典型RFID安全协议的特点和缺陷的基础上,提出了一种轻量级的RFID安全协议,该协议将一次性密码本与询问一应答机制相结合,实现了安全高效的读取访问控制,最后建立该协议的理想化模型,利用BAN逻辑对该协议进行了形式化分析,在理论上证明其安全性. 相似文献
9.
形式化方法为安全协议分析提供了理论工具,但经过形式化验证过的协议标准在转换为具体程序实现时可能无法满足相应的安全属性.为此,提出了一种检测安全协议代码语义逻辑错误的形式化验证方法.通过将协议C源码自动化抽象为Pi演算模型,基于Pi演算模型对协议安全属性形式化验证.最后,给出了方案转换的正确性证明,并通过对Kerberos协议实例代码验证表明方法的有效性.根据该方案实现了自动化模型抽象工具C2P与成熟的协议验证工具ProVerif结合,能够为协议开发者或测试人员检测代码中的语义逻辑错误提供帮助. 相似文献
10.
11.
针对典型的安全协议验证逻辑存在的问题,如安全属性验证存在局限性、对混合密码原语的处理能力不强等,提出一种新的验证逻辑,新逻辑能够验证安全协议的认证性、密钥保密性、非否认性、可追究性、公平性及原子性。现有多数验证逻辑缺乏形式化语义,而逻辑语义能够证明逻辑系统的正确性,因此给出新逻辑所含逻辑构件的串空间语义,并应用串空间模型证明了新逻辑主要推理规则的正 确性。 相似文献
12.
由于类BAN逻辑缺乏明确而清晰的语义,其语法规则和推理的正确性就受到了质疑。本文定义了安全协议的计算模型,在此基础上定义了符合模态逻辑的类BAN逻辑“可能世界”语义模型,并从语义的角度证明了在该模型下的类BAN逻辑语法存在的缺陷,同时,指出了建立或改进类BAN逻辑的方向。 相似文献
13.
Rafael Accorsi David Basin Luca Vigan 《Electronic Notes in Theoretical Computer Science》2003,55(1):5
We report on work-in-progress on a new semantics for analyzing security protocols that combines complementary features of security logics and inductive methods. We use awareness to model the agents' resource-bounded reasoning and, in doing so, capture a more appropriate notion of belief than those usually considered in security logics. We also address the problem of modeling interleaved protocol executions, adapting ideas from inductive methods for protocol verification. The result is an intuitive, but expressive, doxastic logic for formalizing and reasoning about attacks. As a case study, we use awareness to characterize, and demonstrate the existence of, a man-in-the-middle attack upon the Needham-Schroeder Public Key protocol. This is, to our knowledge, not only the first doxastic analysis of this attack but also the first practical application of an awareness logic. Even though defining the awareness sets of the agents, a task that is left unspecified in formal works on awareness logics, turns out to be surprisingly subtle, initial results suggest that our approach is promising for modeling, verifying and reasoning about security protocols and their properties. 相似文献
14.
SU Kaile Xiao Yinyin Chen Qingliang Lin Han 《Frontiers of Computer Science in China》2007,1(2):191-199
The formal methods for security protocols guarantee the security properties of protocols. Instantiation Space Logic is a new
security protocol logic, which has a strong expressive power. Compositional Logic is also a useful security protocol logic.
This paper analyzes the relationship between these two logics, and interprets the semantics of Compositional Logic in Instantiation
Space model. Through our work, the interpreted Compositional Logic can be extended more easily. Moreover, those security protocols
described in Compositional Logic can be automatically verified by the verifier of Instantiation Space. The paper also proves
that the expressive power of Instantiation Space Logic, which can not be completely interpreted by Compositional Logic, is
stronger than Compositional Logic. 相似文献
15.
BAN类逻辑是近年来主要的密码协议分析工具之一,在分析了BAN逻辑存在的各类缺陷并用实例详细说明的基础上,研究和归纳了各种扩展的BAN类逻辑的特点和他们共同的缺陷,指出了BAN类逻辑应该改进的方面以及今后进一步的研究方向。 相似文献
16.
17.
SU Kaile Lü Guanfeng & CHEN Qingliang Department of Computer Science Sun Yat-sen University Guangzhou China 《中国科学F辑(英文版)》2005,48(4):513-532
~~Knowledge structure approach to verification of authentication protocols1. Hintikka, J., Knowledge and Belief, Ithaca, NY. Cornell University Press, 1962.
2. Fagin, R., Halpern, J., Moses, Y. et al.,Reasoning About Knowledge, Cambridge, MA. MIT Press, 1995.
3. Halpern, I., Zuck, L., A little knowledge goes a long way. Simple knowledge based derivations and correctness proofs for a family of protocols. Journal of the ACM, 1992, 39(3): 449-478.
4. Stulp, F., Verbrugge, … 相似文献
18.
19.
20.
安全协议的可视化分析和设计研究 总被引:1,自引:0,他引:1
基于模态逻辑的安全协议形式化分析方法一直备受关注。本文在简述一个基于GNY逻辑实现的可视化集成工具的基础上,以SSL协议为例,详细阐述其自动分析过程。最后,就工具不能自动执行第三方信任逻辑的情况,提出了简单的可信第三方参与的扩展逻辑,为复杂安全协议的可视化分析和设计提供参考。 相似文献