微信服务号

微信订阅号

2025年3月24日 16:48 星期一
首页 > 过刊浏览>2003年第14卷第7期 >1300-1309
PDF HTML阅读 XML下载 导出引用 引用提醒
安全协议的设计与逻辑分析
作者:
基金项目:

(Supported by the National Natural Science Foundation of China under Grant No.60083007 (国家自然科学基金); the National Grand Fundamental Research 973 Program of China under Grant No.G1999035810 (国家重点基础研究发展规划(973))


Design and Logical Analysis of Security Protocols
Author:
  • 摘要
    • | |
  • 访问统计
    • |
  • 参考文献 [40]
    • |
  • 相似文献
    • |
  • 引证文献
    • | |
  • 文章评论
    摘要:

    随着网络应用的迅速发展,网络安全的问题日益重要.研究下述课题:安全协议的设计原则;安全协议设计中形式化方法的应用;各种形式化分析方法,特别是逻辑分析方法的特点.另外,还探讨了串空间模型在逻辑分析中的应用以及串空间模型指导安全协议形式化设计的可能性.

    Abstract:

    With the rapid growth of network applications, network security has become an important issue. In this paper, the following issues are investigated: the design principles of security protocols, the use of formal methods in the design of security protocols, the characteristics of various approaches to formal analysis, in particular logical analysis. The strand space approach to logical analysis, and the possibility of the strand space model guiding the formal design of security protocols are also explored.

    参考文献
    [1]Qing, SH. Cryptography and Computer Network Security. Beijing: Tsinghua University Press, 2001. 127～147 (in Chinese).
    [2]Qing, SH. Formal analysis of authentication protocols. Journal of Software, 1996,7:107～114 (in Chinese with English abstract).
    [3]Meadows C. Formal verification of cryptographic protocols: A survey. In: Advances in Cryptology, Asiacrypt'96 Proceedings. LNCS 1163, Berlin: Springer-Verlag, 1996, 135～150.
    [4]Thayer FJ, Herzog JC, Guttman JD. Strand spaces: Why is a security protocol correct? In: Proceedings of the 1998 IEEE Symposium on Security and Privacy. Los Alamitos: IEEE Computer Society Press, 1998. 160～171.
    [5]Thayer FJ, Herzog JC, Guttman JD. Strand spaces: Proving security protocols correct. Journal of Computer Security, 1999,7(2-3): 191～230.
    [6]Burrows M, Abadi M, Needham R. A logic of authentication. Research Report 39, Digital Systems Research Center, 1989.
    [7]Gong L, Needham R, Yahalom R. Reasoning about belief in cryptographic protocols. In: Proceedings of the 1990 IEEE Computer Society Symposium on Research in Security and Privacy. Los Alamitos: IEEE Computer Society Press, 1990. 234～248.
    [8]Abadi M, Tuttle MR. A semantics for a logic of authentication. In: Proceedings of the 10th ACM Symposium on Principles of Distributed Computing. ACM Press, 1991. 201～216.
    [9]van Oorschot PC. Extending cryptographic logics of belief to key agreement protocols. In: Proceedings of the 1st ACM Conference on Computer and Communications Security. ACM Press, 1993. 233～243.
    [10]Syverson, PF, van Oorschot PC. On unifying some cryptographic protocol logics. In: Proceedings of the 1994 IEEE Computer Society Symposium on Research in Security and Privacy. Los Alamitos: IEEE Computer Society Press, 1994. 14～28.
    [11]Dolev D, Yao A. On the security of public key protocols. IEEE Transactions on Information Theory, 1983,29(2):198～208.
    [12]Syverson P. A taxonomy of replay attacks. In: Proceedings of the Computer Security Foundations Workshop. Los Alamitos: IEEE Computer Society Press, 1994. 187～191.
    [13]Wang GL, Qing SH, Zhou ZF. Some new attacks upon authentication protocols. Journal of Software, 2001,12(6):907～913 (in Chinese with English abstract).
    [14]Clark J, Jacob J. A survey of authentication protocol literature: Version 1.0. 1997. http://www-users.cs.york.ac.uk/～jac/under the link\Security Protocols Review.
    [15]Needham R, Schroeder M. Using encryption for authentication in large networks of computers. Communications of the ACM, 1978, 21(12):993～999.
    [16]Lowe G. Breaking and fixing the Needham-Schroeder public-key protocol using FDR. Software??Concepts and Tools, 1996,17: 93～102.
    [17]Nessett DM. A critique of the burrows, Abadi and Needham logic. ACM Operating Systems Review, 1990,24(2):35～38.
    [18]Syverson P. Knowledge, belief, and semantics in the analysis of cryptographic protocols. Journal of Computer Security, 1992,1(3): 317～334.
    [19]Bieber P. A logic of communication in a hostile environment. In: Proceedings of the Computer Security Foundations Workshop III. Los Alamitos: IEEE Computer Society Press, 1990. 14～22.
    [20]Syverson P. Formal semantics for logics of cryptographic protocols. In: Proceedings of the Computer Security Foundations Workshop III. Los Alamitos: IEEE Computer Society Press, 1990. 32～41.
    [21]Rangan PV. An axiomatic basis of trust in distributed systems. In: Proceedings of the 1988 Symposium on Security and Privacy. Los Alamitos: IEEE Computer Society Press, 1988. 204～211.
    [22]Moser L. A logic of knowledge and belief for reasoning about computer security. In: Proceedings of the Computer Security Foundations Workshop II. Los Alamitos: IEEE Computer Society Press, 1989. 57～63.
    [23]Yahalom R, Klein B, Beth T. Trust relationships in secure systems: A distributed authentication perspective. In: Proceedings of the 1993 IEEE Symposium on Security and Privacy. Los Alamitos: IEEE Computer Society Press, 1993. 150～164.
    [24]Kindred D. Theory generation for security protocols [Ph.D. Thesis]. Pittsburgh: Department of Computer Science, Carnegie Mellon University, 1999.
    [25]CCITT. CCITT draft recommendation X.509. The directory-authentication framework, Version 7, 1987.
    [26]Burrows M, Abadi M, Needham R. Rejoinder to Nessett. Operating Systems Review, 1990,24(2):39～40.
    [27]Diffie W, Hellman ME. New directions in cryptography. IEEE Transactions on Information Theory, 1976,IT-22(6):644～654.
    [28]Doraswamy N, Harkins D. IPSEC: The New Security Standard for the Internet, Intranets, and Virtual Private Networks. Prentice Hall, Inc., 1999.
    [29]Gollmann D. What do we mean by entity authentication? In: Proceedings of the IEEE Symposium on Security and Privacy. Los Alamitos: IEEE Computer Society Press, 1996. 46～54.
    [30]Lowe G. A hierarchy of authentication specifications. In: Proceedings of the 10th IEEE Computer Security Foundations Workshop. Los Alamitos: IEEE Computer Society Press, 1997. 31～43.
    [31]Zhou J, Gollmann D. Towards verification of non-repudiation protocols. In: International Refinement Workshop and Formal Methods Pacific 1998. Berlin: Springer-Verlag, 1998. 370～380.
    [32]Qing, SH. A new non-repudiation protocol. Journal of Software, 2000,11(10):1338～1343 (in Chinese with English abstract).
    [33]Syverson PF. Towards a strand semantics for authentication logic. Electronic Notes in Theoretical Computer Science, 2000,20: 62～72.
    [34]Thayer FJ, Herzog JC, Guttman JD. Strand spaces: Honest ideals on strand spaces. In: Proceedings of the 1998 IEEE Computer Security Foundations Workshop. Los Alamitos: IEEE Computer Society Press, 1998. 66～77.
    [35]Heintze N, Tygar, JD. A model for secure protocols and their composition. IEEE Transactions on Software Engineering, 1996, 22(1):16～30.
    [36]Guttman JD, Thayer FJ. Authentication tests. In: Proceedings of the 2000 IEEE Symposium on Security and Privacy. Los Alamitos: IEEE Computer Society Press, 2000. 150～164.
    [37]卿斯汉.密码学与计算机网络安全.北京:清华大学出版社,2000.127～147.
    [38]卿斯汉.认证协议的形式化分析.软件学报,1996,7:107～114.
    [39]王贵林.卿斯汉,周展飞.认证协议的一些新攻击方法.软件学报,2001,12(6):907～913.
    [40]卿斯汉.一种新型的非否认协议.软件学报,2000,11(10):1338～1343.
    相似文献
    引证文献
引用本文

卿斯汉.安全协议的设计与逻辑分析.软件学报,2003,14(7):1300-1309

复制
分享
文章指标
  • 点击次数:8184
  • 下载次数: 9647
  • HTML阅读次数: 0
  • 引用次数: 0
历史
  • 收稿日期:2003-01-23
  • 最后修改日期:2003-01-23
文章二维码
友情链接:中国科学院软件研究所中国计算机学会中国科学院国家自然科学基金委员会CCF数字图书馆Int'l J of Softw Info计算机系统应用
您是第位访问者
版权所有：中国科学院软件研究所 京ICP备05046678号-3
地址：北京市海淀区中关村南四街4号,邮政编码：100190
电话：010-62562563 传真：010-62562533 Email：jos@iscas.ac.cn
技术支持：北京勤云科技发展有限公司

京公网安备 11040202500063号