Survey on Theories and Methods of Formal Analyses for Security Protocols

doi:10.7523/j.issn.2095-6134.2003.4.001

Abstract

Abstract:

Theories and methods of formal analyses for security protocol are surveyed.A classfication and a system model of formal analyses is given, and three classes of formal analy sis methods(based on reasoning,based on attack, based on proof)and fo rmal languages used in formal analyses are commented in details.Also disscussed is a new challenge the methods of security pro tocol formal analy sis are facing. Corresponding comments on these theories and methods are also given during the discussion.Challenges formal analyses face are also proposed.

Key words: security protocol, security model, formal analysis, formal language

CLC Number:

TP393

Feng Dengguo, Fan Hong. Survey on Theories and Methods of Formal Analyses for Security Protocols[J]. , 2003, 20(4): 389-406.

References

［1］R M Needham, M D Schroeder. Using Encryption for Authentication of Large Networks of Computers. Communications of the ACM, 1978,21(12) :993～999

［2］D Denning, G Sacco. Timestamps in Key Distribution Protocols. Communications of the ACM, 1981,24(8)

［3］D Dolev, A Yao. On the Security of Public Key Protocols. IEEE Transactions on Information Theory, 1983,29(2): 198～208

［4］M Burrows, M Abadi, R Needham. A Logic of Authentication. Research Report 39, Digital Systems Research Center, 1989;Parts and Versions of this Material Have Been Presented in Many Places Including: ACM Transactions on Computer Systems, 1989, 8(1):18～36; Proceedings of the Royal Society of Lond on A. 1989,426:233～271

［5］Paul Syverson. A Taxonomy of Relay Attacks. In proceedings of the 7th IEEE Computer Security Foundations Workshop, 97～ 101.New York:ACM Press, 1994, 131～136

［6］L Gong, R Needham, R Yahalom. Reasoning about Belief in Cryptographic Protocols. In: Proceedings of the 1990 IEEE Computer Society Symposium on Research in Security and Privacy, 234～248. Los Alamitos, California:IEEE Computer Society Press, 1990

［7］M Abadi, M R Tuttle. A Semantics for a Logic of Authentication. In: Proceeding of the Tenth ACM Symposium on Principles of Distributed Computing. ACM Press, 1991. 201～216

［8］P F Syverson, P C van Oorschot. On Unified Some Cryptographic Protocol Logics. In: Proceedings of the 1994. IEEE Computer Society Press, 1994

［9］R Kailar. Accountability in Electronic Commerce Protocols. IEEE Trans on Software Engineering, 1996,22(5) :313～328

［10］D Kindred. Theory Generation for Security Protocols: [Ph. D Thesis]. Computer Science Department, Carnegie Mellon University.1999

［11］Michael Burrows, Martin Abadi, Roger Needham. Authentication: A Practical Study in Belief and Action. Proceedings of the 2nd Conference in Theoretical Aspects of Reasoning about Knowledge. Morgan Kaufmann, 1988. 325～342

［12］Michael Burrows, Martin Abadi, Roger Needham. A Logic of Authentication. ACM Transactions in Computer systems, 1990, 8(1):18～36

［13］P F Syverson, P C van Oorschot. A Unified Cryptographic Protocol Logic. NRL CHACS Report. 1996. 5540-227

［14］Ronald L, Rivest Adi Shamir, David A, Wagner: Timed-lock puzzles and Timed-Release Cryptographic protocol. MIT Laboratary for Computer Science, 1996

［15］T Coffey, P Saidha. Logic for Verifying Public-key Cryptographic Protocols. IEEE Proc Computers and Digital Techniques, 1997,144(1) :28～32

［16］G Lowe. Breaking and fixing the Needham-Schroder public-key protocol using FDR. In: Tools and Algorithms for the Construction and Analysis of Systems, volume 1055 of Lecture Notes in Computer Science. Springer-Verlag, 1996. 147～166

［17］J Bums, C J Mitchell. A Security Scheme for Resource Sharing Over a Network. Computers and Security, 1990, 9:67～76

［18］C Meadows. A Model of Computation for the NRL Protocol Analyzer. In: Proceedings of the 7th Computer Security Foudations Workshop. IEEE Computer Society Press, 1994

［19］Thomas Y C Woo, Simon S. Lam: Authentification for Distributed Systems. IEEE Computer, 1992. 25(1): 39～52

［20］T Genet, F Klay. Rewriting for Cryptographic Protocol Verification. In: Proceedings 17th International Conference on Automated Deduction, Pittsburgh (Pen., USA), volume 1831 of Lecture Notes in Artificial Intelligence. Springer-Verlag, 2000

［21］T Genet, F Klay. Rewriting for Cryptographic Protocol Verification (extended version). Technical Report. CNET-France Telecom, 1999; Available at http://www. loria. fr/genet/Publications/ GenetKlay-RR99. ps.

［22］Richard A Kemmerer. Analyzing Encryption Protocols Using Formal Verification Techniques. IEEE Journal on Selected Areas of Communicaitons, 1989, 7(4) :448～457

