In: Helsinki University of Technology, Digital Systems Laboratory, Technical Report B14, pages 1-32. September 1995.
Abstract: In this paper, security of the Needham-Schrder key distribution protocol is modelled and analyzed with predicate/transition nets, and along that, a methodology for modelling cryptographic protocols with high level Petri nets is developed. The main goal is clarity of the model and its feasibility for automated analysis. The intruder and the communication channels are modelled as one entity that has complete control over all messages in the system. The intruder model is based on the concepts of memory and learning. Special care is taken that the model captures all possible actions of the intruder. Guidelines are given for finding the minimal number of model parts that represents a system with an arbitrary number of entities and concurrent protocol runs. Techniques of coping with state space explosion in reachability analysis, the stubborn set method and prioritizing of