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

密码协议的代数模型及其安全性 被引量：1

原文传递
导出
摘要 引入了一个新的代数系统——称为密码协议代数(cryptographic protocolalgebra,CPA),刻画具有多种密码运算的消息代数性质,并基于CPA提出了一个新的密码协议代数模型.模型中,用子代数、自由生成元和多项式代数等概念刻画主体的知识扩张过程,并用类似于代数中的正合序列概念描述了密码协议的攻击过程,从而为密码协议的安全性分析建立了一种数学方法.基于这个模型,利用代数的技巧证明了对于具有一定对称性的协议,任意多主体参与运行的协议安全性分析可归结为几个主体与攻击者参与的协议安全性分析.研究了密码协议安全的一致性问题,给出了两个协议合成保持安全性的一个充分条件,并提供两个安全的密码协议的合成安全的例子,推广了相关工作.
作者 怀进鹏 李先贤
机构地区 北京航空航天大学计算机科学与工程系
出处 《中国科学（E辑）》 CSCD 北大核心 2003年第12期1087-1106,共20页 Science in China(Series E)
基金 国家自然科学基金(批准号:60073006) 国家"八六三"高技术研究发展计划(2001AA144150)资助项目
关键词 代数模型 密码协议 形式化分析 信息安全 分布式系统
分类号 TN918.1 [电子电信—通信与信息系统]
  • 相关文献

参考文献16

  • 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′abrega 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′abrega 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. Oakland: 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, volume 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. Journal of Computer Security, 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

同被引文献5

  • 1李梦君,李舟军,陈火旺.安全协议的扩展Horn逻辑模型及其验证方法[J].计算机学报,2006,29(9):1666-1678. 被引量：7
  • 2冯登国,范红.安全协议理论与方法[M].北京:科学出版社.2003.
  • 3YASINSEC A. A formal semantics for evaluating eryptographic protocols[D]. University of Virginia, 1996.
  • 4MILLEN J. CAPSL: common authentication protocol specification language [R]. Technical Report MP97B48, The MITRE Corporation, 1997.
  • 5Wei Jin, Su Guiping. An integrated model to analyze eryptographic protocols with colored Petri Nets. In Proceeing [C]. l lth IEEE Symposium on High Assurance Systems Engineering Symposium, 2008.

引证文献1

二级引证文献2

中国科学（E辑）
2003年 第12期

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

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