Model Checking Applications In Security Protocol Formal Verification

Information plays an important role in contemporary society. The analysis of securityis very important to communication. There are many formal verification methods，suchas modal logic，theorem proofing and model checking methods. By using someformulas, modal logic can easily check the expectations. BAN, SVO and Kialar areuseful modal logic. By defining the operating process and using proposition，thetheorem proofing can check the defects. The Isabelle and strand space are very populartheorem proofing methods. But by the updating and development of invasiontechnology, these means are not as useful as before. The modal logic way is easy tounderstand, but it can not provide the specific content of the defect. Theorem provingmethods is a significant improvement compared to modal logic. It can test out where theproblem lies, but the detecting mainly focuses on correctness. However, these twomethods are effective in verifying the early security protocols. The application of modelchecking in security protocol detecting is later than these means, but it becomes morewidely used. This method was used to work in hardware verification. By the end of thelast century, this method was introduced to the field of security protocols verification, inwhich it has experienced a rapid development stage. Model checking is an automatedverification technique, which greatly reduces the human intervention. It can provide thecounter-example when the verification does not meet the system model.Firstly，this thesis introduces the basic theories of cryptography and securityprotocols. Then it presents the theory of formal methods and formal techniques. Afterthat this thesis introduces the working principle of model checking methods and SMV.Then this thesis researches some security protocols by strand space technology. Finally,this thesis verifies the Otway-Rees protocol and NSPK protocol. By taking thesemethods to test whether there are loopholes in the two protocols. It proves that theprevious method is right, and also the model checking method is effective.