［23］J Scheid, S Holtsberg. Ina Jo Specification Language Reference Manual Systems Development Croup. Unisys Corporation, 1988. Michael Burrows, Martin Abadi, Roger Needham. A Logic of Authentication. ACM Transactions in Computer Systems, 1990, 8(1):18～36

［24］C A R Hoare. Communicating Sequential Processes. Prentice-Hall International, Englewood Cliffs, NJ, 1985

［25］Will Marrero, Edmund Clarke, Somesh Jha. A Model Checker for Authentication Protocols. In: Proc DIMACS Workshop on Design and Formal Verification of Security Protocols. 1997

［26］G Lowe. Breaking and Fixing the Needham-Schroder Public-Key Protocol Using FDR. In: Tools and Algorithms for the Construction and Analysis of Systems, volume 1055 of Lecture Notes in Computer Science. Springer-Verlag, 1996. 147～166

［27］T Y C Woo, S S Lam. A Semantic Model for Authentication Protocols. In:Proc 14th IEEE Symposium on Research in Security and Privacy, IEEE Computer Society Press, 1993. 178～ 194

［28］D Longley, S Rigby. Use of Expert Systems in the Analysis of Key Management Systems. Security and Protection in Information Systems. 1989. 213～224

［29］Jonathan K Millen, Sidney C Clark, Sheryl B Freedman. The Interrogator: Protocol Security Analysis. TSE, 1987,13(2): 274～288

［30］Paul Syverson, Catherine Meadows. A Logical Language for Specifying Cryptographic Protocol Requirements, Proceedings of the 1993 IEEE Symposium on Research on Security and Privacy. IEEE Computer Society Press, 1993. 165～177

［31］Gustavus J Simmons. How to (Selectively) Broadcast a Secret. In: Proceedings of the 1985 IEEE Computer Society Symposium on Security and Privacy. IEEE Computer Society Press, 1985. 108～113

［32］D Longley, S. Rigby. An Automatic Search for Security Flaws in Key Management Schemes. Computers ＆ Security, 1992,11 (1):75～89

［33］Bolignano D. An Approach to the Formal Verification of Cryptographic Protocols. Proceedings of the Third ACM Conference on Computer and Communications \Security. ACM Press, 1996. 106～118

［34］L C Paulson. Proving Properties of Security Protocols by Induction. Proceedings of the IEEE Computer Security Foundations Workshop X. IEEE Computer Society Press, 1997.70～83

［35］S Schneider. Using CSP for Protocol Analysis: the Needham-Schroeder Public Key Protocol. Technical Report CSD-TR-96-14.Royal Holloway, 1996

［36］F Javier Thayer Fabrega, Jonathan C Herzog, Joshua D Guttman. Honest Ideals on Strand Spaces. In: Proc 1 l th IEEE Computer Security Foundations Workshop(CSFW). IEEE Computer Society Press, 1998

［37］F Javier Thayer Fabrega, Jonathan C Herzog, Joshua D Guttman. Strand Spaces Pictures. In: Workshop on Formal Methods and Security Protocols. 1998; Available via http://www. cs. bell-labs. com/who/nch/fmsp/index. html

［38］F Javier Thayer Fabrega,Jonathan C Herzog, Joshua D Guttman. Strand Space:Why Is a Security Protocol Correct?In: Proc 18th IEEE Symposium on Research in Security and Privacy. IEEE Computer Society Press, 1998

［39］A W Roscoe. Modeling and Verifying Key Exchange Protocols Using CSP and FDR. In: Proc-8th IEEE Computer Security Foundations Workshop (CSFW). IEEE Computer Society Press, 1995.98～ 107

［40］Gavin Lowe, Bill Roscoe. Using CSP to Detect Errors in the TMN Protocol. IEEE Transactions on Software Engineering, 1997,23(10) :659～669

［41］N Heintze, J D Tygar. A Model for Secure Protocols and Their Composition. IEEE Transaction on Software Engineering, 1996,22(16)

［42］Scott D Stoller. A Bound on Attacks on Payment Protocols. In: Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science (LICS). IEEE Computer Society Press, 2001.61～70

［43］Meadows C. Using the NRL Protocol Analyzer to Examine Protocol Suites. In:Proceedings of the 1998 LICS Workshop on Formal Methods and Security Protocols. 1998; http://www. cs. bell-labs. com/who/nch/fmsp/program. html

［44］L C Paulson. The Inductive Approach to Verifying Cryptographic Protocols. Journal of Computer Security, 1998, 6:85～128

［45］Alec Yasinsac. A Formal Semantics for Evaluating Cryptngraphic Protocols: [Ph. D. Dissertation]. University of Virginia, 1996

［46］S Brackin. An Interface Specification Language for Automatically Analyzing Cryptographic Protocols. Internet Society Symposium on Network and Distributed System Security. San Diego, CA. 1997

