Abstract
Logics can be systematically applied to reasoning about the working of protocols. However, the process of applying and reapplying the inference rules is often tedious and error-prone when carried out manually, while automation method will improve this problem. An automated logic-based analysis tool based on the freshness principle is introduced and developed, which uses the belief multiset formalism to analyze the security of cryptographic protocols.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Dong L, Chen K, Zheng Y, Hong X (2008) The Guarantee of Authentication Protocol Security. Journal of Shanghai JiaoTong University, 42(4): 518–522 (in Chinese)
Chen K, Dong L, Lai X (2008) Security Analysis of Cryptographic Protocols Based on Trusted Freshness. Journal of Korea Institute of Information Security and Cryptology, 18(6B): 1–13
Dong L, Chen K, Lai X (2009) Belief Multisets for Cryptographic Protocol Analysis. Journal of Software, 20(11): 3060–3076 (in Chinese)
Dong L, Chen K, Lai X, Wen M (2009) When is a Key Establishment Protocol Correct? Security and Communication Networks, 2(6): 567–579
Saul E (2001) Facilitating the Modelling and Automated Analysis of Cryptographic Protocols. Master Thesis, University of Cape Town
Saul E and Hutchison A (1999) SPEAR II: The Security Protocol Engineering and Analysis Resource. Second South African Telecommunications, Networks, and Applications Conference. http://pubs.cs.uct.ac.za/archive/ 00000128/01/saul1999 SPEAR SATNAC.pdf. Accessed 5 May 2011
Mao W (2004) Modern Cryptography: Theory and Practice. Prentice Hall, New Jersey
Bekmann J, Goede P. de and Hutchison A (1997) SPEAR: a Security Protocol Engineering & Analysis Resource. In DIMACS Workshop on Design and Formal Verification of Security Protocols. http://dimacs.rutgers.edu/ Workshops/Security/program2/hutch/spear.html. Accessed 5 May 2011
Burrows M, Abadi M, and Needham R (1990) A logic of authentication. ACM Transactions on Computer Systems, 8(1): 18–36
Lowe G (1996) Breaking and Fixing the Needham-Schroeder Public-key Protocol Using FDR. In: TACAS’96 Proceedings of the 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Passau, 27–29 Mar 1996. Lecture Notes in Computer Science (Lecture Notes in Software Configuration Management), vol 1055. Springer-Verlag, Heidelberg, pp 147–166
Lowe G (1995) An Attack on the Needham-Schroeder Public Key Authentication Protocol. Information Processing Letters, 56(3): 131–133, 1995
Lowe G (1996) Some new Attacks Upon Security Protocols. In Proceedings of the 9th IEEE Computer Security Foundations Workshop, pages 162–169, Jun. 1996
Roscoe A W (1994) Model Checking CSP. In: Roscoe A W (ed) A Clasical Mind: Essays in Honour of C.A.R Hoare. Prentice-Hall, 1994
Meadows C (1996) The NRL Protocol Analyzer: an Overview. Journal of Logic Programming, 26(2): 113–131
Dolev D, Yao AC (1983) On the Security of Public Key Protocols. IEEE Transactions on Information Theory 29(2): 198–208
Meadows C (1994) A Model of Computation for the NRL Protocol Analyzer. In: Proceedings of the 1994 Computer Security Foundations Workshop, Franconia, 14–16 June 1994
Harkins D and Carrel D (1998) The Internet Key Exchange Protocol (IKE). IETF RFC 2409, Available at http://www.ietf.org/rfc/rfc2409.txt. Accessed 5 May 2011
Kaufman C (2005) Internet Key Exchange (IKEv2) Protocol. IETF RFC 4306, Available at http://tools.ietf.org/html/rfc4306. Accessed 5 May 2011
SET (1997) Secure Electronic Transaction. The SET Standard Specification. http://www.setco.org/set-specifications. Accessed 5 May 2011
Mitchell J.C, Mitchell M and Stern U (1997) Automated Analysis of Cryptographic Protocols Using Mur?. Proc. of 1997 IEEE Symposium on Security and Privacy, Oakland, California, pp 141–153
Needham RM, Schroeder MD (1978) Using Encryption for Authentication in Large Network of Computers. Communication of the ACM 21(12): 993–999
Tatebayashi M, Matsuzaki N, Newman D (1990) Key Distribution Protocol for Digital Mobile Communication Systems, CRYPTO’89, LNCS435
Neuman C, Ts’o T (1994) Kerberos: An Authentication Service for Computer Networks, IEEE Communications Magazine, 32(9): 33–38
Millen JK, Clark SC, Freedman SB (1987) The Interrogator: Protocol Security Analysis. IEEE Trans. Software Eng. 13(2): 274–288
Berezin S, Groce A. SyMP: Symbolic Model Prover. Model Checking@CMU. http://www.cs.cmu.edu/ modelcheck/symp.html. Accessed 5 May 2011
Fabrega FJT, Herzog JC, Guttman JD (1998) Strand Spaces: Why is a Security Protocol Correct? In: Proceedings of IEEE Symposium on Security and Privacy, Oakland, 3–6 May 1998
Song D (1999) Athena: A New Efficient Automatic Checker for Security Protocol Analysis. Proceedings of the 1999 IEEE Computer Security Foundations Workshop, IEEE Computer Society Press, pp 192–202
Millen J K (1996) CAPSLS: Common Authentication Protocol Specification Language. http://www.csl.sri.com/users/millen/capsl. Accessed 5 May 2011
Wei MQ (2008) Automated Verification of Security Protocol. BE Thesis (in Chinese), Shanghai Jiaotong University
Wang EJ (2008) Research of Automated Verification Tool for Security Protocol. BE Thesis (in Chinese), Shanghai Jiaotong University
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 2012 Higher Education Press, Beijing and Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Dong, L., Chen, K. (2012). Automated Analysis of Cryptographic Protocols Based on Trusted Freshness. In: Cryptographic Protocol. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-24073-7_9
Download citation
DOI: https://doi.org/10.1007/978-3-642-24073-7_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-24072-0
Online ISBN: 978-3-642-24073-7
eBook Packages: Computer ScienceComputer Science (R0)