Incremental SAT-based Formal Verification Of Security Protocols

With the incessant of advancement of computer and network techniues, as well as its application in broader fields, the security of network has become the main requirement. The security protocols, which is developed for this purpose, plays very important role in the communication procedure. However, the security leaks, which is the the result of the flaw because of the protocols itself, become severe problem in the network security. Therefore, more and more people pay much more attention to the design&analyse of the security protocols.The design of the security protocols supplies the standard for the security protocols while the analysis of security protocols can make the security protocols accomplish the security capability. Besides, these are attended by more and more people because of the fast development of the computer networks. Formally analyzing the security protocols is included in those works.Formal analysis of the security protocols consists of three methods, formal logic, model checker and theorem proving. Model checker, which is the important method and technique of the formal analyze, plays an important role in the analysis of security protocols. One of those methods named as SAT-based model checker has been used. The main work for us includes doing the research in the formal analysis of security protocols referring to three methods and especially paying more attention to the method of SAT-based model checker, which is constituted by SAT-compiler and SAT-solver. We make good use of the idear and put forward a new method-A incremental SAT-based formal verificaiton of security protocols. Our work refers two parts: the realization about the incremental satisfiability compiler and incremental satisfiability solver.