Modelling the Needham-Schröder authentication protocol with high level Petri nets

Reference:

Tuomas Aura. Modelling the Needham-Schröder authentication protocol with high level Petri nets. Technical Report B14, Helsinki University of Technology, Digital Systems Labora tory, Espoo, Finland, September 1995.

Abstract:

In this paper, security of the Needham-Schr<F6>der 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 transitions, are discussed. Introduction of set type places or negative arcs in the net formalism is proposed as a solution for reducing the storage space requirements of the reachability graph. In experiments with the reachability analysis tool PROD, the model proved efficient in detecting protocol failures. Further optimization of the formalism and tools is necessary for the presented methods to be useful in full verification of real size protocols.

Keywords:

Cryptographic protocols, Needham-Schr<F6>der, formal model, Petri nets, Pr/T nets, PROD

Suggested BibTeX entry:

@techreport{HUT-TCS-B14,
    address = {Espoo, Finland},
    author = {Tuomas Aura},
    institution = {Helsinki University of Technology, Digital Systems Labora tory},
    month = {September},
    number = {B14},
    pages = {32},
    title = {Modelling the {N}eedham-{S}chr{\"o}der authentication protocol with high level {P}etri nets},
    type = {Technical Report},
    year = {1995},
}