On-the-fly Trace Generation Approach to the Security Analysis of Cryptographic Protocols: Coloured Petri Nets-based Method

• Autorzy: Permpoontanalarp Y. , Sornkhom P.

Identyfikatory

DOI

10.3233/FI-2014-999

• Języki publikacji: EN

Abstrakty

EN

Most Petri nets-based methods that have been developed to analyze cryptographic protocols provide the analysis of one attack trace only. Only a few of them offer the analysis of multiple attack traces, but they are rather inefficient. Analogously, the limitation of the analysis of one attack trace occurs in most model checking methods for cryptographic protocols. In this paper, we propose a very simple but practical Coloured Petri nets-based model checking method for the analysis of cryptographic protocols, which overcomes these limitations. Our method offers an efficient analysis of multiple attack traces. We apply our method to two case studies which are TMN authenticated key exchanged protocol and Micali's contract signing protocol. Surprisingly, our simple method is very efficient when the numbers of attack traces and states are large. Also, we find many new attacks in those protocols.

Słowa kluczowe

EN

formal methods for cryptographic protocols; model checking; coloured Petri nets; Petri nets

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2014
• Tom: Vol. 130, nr 4
• Strony: 423--466
• Opis fizyczny: Bibliogr. 50 poz., rys., tab.

Twórcy

autor

Permpoontanalarp Y.

• Logic and Security Laboratory, Department of Computer Engineering, Faculty of Engineering, King Mongkut's University of Technology Thonburi, Bangkok, Thailand

autor

Sornkhom P.

• Logic and Security Laboratory, Department of Computer Engineering, Faculty of Engineering, King Mongkut's University of Technology Thonburi, Bangkok, Thailand

Bibliografia

