期刊文献+

安全协议的形式化分析技术与方法 被引量:62

The Approaches and Technologies for Formal Verification of Security Protocols
在线阅读 下载PDF
导出
摘要 对于安全协议的形式化分析方法从技术特点上做了分类和分析.对于安全协议分析技术的发展历史、目前的状况以及将来的趋势作了总体的介绍和总结.根据作者的体会,从纵向和横向两个角度进行了总结.纵向方面主要是从用于分析安全协议的形式化方法的出现和发展的历史角度加以总结.横向方面主要从所应用的技术手段、技术特点入手,进行总结分析.说明了目前协议形式化分析发展的主要方向.对于目前国际流行的方法和模型进行了例解. The formal methods for verifying security protocols are classified and analyzed from technological points of view. Authors survey the developing history of analyzing approaches and techniques on security protocols; describe the current status, as well as point out the tendency of them. This work comes from authors' personal research interesting, and it processes in two different lines: The first line follows the trace of emergence and developments of formal methods in verification of security protocols. The other line is to analyze the features when concrete systems are used during verification. The most popular methods and systems are briefly introduced by examples.
作者 薛锐 冯登国
出处 《计算机学报》 EI CSCD 北大核心 2006年第1期1-20,共20页 Chinese Journal of Computers
基金 国家自然科学基金(60373048)资助~~
关键词 安全协议 形式化分析 安全目标 Dolev-Yao模型 密码学可靠性 secure protocol formal analysis security goal Dolev-Yao model cryptographic reliability
  • 相关文献

参考文献1

二级参考文献22

  • 1Meadows C A. Formal verification of cryptographic protocols: A survey. In ASIACRYPT: International Conference on the Theory and Application of Cryptology, Wollongong, Australia, LNCS 917, Springer-Verlag, 1994, pp.133-150.
  • 2Burrows M, Abadi M, Needham R. A logic of authentication. ACM Trans. Computer Systems, February 1990, 8:18 36.
  • 3Meadows C. Invariant generation techniques in cryptographic protocol analysis. In the 13th Computer Security Foundations Workshop, IEEE Computer Society,Cambridge, England, July 2000, pp.159-167.
  • 4Meadows C. Language generation and verification in the NRL protocol analyzer. In 9th IEEE Computer Security Foundations Workshop, IEEE Computer Society,Kenmare, Ireland, 1996, pp.48-61.
  • 5Schneider S. Verifying authentication protocols with CSP. In The 10th Computer Security Foundations Workshop, Cambridge, England, IEEE Computer Society, June 1997, pp.l-I5.
  • 6Thayer J, Herzog J, Guttman J. Honest ideals on strand spaces. In 11th IEEE Computer Security Foundations Workshop, IEEE Computer Society, Rockport. Massachusetts, USA, 1998, pp.66-78.
  • 7Paulson L. The inductive approach to verifying cryptographic protocols. Journal of Computer Security, 1998,6(1): 85-128.
  • 8Canetti R. Universally composable security: A new paradigm for cryptographic protocols. In Proc. 42rid FOCS, Las Vegas, Nevada, IEEE, October 2001,pp. 136-145.
  • 9Woo T Y C, Lam S S. A semantic model for authentication protocols. In IEEE Symposium on Research in Security and Privacy, Oakland, May 1993, pp.178-194.
  • 10Bella G, Riccobene E. Formal analysis of the kerberos authentication system. Journal of Universal Computer Science, December 1997, 3:1337 1381.

共引文献4

同被引文献627

引证文献62

二级引证文献153

相关作者

内容加载中请稍等...

相关机构

内容加载中请稍等...

相关主题

内容加载中请稍等...

浏览历史

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