The Research Of Automatic Verification For Security Protocol Based On Model Checking

The security protocol is an information interchange protocol which is based on cryptology.But this work is very hard,beacause of the complicacy of protocol goal,environment and attacker model.So it is necessary to use formal methods and tools to analyze and verify security.In all formal methods,model checking is the most promising method for industrial application.It is used to verify the system property.The SPIN is an outstanding model checking tools,it has the strong ability of modeling.Meanwhile,the efficiency of verification also is outstanding.This paper describes the theory,tool and language of SPIN,and it also discusses the modeling method of Dolev-Yao attacker model.The main works and inovations of this paper are following:1.It disscusses the theory and principles and SPIN.2.It builds the operation platform of SPIN in the windows enviroment,this work can be base of other future works.3.It gives a detailed introduction of Promela which is the modeling language of SPIN.The detailed introduction includes the data types,operations,control structures and channel mechanism.This work can be a reference for other works which need Promela language.4.It discusses the Dolev-Yao attacker model which is very important for the verification of security protocol.It gives the formal definition of DY model,and it also builds a framework for the description of actions.This work provides a uniform framework for describing the DY model,it can reduce the artificial affect.5.It uses Promela language to realize the DY model by the framework which is proposed in this paper.It uses this model to veriy tow security protocols-NSPK and A(0),they have different secure goals.The SPIN checker verifies these models automatically,and the results prove the the avaliability of these models.