期刊文献+
任意字段
题名或关键词
题名
关键词
文摘
作者
第一作者
机构
刊名
分类号
参考文献
作者简介
基金资助
栏目信息

基于知识结构的认证协议验证 被引量：7

原文传递
导出
摘要 认知逻辑的Kripke语义,已被成功地运用到分析无黑客存在的安全网络下的通信协议.提出认知逻辑的Kripke语义的一种简单而自然的形式,称之为知识结构,并把这种语义用到分析黑客存在的非安全网络环境中的通信协议,特别是认证协议.与类BAN的那一类逻辑相比,文中的方法可以直接转化成算法实现,对协议本身进行操作,而不需对协议进行一些难以把握的抽象判断.而且,在这套理论的基础上开发了安全协议分析器SPV.文中的方法是基于证明的而不是证伪的,即证明协议的正确性而不是找协议漏洞.
作者 苏开乐 吕关锋 陈清亮
机构地区 中山大学计算机科学系
出处 《中国科学（E辑）》 CSCD 北大核心 2005年第4期337-351,共15页 Science in China(Series E)
基金 国家自然科学基金(批准号:60496327 10410638 60473004) 广东省自然科学基金团队项目(批准号:04205407) 教育部留学回国人员科研启动基金 上海市智能信息处理重点实验室(筹)开放课题资助项目
关键词 知识结构 协议验证 Kripke语义 认知逻辑 通信协议 协议分析器 安全网络 网络环境 认证协议 算法实现 直接转化 SPV 正确性 黑客 证明 漏洞
分类号 TN918 [电子电信—通信与信息系统]
  • 相关文献

参考文献3

二级参考文献41

  • 1[1]Meadows, C., A model of computation for the NRL protocol analyzer, in Proceedings of the 1994 Computer Security Foundations Workshop, Franconia, NH, USA, 1994, 84-89.
  • 2[2]Fábrega, F. J. T., Herzog, J. C., Guttman, J. D., Strand spaces: proving security protocols correct, Journal of Computer Security, 1999, 191-230.
  • 3[3]Fábrega, F. J. T., Herzog, J. C., Guttman, J. D., Strand spaces: Why is a security protocol correct? in Proceedings of the 1998 IEEE Symposium on Security and Privacy, IEEE Computer Press, 1998, 160-171.
  • 4[4]Paulson, L. C., The inductive approach to verifying cryptographic protocols, Journal of Computer Security,1998, (6): 85-128.
  • 5[5]Lowe, G., Breaking and fixing the Needham-Schroeder public-key protocol using FDR, in Tools and Algorithms for the Construction and Analysis of Systems, vol. 1055 of Lecture Notes in Computer Science,Berlin: Springer-Verlag, 1996, 147-166.
  • 6[6]Mitchell, J. C., Mitchell, M., Stern, U., Automated analysis of cryptographic protocols using murψ, in Proceedings of the 1997 IEEE Symposium on Security and Privacy, IEEE Computer Society Press, 1997.
  • 7[7]Clarke, E. M., Jha, S., Marrero, W., Verifying security protocols with Brutus, ACM Transactions on Software Engineering and Methodology, 2000, 9(4): 443-487.
  • 8[8]Song, D., Beresin, S., Perrig, A., Athena: a novel approach to efficient automatic security protocol analysis,2001, 9(1,2): 47-74.
  • 9[9]Lowe, G., Towards a completeness result for model checking of security protocols, in Proceedings of 11th IEEE Computer Security Foundation Workshop (CSFW′98), Rockport Massachusetts USA, 1998.
  • 10[10]Durgin, N. A., Lincoln, P. D., Mitchell, J. C. et al., Undecidability of bounded security protocols, in Electronic Proceedings of the Workshop on Formal Methods and Security Protocols, 1999, http:∥www.cs.bell-labs.com/who/nch/fmsp99/program.html.

共引文献47

同被引文献118

引证文献7

二级引证文献6

中国科学（E辑）
2005年 第4期

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

内容加载中请稍等...
;
使用帮助 返回顶部