微信服务号

微信订阅号

2025年3月24日 17:17 星期一
首页 > 过刊浏览>2003年第14卷第10期 >1740-1752
PDF HTML阅读 XML下载 导出引用 引用提醒
安全协议20年研究进展
作者:
基金项目:

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))


Twenty Years Development of Security Protocols Research
Author:
  • 摘要
    • | |
  • 访问统计
    • |
  • 参考文献 [84]
    • |
  • 相似文献 [20]
    • |
  • 引证文献
    • | |
  • 文章评论
    摘要:

    总结了安全协议的20年研究进展情况,指出形式化方法在安全协议的设计与分析中的重要应用.对安全协议的若干热点研究方向进行了归纳和展望.

    Abstract:

    This paper is a survey on the twenty years development of security protocols research. The state of the art in the application of formal methods to the design and analysis of security protocols is presented. Some major threads and emerging trends of research in this area are outlined.

    参考文献
    [1]Needham R, Schroeder M. Using encryption for authentication in large networks of computers. Communications of the ACM, 1978, 21(12):993～999.
    [2]Qing SH. Cryptography and Computer Network Security. Beijing: Tsinghua University Press, 2001, 127～147 (in Chinese).
    [3]Qing SH. Formal analysis of authentication protocols. Journal of Software, 1996,7(Supplement):107～114 (in Chinese with English abstract).
    [4]Otway D, Rees O. Efficient and timely mutual authentication. Operating Systems Review, 1987,21(1):8～10.
    [5]Burrows M, Abadi M, Needham R. A logic of authentication. In: Proceedings of the Royal Society of London A, Vol 426. 1989. 233～271.
    [6]Miller SP, Neuman C, Schiller JI, Saltzer JH. Kerberos authentication and authorization system. Project Athena Technical Plan Section E.2.1, MIT, 1987.
    [7]CCITT. CCITT draft recommendation X.509. The Directory-Authentication Framework, Version 7, 1987.
    [8]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.
    [9]ISO/IEC. Information technology?security techniques?entity authentication mechanisms part 2: Entity authentication using symmetric techniques. 1993.
    [10]Satyanarayanan M. Integrating security in a large distributed system. Technical Report, CMU-CS, CMU, 1987. 87～179.
    [11]ISO/IEC. Information technology?security techniques?entity authentication mechanisms part 4: Entity authentication using cryptographic check functions. 1993.
    [12]Denning D, Sacco G. Timestamps in key distribution protocols. Communications of the ACM, 1981,24(8):533～536.
    [13]Woo T, Lam S. A lesson on authentication protocol design. Operating Systems Review, 1994,28(3):24～37.
    [14]Neuman BC, Stubblebine SG. A note on the use of timestamps as nonces. Operating Systems Review, 1993,27(2):10～14.
    [15]Kao IL, Chow R. An efficient and secure authentication protocol using uncertified keys. Operating Systems Review, 1995,29(3): 14～21.
    [16]ISO/IEC. Information technology?security techniques?entity authentication mechanisms part 3: Entity authentication using a public key algorithm. 1995.
    [17]Diffie W, Hellman ME. New directions in cryptography. IEEE Transactions on Information Theory, 1976,IT-22(6):644～654.
    [18]Boyd C. Hidden assumptions in cryptographic protocols. Proceedings of the IEE, 1990,137(6):433～436.
    [19]Lowe G. Breaking and fixing the Needham-Schroeder public-key protocol using FDR. Software-Concepts and Tools, 1996,17: 93～102.
    [20]Dolev D, Yao A. On the security of public key protocols. IEEE Transactions on Information Theory, 1983,29(2):198～208.
    [21]Nessett DM. A critique of the burrows, Abadi and Needham logic. ACM Operating Systems Review, 1990,24(2):35～38.
    [22]Burrows M, Abadi M, Needham R. Rejoinder to Nessett. Operating Systems Review, 1990,24(2):39～40.
    [23]Roscoe A, Goldsmith M. The perfect 'spy' for model-checking cryptoprotocols. In: DIMACS Workshop on Design and Formal Verification of Security Protocols. 1997.
    [24]Schneider SA. Using CSP for protocol analysis: The Needham-Schroeder public-key protocol. Technical Report, CSD-TR-96-14, Royal Holloway: University of London, 1996.
    [25]Schneider SA. Security properties and CSP. In: Proceedings of the 1996 IEEE Symposium on Security and Privacy. Los Alamitos: IEEE Computer Society Press, 1996. 174～187.
    [26]Schneider S, Sidiropoulos A. CSP and anonymity. In: Proceedings of Computer Security-ES-ORICS 96. Berlin: Springer-Verlag, 1996. 198～218.
    [27]Marrero W, Clarke E, Jha S. A model checker for authentication protocols. In: DIMACS Workshop on Design and Formal Verification of Security Protocols. 1997.
    [28]Mitchell J, Mitchell M, Stern U. Automated analysis of cryptographic protocols using murphi. In: Proceedings of the 1997 IEEE Computer Society Symposium on Research in Security and Privacy. Los Alamitos: IEEE Computer Society Press, 1997. 141～151.
    [29]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.
    [30]Thayer FJ, Herzog JC, Guttman JD. Strand spaces: Proving security protocols correct. Journal of Computer Security, 1999,7(2-3): 191～230.
    [31]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.
    [32]Perrig A, Song D. Looking for diamonds in the desert-extending automatic protocol generation to three-party authentication and key agreement. In: Proceedings of the 13th IEEE Computer Security Foundations Workshop. Los Alamitos: IEEE Computer Society Press, 2000. 64～76.
    [33]Song D. Athena: A new efficient automatic checker for security protocol analysis. In: Proceedings of the 1999 IEEE Computer Security Foundations Workshop. Los Alamitos: IEEE Computer Society Press, 1999. 192～202.
    [34]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.
    [35]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.
    [36]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.
    [37]Syverson P. Knowledge, belief, and semantics in the analysis of cryptographic protocols. Journal of Computer Security, 1992,1(3): 317～334.
    [38]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.
    [39]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.
    [40]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.
    [41]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.
    [42]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.
    [43]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.
    [44]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.
    [45]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.
    [46]Kessler V, Wedel G. AUTOLOG?An advanced logic of authentication. In: Proceedings of the Computer Security Foundations Workshop. Los Alamitos: IEEE Computer Society Press, 1994. 90～99.
    [47]Kindred D. Theory generation for security protocols [Ph.D. Thesis]. Pittsburgh: Computer Science Department, Carnegie Mellon University, 1999.
    [48]Doraswamy N, Harkins D. IPSEC: The New Security Standard for the Internet, Intranets, and Virtual Private Networks. Prentice Hall, 1999.
    [49]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.
    [50]Qing SH. A new non-repudiation protocol. Journal of Software, 2000,11(10):1338～1343 (in Chinese with English abstract).
    [51]Meadows C. The NRL protocol analyzer: An overview. Journal of Logic Programming, 1996,26(2):113～131.
    [52]Meadows C. Analysis of the Internet key exchange protocol using the NRL protocol analyzer. In: Proceedings of the IEEE Symposium on Security and Privacy. Los Alamitos: IEEE Computer Society Press, 1999. 84～89.
    [53]Cervesato I, Durgin N, Lincoln P, Mitchell J. A meta-notation for protocol analysis. In: Proceedings of the 1999 IEEE Symposium on Security and Privacy. Los Alamitos: IEEE Computer Society Press, 1999. 55～69.
    [54]Millen J. The Interrogator model. In: Proceedings of the 1995 IEEE Symposium on Security and Privacy. Los Alamitos: IEEE Computer Society Press, 1995. 251～260.
    [55]Kemmerer R, Meadows C, Millen J. Three systems for cryptographic protocol analysis. Journal of Cryptology, 1994,7(2):251～260.
    [56]Paulson LC. Mechanized proofs for a recursive authentication protocol. In: Proceedings of the 10th IEEE Computer Security Foundations Workshop. Los Alamitos: IEEE Computer Society Press, 1997. 84～94.
    [57]Paulson LC. The inductive approach to verifying cryptographic protocols. Journal of Computer Security, 1998,(6):85～128.
    [58]Milner R, Parrow J, Walker D. A calculus of mobile processes. Information and Computation, 1992,100(1):1～77.
    [59]Abadi M, Gordon AD. A calculus for cryptographic protocols: The spi calculus. In: Proceedings of the 4th ACM Conference on Computer and Communications Security. 1997. 36～47.
    [60]Amadio R, Lugiez D. On the reachability problem in cryptographic protocols. In: Proceedings of the CONCUR. Berlin: Springer-Verlag, 2000. 380～394.
    [61]Abadi M, Blanchet B. Secrecy types for asymmetric communication. In: Proceedings of Foundations of the Software Science and Computation Structures. 2001. 35～49.
    [62]Amadio R, Prasad S. The game of the name in cryptographic tables. In: Proceedings of the ASIAN'99. Berlin: Springer-Verlag, 1999. 15～26.
    [63]Meadows C. Formal verification of cryptographic protocols: A survey. In: Advances in Cryptology, Asiacrypt'96 Proceedings. Berlin: Springer-Verlag, 1996. 135～150.
    [64]Heintze N, Tygar JD. A model for secure protocols and their composition. IEEE Transactions on Software Engineering, 1996,22(1): 16～30.
    [65]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.
    [66]Abadi M, Needham R. Prudent engineering practices for crypto-graphic protocols. In: Proceedings of the 1994 IEEE Symposium on Security and Privacy. Los Alamitos: IEEE Computer Society Press, 1994. 122～136.
    [67]Bolognesi T, Brinksma E. Introduction to the ISO specification language LOTOS. Computer Networks and ISDN Systems, 1987,14: 25～59.
    [68]Millen JK. CAPSL: Common authentication protocol specification language. Technical Report, MP 97B48, The MITRE Corporation, 1997.
    [69]Syverson P. A taxonomy of replay attacks. In: Proceedings of the Computer Security Foundations Workshop. Los Alamitos: IEEE Computer Society Press, 1994. 187～191.
    [70]Syverson P. On key distribution protocols for repeated authentication. Operating Systems Review, 1993,27(4):24～30.
    [71]Carlsen U. Using logics to detect implementation-dependent flaws. In: Proceedings of the 9th Annual Computer Security Applications Conference. Los Alamitos: IEEE Computer Society Press, 1993. 64～73.
    [72]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).
    [73]Meadows C. Open issues in formal methods for cryptographic protocol analysis. In: Proceedings of the DARPA Information Survivability Conference and Exposition. Los Alamitos: IEEE Computer Society Press, 2000. 237～250.
    [74]Kailar R. Reasoning about accountability in protocols for electronic commerce. In: Proceedings of the IEEE Symposium on Security and Privacy. Los Alamitos: IEEE Computer Society Press, 1995. 236～250.
    [75]Zhou DC, Qing SH, Zhou ZF. Limitations of Kailar logic. Journal of Software, 1999,10(12):1238～1245 (in Chinese with English abstract).
    [76]Zhou DC, Qing SH, Zhou ZF. A new approach for the analysis of electronic commerce protocols. Journal of Software, 2001,12(9): 1318～1328 (in Chinese with English abstract).
    [77]Qing SH. Design and logical analysis of security protocols. Journal of Software, 2003,14(7):1300～1309 (in Chinese with English abstract).
    [78]卿斯汉.密码学与计算机网络安全.北京:清华大学出版社,2000.127～147.
    [79]卿斯汉.认证协议的形式化分析.软件学报,1996,7(增刊):107～114.
    [80]卿斯汉.一种新型的非否认协议.软件学报,2000,11(10):1338～1343.
    [81]王贵林,卿斯汉,周展飞.认证协议的一些新攻击方法.软件学报,2001,12(6):907～913.
    [82]周典萃,卿斯汉,周展飞.Kailar逻辑的缺陷.软件学报,1999,10(12):1238～1245.
    [83]周典萃,卿斯汉,周展飞.一种分析电子商务协议的新工具.软件学报,2001,12(9):1318～1328.
    [84]卿斯汉.安全协议的设计与逻辑分析.软件学报,2003,14(7):1300～1309.
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

卿斯汉.安全协议20年研究进展.软件学报,2003,14(10):1740-1752

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

京公网安备 11040202500063号