A Reduction method for Verification of Security Protocol through CPN

Model checking is an excellent candidate for analysis and verification of security protocols. However, it suffers from a big drawback of state space explosion. The goal of the paper is to deal with state space explosion problem. By use of coloured Petri nets to model check security protocols, reasons for state explosion are analyzed and general reduction methods are compared. Further, a control method is introduced and improved for reduction of state space through CPN in the paper which is proved to be effective through an STS protocol illustration. The control method is implemented through three modeling steps of full model, lazy model and control model and is assisted through a new tool called firing control graph to simplify the procedure.