期刊文献+

Otway-Rees协议改进及形式化证明 被引量:3

Improvement and formal proof on protocol Otway-Rees
下载PDF
导出
摘要 选取认证密钥分配协议Otway-Rees协议作为研究对象,利用协议组合逻辑(PCL)作为协议证明工具,对安全协议形式化分析及证明进行了研究。首先给出了Otway-Rees协议常见的攻击形式,分析了存在的缺陷,提出了改进方案(AOR协议);然后,为了更好地形式化描述AOR协议,对传统的PCL进行一定的扩展;紧接着,用扩展后的PCL对改进的协议中各个实体的行为和协议的安全属性进行形式化描述,将改进后的协议进行模块化划分,并利用PCL进行组合证明;最后,得出改进后的AOR协议具有密钥保密属性。 选取认证密钥分配协议Otway-Rees协议作为研究对象,利用协议组合逻辑(PCL)作为协议证明工具,对安全协议形式化分析及证明进行了研究。首先给出了Otway-Rees协议常见的攻击形式,分析了存在的缺陷,提出了改进方案(AOR协议);然后,为了更好地形式化描述AOR协议,对传统的PCL进行一定的扩展;紧接着,用扩展后的PCL对改进的协议中各个实体的行为和协议的安全属性进行形式化描述,将改进后的协议进行模块化划分,并利用PCL进行组合证明;最后,得出改进后的AOR协议具有密钥保密属性。
出处 《通信学报》 EI CSCD 北大核心 2012年第S1期250-254,共5页 Journal on Communications
基金 国家自然科学基金资助项目(61173190) 陕西省自然科学基金资助项目(2009JM8002 2012JQ8023) 中央高校基本科研业务费基金资助项目(GK200902051 GK201002041 GK201002037)~~
关键词 安全协议 形式化方法 协议组合逻辑 OTWAY-REES协议 security protocol formal methods protocol composition logic protocol Otway-Rees
  • 相关文献

参考文献2

二级参考文献6

共引文献117

同被引文献21

  • 1李建华,张爱新,薛质.网络安全协议的形式化分析与验证[M].北京:机械工业出版社,2010.
  • 2王建华,张岚,何良生,许旸.基于广义串空间模型构造攻击的缺陷及改进[J].电子与信息学报,2007,29(10):2451-2454. 被引量:1
  • 3Burrows M, Abadi M, Needham R. A Logic of Authentication[J]. ACM Trans, on Computer Systems, 1990, 8( 1 ) : 18-36.
  • 4Gong L, Needham R, Yahalom R. Reasoning about belief in cryptographic protocols[ C ]//Proceedings of 1990 IEEE Sympo- sium on Research in Security and Privacy. 1990: 234-245.
  • 5Syverson P F,Oorschot P C van. On unifying, some cryptographic protocol logics[ C]//Proceedings of 1994 IEEE Symposium on Research in Security and Privacy. 1994: 14-28.
  • 6Yap R. Extending BAN Logic for Reasoning with Modern PKI-Based Protocols[ C ]//Network and Parallel Computing. 2008: 190-197.
  • 7Claycomb W, Shin I). Extending formal analysis of mobile device authentication[ J]. Journal of Internet Services and Informa- tion Security ( JISIS), 2011, 1 ( 1 ) : 86-102.
  • 8Cohen M, Dam M. A Completeness Result for BAN Logic [ C ]//Proceedings of Methods for Modalities. 2005:202-219.
  • 9Otway D, Rees O. Efficient and timely mutual authentication[ J]. Operating Systems Review, 1987, 21 (1) :8-10.
  • 10李谢华,高春鸣.基于改进认证测试理论的高效安全协议验证算法[J].计算机科学,2009,36(4):73-76. 被引量:3

引证文献3

二级引证文献8

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

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