Analyzing Minimization of Counterexamples on Model Checking
Hao Xiong · Journal of Nanchang University · 2008
The paper first introduces the main ideas of the algorithm Gastin.P proposes,and then gives an informal analysis on the well-known Needham-Schroeder public-key authentication protocol,whose result demonstrates that it is very effective for using the algorithm to analyze network security protocols.For the existing shortcoming that the algorithm has to revisited some states already visited in the course of searching the minimal counterexample in Gastin.P algorithm,we proposed a new algorithm framework combining with syntax reordering strategy and effectively solved the problem.Therefore,it is quite efficient of the new algorithm-framework to analyze network security protocols.