Design And Implementation Of Model Checking Platform For Security Exchange Protocol

With the development of computer network technology and the popularity of electronic commerce, electronic data interchange becomes more and more important, which the safety, fairness and other issues also plagued the supplier and consumer of electronic commerce. As the basis of electronic commerce protocols, security exchange protocol provides an effective solution for data exchange problem. Due to the importance state, complexity and asymmetry structure of security exchange protocol, the analysis of such protocols has become a hot research to Pic in the field of information security in recent years. At present, there are some analysis methods of security exchange protocol at home and abroad, including Paulson induction, CSP formal modeling method, and a string of space model method, etc.After doing research in the field of security exchange protocol analysis, based on extended applied Pi-calculus and linear temporal logic assertion, this paper presents a nativemethod for security exchange protocol analysis, and implements the model checking platform by Antlr and C# programming language. The main research context is listed as below: Firstly, by abstracting from security exchange protocol, this paper give definitions of fairness and non-repudiation, and using temporal logic to formal such properties. After doing this, transfer LTL formula to Bu?chi automata. And this paper has extended Pi-calculus of Proverif by the choice operator to model security exchange protocol. Then, DY model was modified with respect to the RCC assumption to verify these properties, intruder model can be generated automatically according to protocols. Based on the work above, Pi-calculus model with attacker was transferred to Labeled Transition System. Finally, MoveOneStep and Tarjan algorithm was incorporated to explore the state space On-the-fly. The search of state space in Bu?chi automata and LTS will be stopped if an attacking was found.To illustrate the feasibility of the proposed approach, we have analyzed several security exchange protocols, and the results show that our method can detect attacking trace effectively. The research in this paper has significant meaning in the field electronic business both theoretical and practical.