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

密码协议的一种基于组合推理的模型验证 被引量：2

Model checking based on compositional reasoning for cryptographic protocols
在线阅读 下载PDF
导出
摘要 将密码协议与协议中用到的密码算法视为一个系统,基于组合推理技术建立了密码协议系统的形式化模型。采用基于假设/保证的组合推理技术提出了新的假设/保证推理规则和假设/保证推理算法,证明了该规则的正确性,实现了密码协议系统的模型验证,并重点解决了系统分解问题、假设函数的设定问题等难题。以kerberos v5密码协议系统为例,利用该组合推理技术对密码协议系统进行了安全验证。 A cryptographic protocol together with its cryptographic algorithm was regarded as one system, and based on compositional reasoning techniques, a formal model for the system was built. Using assume-guarantee based compositional reasoning techniques, a new assume-guarantee based reasoning rule and algorithm were proposed, and the soundness of the rule was proved. In realizing model checking to the cryptographic protocol system, several difficulties were solved such as decomposition of the system and generation of assumed function. Using this formal model and assume- guarantee based reasoning techniques, the kerberos v5 cryptographic protocol system was verified.
作者 刘怡文 李伟琴 冯登国
机构地区 北京航空航天大学计算机科学与工程系 中科院软件所信息安全国家重点实验室
出处 《通信学报》 EI CSCD 北大核心 2003年第9期122-127,共6页 Journal on Communications
基金 国家"973"基金资助项目(G1999035802)
关键词 密码协议 形式化模型 组合推理 模型检查 cryptographic protocol formal model compositional reasoning model checking
分类号 TP393.08 [自动化与计算机技术—计算机应用技术]
  • 相关文献

参考文献7

  • 1Schneier B 吴世忠等（译）.应用密码学：协议、算法与C源程序[M].机械工业出版社,2000.368-376.
  • 2SCHNEIER B著 吴世忠等译.应用密码学:协议、算法与C源程序].北京:机械工业出版社,2000..
  • 3DOLEV D, YAO A. On the security of public key protocols[J]. IEEE Trans on Information Theory, 1983,29(2):198-208.
  • 4BEREZIN S, CAMPOS S, CLARKE E. Compositional Reasoning in Model Checking[R]. Technical Report TR CMU-CS-98-106,Carnegie Mellon University, February, 1998.
  • 5GRUMBERG O, LONG D. Model checking and modular verification[J]. ACM Trans on Programming Languages and Systems,1994,16(3):843-871.
  • 6LIU Y W, L1 W Q. The model reasoning verifier for cryptographic protocols[A]. Proceedings of the sixth International Conference for Young Computer Scientist[C]. Hangzhou, 2001. 290-295.
  • 7LOWE G. A hierarchy of authentication specifications[A]. 10th IEEE Computer Security Foundations Workshop Proceedings[C].IEEE Computer Society Press,Rockport,Massachusetts,USA,1997.31-43.

共引文献4

同被引文献27

  • 1Dolev D, Yao A. On the security of public key protocols [J]. IEEE Transactions on Information Theory, 1983,29(2) :198～208
  • 2Benjamin W L. Formal verification of type flaw attacks in security protocols [ J]. Journal of Computer Security, 2003, 11(2): 217～244
  • 3ABADI M, ROGAWAY P. Reconciling two views of cryptography (The computational soundness of formal encryption ) [ C ]//Proe of the 1 st IFIP International Conference on Theoretical Computer Science. IS. 1. 7: Springer, 2000: 3-22.
  • 4ABADI M, JURJENS J. Formal eavesdropping and its computational interpretation [ C ]//Proc of the 4th International Symposium on Theoretical Aspects of Computer Software (TACS). 2001 : 82-94 .
  • 5LAUD P. Symmetric encryption in automatic analyses for confidentiality against active adversaries [ C ]//Proc of 2004 IEEE Symposium on Security and Privacy. 2004 : 71-85.
  • 6MICCIANCIO D, WARINSCHI B. Completeness theorems for the Abadi-Rogaway logic of encrypted expressions[ J ]. Journal of Computer Security, 2004,12( 1 ) :99-129.
  • 7MICCIANCIO D, WARINSCHI B. Soundness of formal encryption in the presence of active adversaries [ C ]//Proc of Theory of Cryptography Conference(TCC). Cambridge, Massachusetts: [ s. n. ] , 2004 : 133-151.
  • 8IMPAGLIAZZO R, KARPON R. Logics for reasoning about cryptographic constructions [ C ]//Proc of STOC' 03. San Diego, California:[s, n. ], 2003: 372-383.
  • 9BACKES M, PFITZMAN B, WAIDNER M. A composable cryptographic library with nested operations (extended abstract )[ C]//Proc of the 10th ACM Conference on Computer and Communications Security. 2003 : 220-230.
  • 10BACKES M, JACOBI C. Cryptographieally sound and machine-assisted verification of security protocols [ C ]//Proc of the 20th Annual Symposium on Theoretical Aspects of Computer Science (STACS). 2003:675-686.

引证文献2

通信学报
2003年 第9期

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

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