微信服务号

微信订阅号

2025-6-6- 15
Home > Archive>Volume 14, Issue 10, 2003 >1740-1752
PDF HTML XML Export Cite reminder
Twenty Years Development of Security Protocols Research
Author:
Affiliation:

  • Article
    • | |
  • Metrics
    • |
  • Reference [84]
    • |
  • Related [20]
    • |
  • Cited by [90]
    • | |
  • Comments
    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.

    Reference
    [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.
    Comments
    Comments
    分享到微博
    Submit
Get Citation

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

Copy
Share
Article Metrics
  • Abstract:9416
  • PDF: 10269
  • HTML: 0
  • Cited by: 0
History
  • Received:February 20,2003
  • Revised:February 20,2003
Links:Institute of Software, CASChina Computer FederationCASNSFC
You are the first2051952Visitors
Copyright: Institute of Software, Chinese Academy of Sciences Beijing ICP No. 05046678-4
Address：4# South Fourth Street, Zhong Guan Cun, Beijing 100190,Postal Code：100190
Phone：010-62562563 Fax：010-62562533 Email：jos@iscas.ac.cn
Technical Support：Beijing Qinyun Technology Development Co., Ltd.

Beijing Public Network Security No. 11040202500063