［47］J Millen. CAPSL:Common Authentication Protocol Specification Language. Technical Report MP 97B48. The MITRE Corporation.1997

［48］J Millen. CAPSL Semantics. The MITRE Corporation, MP 97B60. 1997

［49］J Millen. Term Replacement Algebra for the Interrogator. The MITRE Corporation, MP 97B65. 1997

［50］J Millen. The Interrogator User＇s Guide. The MITRE Corporation, MP 97B66. 1997

［51］G Lowe. A Hierarchy of Authentication Specifications. In: Proceedings of the 1997 IEEE Computer Society Symposium on Research in Security and Privacy. 1997.31～43

［52］G Agha. Abstracting Interaction Patterns: A Programming Paradigm for Open Distribute Systems. In: H Bowman, J Derrick, editors. Formal Methods for Open Object-Based Distributed Systems (FMOODS' 97): Volume 2. IFIP TC6 WG6.1 Intern Workshop,Canterbury, Kent UK. Chapman ＆ Hall, 1997. 135～153

［53］S Brackin. Evaluating and Improving Protocol Analysis by Automatic Proof. CSFW. 1998. 138～152

［54］Secure Electronic Transaction (SET) specification. Available from http://www. visa. com/cgi-bin/vee/sf/set/intro. html?2+0, 1996

［55］R Milner, J Parrow, D Walker. A Calculus of Mobile Processes, Parts Ⅰ and Ⅱ. Information and Computation, 1992.1～40, 41～77

［56］J Gray, J Mclean. Using Temporal Logic to Specify and Verify Cryptographic Protocols (Progress Report). In: Proceedings of the 8th IEEE Computer Security Foundations Workshop. 1995. 108～116

［57］L Gong, P Syverson. Fail-Stop Protocols: An Approach to Designing Secure Protocols. In: Proceedings of the 5th IFIP Working Conference on Dependable Computing for Critical Applications, Dependable Computing and Fault-Tolerant Systems. Urbana-Champaign, Illinois. Springer-Verlag, 1995. 44～55

［58］M Abadi, R Needham. Prudent Engineering Practice for Cryptographic Protocols. IEEE Transactions on Software Engineering,1996, 22(1) :6～15.

［59］Bracking S. A State-Based HOL Theory of Protocol Failure. ATR 98007, Arca Systems. Inc, 1997; http://www. arca. com/paper.htm

［60］S Brackin. Deciding Cryptographic Protocol Adequacy with HOL: The Implementation. In: Theorem Proving in Higher Ordcr Logics: number 1125 in Lecture Notes in Computer Science. Finland, Turku, Springer-Verlag, 1996.61～76

［61］冯登国.国内外信息安全研究现状及其发展趋势.网络安全技术与应用,2001,1(1):108～113

［62］冯登国.国内外密码学研究现状及发展趋势.通信学报,2002,23(5):18～26

［63］Stefanos Gritzalis, Diomidis Spinellis. The Cascade Vulnerability Problem: The Detection Problem and a Simulated Annealing Approach for its Correction. Microprocessors and Microsystems, 1998, 21(10) :621～628

［64］F Javier Thayer Fabrega, Jonathan C Herzog, Joshua D Guttman. Strand Space: Why is a Security Protocol Correct?In: Proceedings of the 1998 IEEE Symposium on Security and Privacy, IEEE Computer Society Press, 1998. 160～171

［65］S Bellovin, M Merritt. Encrypted Key Exchange: Password-Based Protocols Secure Against Dictionary Attacks. In: Proceedings of the IEEE Symposium on Security and Privacy. Oakland, California, 1992. 72～84

[1]	QIN Yu, LAN Hai-Bo. TPM security model for virtual domains [J]. , 2011, 28(5): 648-658.
[2]	WANG Zhi-Ling, ZHANG Yu-Qing, YANG Bo. Design Principles of Fair Exchange Protocol [J]. , 2006, 23(4): 555-560.
[3]	MO Yan, ZHANG Yu-Qing, LI Xue-Gan. The Running-Mode Analysis of SSL310 Basic Handshake Protocol [J]. , 2005, 22(4): 511-517.
[4]	LIU XiuYing, ZHANG YuQing, YANG Bo, XING Ge. Running-Mode Analysis of the Three-Party Cryptographic Protocol [J]. , 2004, 21(3): 380-385.
[5]	LIU Yi-Wen, LI Wei-Qin. Some Bounds on Security Protocol Analysis——Combining Model Checking and Strand Spaces [J]. , 2002, 19(3): 288-294.
[6]	FAN Hong, FENG Deng-Guo. A Mixed Formal Analysis Technology of Security Protocols [J]. , 2002, 19(3): 240-245.
[7]	FAN Hong, FENG DengGuo, GUO JinGeng. Invariant Generation Techniques in Cryptographic Protocol Analysis [J]. , 2002, 19(1): 91-96.
[8]	Wang Hui, Shao Peiying. Design and Implement of Multi-Level Security Policy for Internet Firewalls [J]. , 2000, 17(2): 99-104.