Abstract
In this paper, we present a Petri net based methodology for the formal modelling and analysis of cryptographic protocols. We set up modelling rules that represent the protocols in terms of Petri nets. The modelling produces formal descriptions for the protocols with good visibility and layered abstraction. In particular, the descriptions clearly visualize the causal relations and constraints among the data flows in the protocols. An intruder model is introduced to formulate intruder attacks and to generate test cases against the cryptographic protocols. A procedure that exhaustively generates the test cases and searches for states that violate specified security criteria, is also proposed. We demonstrate the value of this methodology by applying it to a number of published protocols. In this way, we are able to reveal security flaws of these protocols. This methodology is applicable to both public-key and private-key based cryptographic protocols.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
D. Dolev and A. C. Yao, “On the security of public key protocols,” IEEE Trans. Infor. Theory, vol. IT-29, no. 2, pp. 198–208, March 1983.
R. A. Kemmerer, “Analyzing encryption protocols using formal verification techniques,” IEEE J. Selected Areas in Commun., vol. 7, pp. 448–457, May, 1989.
J. K. Millen, S. C. Clark and S. B. Freedman, “The interrogator: Protocol security analysis,” IEEE Trans. Software Eng., vol. SE-13, no. 2, pp. 274–288, 1987.
C. Meadows, “Using narrowing in the analysis of key management protocols,” in Proc. IEEE Symp. Security and Privacy, Oakland, California, pp. 138–147, 1989.
D. Longley and S. Rigby, “An automatic search for security flaws in key management schemes,” Computers & Security, vol. 11, no. 1, pp. 75–89, 1992.
M. Burrows, M. Abadi and R. Needham, “A logic of authentication,” ACM Trans. Computer Systems, vol. 8, no. 1, pp. 18–36, 1990.
P. V. Rangan, “An axiomatic theory of trust in secure communication protocols,” Computers & Security, vol. 11, no. 2, pp. 163–172, 1992.
C. A. Petri, Kommunikation mit Automaten. PhD thesis, Bonn: Institut für Instrumentelle Mathematik, Schriften des IIM Nr. 3, 1962.
T. Murata, “Petri nets: Properties, analysis and applications,” Proc. IEEE, vol. 77, no. 4, pp. 541–580, April 1989.
K. Jensen, “Coloured Petri nets: A high level language for system design and analysis,” in Advances in Petri Nets 1990, vol. LNCS-483, pp. 342–416, Springer-Verlag, 1991.
T. Suzuki, S. M. Shatz and T. Murata, “A protocol modeling and verification approach based on a specification language and Petri nets,” IEEE Trans. Software Eng., vol. 16, no. 5, pp. 523–536, May, 1990.
M. Diaz, “Modeling and analysis of communication and cooperation protocols using Petri net based models,” Computer Networks, vol. 6, no. 6, pp. 419–441, 1982.
J. Burns and C. J. Mitchell, “A security scheme for resource sharing over a network,” Computers & Security, vol. 9, no. 1, pp. 67–75, 1990.
C. H. Meyer and S. M. Matyas, Cryptography: A New Dimension in Computer Data Security. New York: John Wiley & Sons, 1982.
G. V. Bochmann, “Protocol specification for OSI,” Computer Networks and ISDN Systems, vol. 18, pp. 167–184, 1989/90.
G. Berthelot, “Checking properties of nets using transformations,” in Advances in Petri Nets 1985, vol. LNCS-222, pp. 19–40, Springer-Verlag. 1985.
B. B. Nieh, “Modelling and analysis of cryptographic protocols using Petri nets,” Master's thesis, Electrical Engineering, Queen's University, Kingston, Canada, 1992.
N. Behki and S. E. Tavares, “An integrated approach to protocol design,” in Proc. IEEE Pacific Rim Conf. on Commun., Computers and Signal Processing, pp. 244–248, June 2–4 1989.
C. Meadows, “A system for the specification and analysis of key management protocols,” in Proc. IEEE Symp. Research in Security and Privacy, Oakland, California, pp. 182–195, May, 1991.
B. B. Nieh and S. E. Tavares, “Modelling and analysis of secure communication protocols using Petri net formalism,” in Proc. Canadian Conference on Electrical and Computer Engineering, Quebec, P.Q., Canada, pp. 37.3.1–37.3.4, Sept 1991.
R. M. Needham and M. D. Schroeder, “Using encryption for authentication in large networks of computers,” Commun. ACM, vol. 21, no. 12, pp. 993–999, 1978.
D. E. Denning and G. M. Sacco, “Timestamps in key distribution protocols,” Commun. ACM, vol. 24, no. 8, pp. 533–536, 1982.
V. L. Voydock and S. T. Kent, “Security mechanisms in a transport layer protocol,” Computers & Security, no. 5, pp. 325–341, 1985.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Nieh, B.B., Tavares, S.E. (1993). Modelling and analyzing cryptographic protocols using Petri nets. In: Seberry, J., Zheng, Y. (eds) Advances in Cryptology — AUSCRYPT '92. AUSCRYPT 1992. Lecture Notes in Computer Science, vol 718. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57220-1_69
Download citation
DOI: https://doi.org/10.1007/3-540-57220-1_69
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-57220-6
Online ISBN: 978-3-540-47976-5
eBook Packages: Springer Book Archive