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

基于Strand空间的认证协议证明方法研究 被引量：5

Study on the Proof Method of Authentication Protocols Based on Strand Space
下载PDF
导出
摘要 Strand空间是一种新的安全协议分析模型.系统研究了使用Strand空间模型证明认证协议存在缺陷的方法.在证明过程中,使用目标细化方法证明了认证属性.通过在该模型中引入消息类型检查机制,简化了证明过程.并将该方法应用到包含三方主体的认证协议.最后得出与相关文献相同的结论. Strand space is a new model for the analysis of security protocols. In this paper, a systematic study is made on how to prove the existence of vulnerabilities in authentication protocols based on the Strand space. During the proof procedure, the authentication property is proved by using the goal-refined method. Moreover, by introducing type-check mechanism into this model, the proof procedure is simplified significantly. In addition, this method is also applied to authentication protocols involved three principals. At last, the same results are got as the relevant literatures.
作者 刘东喜 白英彩
机构地区 上海交通大学计算机科学与工程系
出处 《软件学报》 EI CSCD 北大核心 2002年第7期1313-1317,共5页 Journal of Software
基金 国家S219工程资助项目(2000-A32-09)
关键词 STRAND空间 认证协议 协议证明 形式化方法 密码 信息安全 Strand space authentication protocol protocol proof formal method
分类号 TP309 [自动化与计算机技术—计算机系统结构]
  • 相关文献

参考文献7

  • 1[1]Lowe, G. An attack on the needham-schroeder public key authentication protocol. Information Processing Letters, 1995,56(3): 131～136.
  • 2[2]Gritzalis, S., Spinellis, D., Georgiadis, P. Security protocols over open networks and distributed systems: formal methods for their analysis, design, and verification. Computer Communications, 1999,22(8):695～707.
  • 3[3]Burrows, M., Abadi, M., Needham, R. A logic of authentication. ACM Transactions on Computer Systems, 1990,8(1):18～36.
  • 4[4]Clarke, E.M., Jha, S., Marrero, W. Using state space exploration and a natural deduction style message derivation engine to verify security protocols. In: Proceedings of the IFIP Working Conference on Programming Concepts and Methods (PROCOMET). New York, 1998. http://www.cs.cmu.edu/～Emarrero/procomet.ps.gz.
  • 5[5]Thayer, F., Herzog, J.C., Guttman, J.D. Strand space: why is a security protocol correct? In: Proceedings of the 1998 IEEE Symposium on Security and Privacy. 1998. 160～171.
  • 6[6]F'abrega, F.J.T., Herzog, J.C., Guttman, J.D. Strand space pictures. In: Workshop on Formal Methods and Security Protocols. Indianapolis, Indiana, 1998. http://www.cs.bell-labs.com/who/nch/fmsp/8-guttman.ps.
  • 7[7]Thomas, Y.C.W., Simon, S.L. A semantic model for authentication protocols. In: Proceedings of the 14th IEEE Symposium on Research in Security and Privacy. Oakland: IEEE Computer Society Press, 1993. 178～194.

同被引文献57

  • 1李梦君,李舟军,陈火旺.基于进程代数安全协议验证的研究综述[J].计算机研究与发展,2004,41(7):1097-1103. 被引量：25
  • 2李梦君,李舟军,陈火旺.基于逻辑程序的安全协议验证[J].计算机学报,2004,27(10):1361-1368. 被引量：7
  • 3R W Cleaveland,P Lewis,S Smolka et al.The concurrency factory:a development environment for concurrent systems[C].In:Alur and Henzinger[6], 398～401
  • 4R W Cleaveland,S Sims.The NCSU concurrency workbench[C].In:Alur and Henzinger[6] ,394～397
  • 5J Yang,A Mok,F Wang. Symbolic model checking for event-driven real-time systems[C].In:IEEE Real-Time Systems Symposium,IEEE Computer Society Press, 1993
  • 6Alur C Coureoubetis,D L Dill.Model-checking for real-time systems[C].In:Proceedings of the 5th Annual Symposium on Logic in Computer Science,IEEE Computer Society Press,1990:414～425
  • 7David L Dill.timing assumptions and verification of finite-state concurrent systems[C].In:J Sifakis ed. Proceedings of the international Workshop on Automatic Verification Methods for Finite State Systems,LNCS 407,1989:197～212
  • 8D Dolev,A Yao. On the security of Public Key Protocols[J].IEEE Transaction on information Theory, 1989;29(2): 198～208
  • 9G Lowe .Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR[C].In:Proceedings of TACAS,LNCS 1055,SpringerVerlag, 1996:147～166
  • 10S Lu,S Smolka. Model checking the Secure Electronic Transaction (SET)Protocol[C].In:Proceedings of the Seventh International Symposium on Modeling,Analysis and simulation of Computer and Telecommunication Systems, 1999

引证文献5

二级引证文献31

软件学报
2002年 第7期

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

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