• [1] Al-Azzoni, I., Down, D.G., and Khedri, R.: Modeling and Verification of Cryptographic Protocols Using Coloured Petri Nets and Design/CPN, Nordic Journal of Computing, 12(3), 2005, 201-228.
• [2] Allamigeon, X. and Blanchet, B.: Reconstruction of Attacks against Cryptographic Protocols, Proc. 18th IEEE Computer Security Foundations Workshop, Aix-en-Provence, France, 2005.
• [3] Armando, A. and Compagna, L.: SAT-based Model Checking for Security Protocols Analysis, International Journal of Information Security, 7(1), 2008, 3-32.
• [4] The AVISPA project, 2003, http://avispa-project.org, accessed on 1 Nov 2011.
• [5] Bao, F., Wang, G., Zhou, J., Zhu, Z.: Analysis and Improvement of Micali’s Fair Contract Signing Protocol, Proc. 9th Australasian Conference on Information Security and Privacy (H.Wang, J. Pieprzyk, V. Varadharajan, Ed.), LNCS 3108, Springer Verlag, Berlin, 2004.
• [6] Basin, D., Mödersheim, S. and Vigano, L.: OFMC: A symbolic model checker for security protocols, International Journal of Information Security, 4(3), 2005, 181-208.
• [7] Bird, R., Gopal, I., Herzberg, A., Janson, P.A., Kutten, S., Molva, R. and Yung, M.: Systematic Design of a Family of Attack-Resistant Authentication Protocols, IEEE Journal on Selected Areas in Communications, 11(5), 1993, 679-693.
• [8] Blanchet, B.: An Efficient Cryptographic Protocol Verifier Based on Prolog Rules, Proc. 14th IEEE Computer Security Foundations Workshop, Nova Scotia, Canada, 2001.
• [9] Boichut, Y. , Héam, P.-C. and Kouchnarenko, O.: Automatic Verification of Security Protocols Using Approximations, INRIA Research Report, 2005.
• [10] Bouroulet, R., Devillers, R., Klaudel, H., Pelz, E., Pommereau, F.: Modeling and Analysis of Security Protocols Using Role Based Specifications and Petri Nets, Proc. 29th International Conference on Applications and Theory of Petri Nets-PETRI NETS (K.M. van Hee, R. Valk, Ed.), LNCS 5062, Springer Verlag, Berlin, 2008.
• [11] Cervesato, I., Jaggard, A.D., Scedrov, A., Tsay, J., Walstad, C.: Breaking and fixing public-key Kerberos, Information and Computation, 206(2-4), 2008, 402-424.
• [12] Clark, J., Jacob, J.: A survey on Authentication Protocols Literature: Version 1.0, Research report, University of York, 1997.
• [13] Comon-Lundh, H. and Cortier, V.: Security properties: two agents are sufficient, Science of Computer Programming, 50(1-3), 2004, 51-71.
• [14] CPNTools, 2000, http://cpntools.org/, accessed on 21 August 2012.
• [15] Cremers, C.: Unbounded verification, falsification, and characterization of security protocols by pattern refinement, Proc. 15th ACM Conference on Computation and Communication Security, Virginia, USA, 2008.
• [16] Dolev, D., Yao, A.: On the security of public key protocols, IEEE Transactions on Information Theory, 29(2), 1983, 198-207.
• [17] Dresp, W.: Security Analysis of the Secure Authentication Protocol by Means of Coloured Petri Nets, Proc. 9th IFIP Communications and Multimedia Security (J. Dittmann, S. Katzenbeisser, A. Uhl, Ed.), LNCS 3677, Springer-Verlag, Berlin, 2005.
• [18] Escobar, S., Meadows, C. and Meseguer, J.: Maude-NPA: Cryptographic Protocol Analysis Modulo Equational Properties, in: Foundations of Security Analysis and Design V, FOSAD 2007/2008/2009 Tutorial Lectures (A. Aldini, G. Barthe, R. Gorrieri, Ed.), LNCS 5705, Springer-Verlag, Berlin, 2009, 1-50.
• [19] Esparza, J. and Heljanko, K.: Unfoldings − A Partial-Order Approach to Model Checking, EATCS Monographs in Theoretical Computer Science, Springer-Verlag, Berlin, 2008.
• [20] Grahlmann, B. and Best, E.: PEP − More than a Petri Net Tool, Proc. 2nd International Workshop on Tools and Algorithms for Construction and Analysis of Systems(T. Margaria, B. Steffen, Ed.), LNCS 1055, Springer-Verlag, Berlin, 1996.
• [21] Holzmann, G.: The SPIN Model Checker : Primer and Reference Manual, Addison-Wesley, 2003.
• [22] Jensen, K.: Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use, vol.1., Monographs in Theoretical Computer Science, Springer-Verlag, Berlin, 1997.
• [23] Jensen, K. and Kristensen L.M.: Coloured Petri Nets: Modelling and Validation of Concurrent Systems, Springer-Verlag, Berlin, 2009.
• [24] Kemmerer, R., Meadows, C., Millen, J.: Three systems for cryptographic protocol analysis, Journal of Cryptology, 7(2), 1994, 79-130.
• [25] Lee, G., and Lee, J.: Petri Net Based Models for Specification and Analysis of Cryptographic Protocols, The Journal of Systems and Software, 37, 1997, 141-159.
• [26] Lim, S., Ko, J., Jun, E., and Lee, G.: Specification and Analysis of N-Way Key Recovery System by Extended Cryptographic Timed Petri Net, The Journal of Systems and Software, 58, 2001, 93-106.
• [27] Liu, J., Ye, X., Zhang, J. and Li, J.: Security Verification of 802.11i 4-Way Handshake Protocol, Proc. IEEE International Conference on Communications, Beijing, China, 2008.
• [28] Lowe, G.: An Attack on the Needham-Schroeder Public-Key Authentication Protocol, Information Processing Letters, 56(3), 1995, 131-133.
• [29] Lowe, G.: Breaking and Fixing the Needham-Schroeder Public-Key Protocol Using FDR, Software – Concepts and Tools, 17(3), 1996, 93-102.
• [30] Lowe, G., Roscoe, B.: Using CSP to Detect Errors in the TMN Protocol, IEEE Transactions on Software Engineering, 23(10), 1997, 659-669.
• [31] Maggi, P., Sisto, R.: Using SPIN to Verify Security Properties of Cryptographic Protocols, Proc. 9th International SPIN Workshop on Model Checking of Software (D. Bosnacki, S. Leue, Ed.), LNCS 2318, Springer-Verlag, Berlin, 2002.
• [32] Meadows, C.: The NRL protocol analyzer: An overview, Journal of Logic Programming, 26(2), 1996, 113-131.
• [33] Meadows, C.: Formal Methods for Cryptographic Protocol Analysis: Emerging Issues and Trends, IEEE Journal on Selected Areas in Communications, 21(1), 2003, 44-54.
• [34] Meyer, U., Wetzel, S.: A man-in-the-middle attack on UMTS, Proc. 3rd ACM workshop on Wireless security, Philadelphia, USA, 2004.
• [35] Micali, S.: Simple and Fast Optimistic Protocols for Fair Electronics Exchange, Proc. 21st ACM Symposium on Principles of Distributed Computing, Massachusetts, USA., 2003.
• [36] Mitchell, J., Mitchell, M., Stern, U.: Automated analysis of cryptographic protocols using Mur_, Proc. IEEE Symposium on Security and privacy, California, USA, 1997.
• [37] Murata, T.: Petri Nets: Properties, Analysis and Applications, Proceedings of the IEE, 77(4), 1989, 541-580.
• [38] Nieh, B., and Tavares, S.: Modelling and Analyzing Cryptographic Protocols Using Petri Nets, Proc. Workshop on the Theory and Application of Cryptographic Techniques − Advances in Cryptology (J. Seberry, Y. Zheng ,Ed.), LNCS 718, Springer-Verlag, Berlin, 1992.
• [39] Permpoontanalarp, Y. and Sornkhom, P.: A New Coloured Petri Net Methodology for the Security Analysis of Cryptographic Protocols, Proc. 10th Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools, Arhus, Denmark, 2009.
• [40] Permpoontanalarp, Y.: Security Analysis of the TMN protocol by using Coloured Petri Nets : Multi-Session Case, Proc. 10th International Conference on Intelligent Technologies, Guilin, China, 2009.
• [41] Permpoontanalarp, Y.: On-the-fly Trace Generation and Textual Trace Analysis and their applications to the analysis of Cryptographic Protocols, Proc. 30th Formal Techniques for Networked and Distributed Systems (J. Hatcliff, E. Zucca, Ed.), LNCS 6117, Springer-Verlag, Berlin, 2010
• [42] Permpoontanalarp, Y. and Changkhanak, A.: On-the-fly Trace Generation Approach to the Security Analysis of the TMN Protocol with Homomorphic property: A Petri Nets-based Method, IEICE Transactions on Information and Systems, E95-D(1), 2012, 215-229.
• [43] Scyther tool, 2009, http://people.inf.ethz.ch/cremer/scyther, accessed on 1 Nov 2011.
• [44] Shmatikov, V., Mitchell, J.C.: Finite-state analysis of two contract signing protocols, Theoretical Computer Science, 283(2), 2002, 419-450.
• [45] Sornkhom, P. and Permpoontanalarp, Y.: Security Analysis of Micali’s Fair Contract Signing Protocol by Using Coloured Petri Nets : Multi-session case, Proc. 5th International Workshop on Security in Systems and Networks, IEEE press, Rome, Italy, 2009.
• [46] Syverson, P.F.: A Taxonomy of Replay Attacks, Proc. 7th IEEE Computer Security Foundations Workshop, New Hampshire, USA, 1994.
• [47] Tatebayashi, M., Matsuzaki, N., Newman, D.: Key Distribution Protocol for Digital Mobile Communication Systems, Proc. 9th Annual International Cryptology Conference - Advances in Cryptology - CRYPTO ’89 (G. Brassard, Ed.), LNCS 435, Springer-Verlag, Berlin, 1990.
• [48] Turuani, M.: The CL-Atse Protocol Analyser, Proc. 17th International Conference on Term Rewriting and Applications (F. Pfenning, Ed.), LNCS 4098, Springer-Verlag, Berlin, 2006.
• [49] Zhang, Y., Liu, X.: An approach to the formal analysis of TMN protocol, in: Progress on Cryptography: 25 years of Cryptography in China (K. Chen, Ed.), The Springer International Series in Engineering and Computer Science 769, 2004, 235-243.
• [50] Zhang, Y., Wang, Z., Yang, B.: The Running-Mode Analysis of Two-Party Optimistic Fair Exchange Protocols, Proc. International Conference on Computational Intelligence and Security (Y. Hao et al, Ed.), LNCS 3802, Springer-Verlag, Berlin, 2005.