Abstract
Many model checking methods have been developed and applied to analyze cryptographic protocols. Most of them can analyze only one attack trace of a found attack. In this paper, we propose a very simple but practical model checking methodology for the analysis of cryptographic protocols. Our methodology offers an efficient analysis of all attack traces for each found attack, and is independent to model checking tools. It contains two novel techniques which are on-the-fly trace generation and textual trace analysis. In addition, we apply our method to two case studies which are TMN authenticated key exchanged protocol and Micali’s contract signing protocol. Surprisingly, it turns out that our simple method is very efficient when the numbers of traces and states are large. Also, we found many new attacks in those protocols.
Chapter PDF
Similar content being viewed by others
References
Clark, J., Jacob, J.: A survey on Authentication Protocols, Research report, University of York (1997), http://www.cs.york.ac.uk/~jac/papers/drareview.ps.gz
Meadows, C.: Formal Methods for Cryptographic Protocol Analysis: Emerging Issues and Trends. IEEE Journal on Selected Areas in Communications 21(1), 44–54 (2003)
Meyer, U., Wetzel, S.: A man-in-the-middle attack on UMTS. In: The 3rd ACM workshop on Wireless Security, pp. 90–97 (2004)
Cervesato, I., Jaggard, A.D., Scedrov, A., Tsay, J., Walstad, C.: Breaking and fixing public-key Kerberos. Information and Computation 206(2-4), 402–424 (2008)
Syverson, P.F.: A Taxonomy of Replay Attacks. In: The 7th IEEE Computer Security Foundations Workshop, pp. 187–191 (1994)
The AVISPA project, http://avispa-project.org
Viganò, L.: Automated Security Protocol Analysis With the AVISPA Tool. Electr. Notes Theor. Comput. Sci. 155, 61–86 (2006)
Maggi, P., Sisto, R.: Using SPIN to Verify Security Properties of Cryptographic Protocols. In: Bošnački, D., Leue, S. (eds.) SPIN 2002. LNCS, vol. 2318, pp. 85–87. Springer, Heidelberg (2002)
Lowe, G., Roscoe, B.: Using CSP to Detect Errors in the TMN Protocol. IEEE Transactions on Software Engineering 23(10), 659–669 (1997)
Lowe, G.: Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR. Software - Concepts and Tools 17(3), 93–102 (1996)
Mitchell, J., Mitchell, M., Stern, U.: Automated analysis of cryptographic protocols using Murφ. In: 1997 IEEE Symposium on Security and privacy, pp. 141–151 (1997)
Shmatikov, V., Mitchell, J.C.: Finite-state analysis of two contract signing protocols. Theor. Comput. Sci. 283(2), 419–450 (2002)
Al-Azzoni, I., Down, D.G., Khedri, R.: Modeling and Verification of Cryptographic Protocols Using Coloured Petri Nets and Design/CPN. Nordic Journal of Computing 12(3), 201–228 (2005)
Bouroulet, R., Devillers, R., Klaudel, H., Pelz, E., Pommereau, F.: Modeling and Analysis of Security Protocols Using Role Based Specifications and Petri Nets. In: van Hee, K.M., Valk, R. (eds.) PETRI NETS 2008. LNCS, vol. 5062, pp. 72–91. Springer, Heidelberg (2008)
Meadows, C.: The NRL protocol analyzer: An overview. Journal of Logic Programming 26(2), 113–131 (1996)
Blanchet, B.: An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In: 14th IEEE Computer Security Foundations Workshop, pp. 82–96. IEEE press, Los Alamitos (2001)
Micali, S.: Simple and Fast Optimistic Protocols for Fair Electronics Exchange. In: 21st Symposium on Principles of Distributed Computing, pp. 12–19. ACM Press, New York (2003)
Tatebayashi, M., Matsuzaki, N., Newman, D.: Key Distribution Protocol for Digital Mobile Communication Systems. In: Brassard, G. (ed.) CRYPTO 1989. LNCS, vol. 435, pp. 324–334. Springer, Heidelberg (1990)
Jensen, K.: Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use. Monographs in Theoretical Computer Science, vol. 1. Springer, Heidelberg (1997)
CPNTools, http://wiki.daimi.au.dk/cpntools/
Sornkhom, P., Permpoontanalarp, Y.: Security Analysis of Micali’s Fair Contract Signing Protocol by Using Coloured Petri Nets. In: The 9th ACIS-SNPD 2008, pp. 329–334. IEEE Press, Thailand (2008)
Sornkhom, P., Permpoontanalarp, Y.: Security Analysis of Micali’s Fair Contract Signing Protocol by Using Coloured Petri Nets: Multi-session case. In: The 5th International Workshop on Security in Systems and Networks, pp. 1–8. IEEE press, Italy (2009)
Permpoontanalarp, Y., Sornkhom, P.: A New Coloured Petri Net Methodology for the Security Analysis of Cryptographic Protocols. In: The 10th Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools, Denmark, pp. 81–100 (2009)
Permpoontanalarp, Y.: Security Analysis of the TMN protocol by using Coloured Petri Nets: Multi-Session Case. In: The 10th International Conference on Intelligent Technologies, China, pp. 401–410 (2009)
Bao, F., Wang, G., Zhou, J., Zhu, Z.: Analysis and Improvement of Micali’s Fair Contract Signing Protocol. In: Wang, H., Pieprzyk, J., Varadharajan, V. (eds.) ACISP 2004. LNCS, vol. 3108, pp. 176–187. Springer, Heidelberg (2004)
Zhang, Y., Wang, Z., Yang, B.: The Running-Mode Analysis of Two-Party Optimistic Fair Exchange Protocols. In: Hao, Y., Liu, J., Wang, Y.-P., Cheung, Y.-m., Yin, H., Jiao, L., Ma, J., Jiao, Y.-C. (eds.) CIS 2005. LNCS (LNAI), vol. 3802, pp. 137–142. Springer, Heidelberg (2005)
Kemmerer, R., Meadows, C., Millen, J.: Three systems for cryptographic protocol analysis. Journal of Cryptology 7(2) (1994)
Zhang, Y., Liu, X.: An approach to the formal analysis of TMN protocol. In: Chen, K. (ed.) Progress on Cryptography: 25 years of Cryptography in China. The Inter-National Series in Engineering and Computer Science, vol. 769, pp. 235–243. Springer, Netherlands (2004)
Dolev, D., Yao, A.: On the security of public key protocols. IEEE Transactions on Information Theory 29(2), 198–207 (1983)
Lowe, G.: An Attack on the Needham-Schroeder Public-Key Authentication Protocol. Information Processing Letters 56(3), 131–133 (1995)
ITU-T, Recommendation Z.120: Message Sequence Chart (MSC), ITU-T, Geneva (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Permpoontanalarp, Y. (2010). On-the-Fly Trace Generation and Textual Trace Analysis and Their Applications to the Analysis of Cryptographic Protocols. In: Hatcliff, J., Zucca, E. (eds) Formal Techniques for Distributed Systems. FMOODS FORTE 2010 2010. Lecture Notes in Computer Science, vol 6117. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-13464-7_16
Download citation
DOI: https://doi.org/10.1007/978-3-642-13464-7_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-13463-0
Online ISBN: 978-3-642-13464-7
eBook Packages: Computer ScienceComputer Science (R0)