Security Protocol Analysis And Verification Based On Model Checker SPIN

As the rapid development of Internet, the security protocols have played very important role on the exchanged message. Formal methods are the most important methods to analysis and verify the security protocols. Such as the provable theory, BAN logics, strand space model and model checking.Model checking, as one of the formal methods has many good advantages, such as automatism and providing the violate example. Recent years, model checking has been popular in verifying the hardware designing. Model checker SPIN is developed by the Bell Lab and it can be used to analysis and verify software and protocols.Based on the model checker SPIN , this paper is analysis and verify the security protocol Netbill, which is one of the business protocol developed by the Carnegie Mellon University. First we abstract the protocol from two aspects: the behaviors and the correct properties. The protocol's behavior abstraction includes the definitions of actions, states and the events the protocol takes when the states translate. Second, we use the PROMELA language to establish the verification (valid) model .We use the model to simulate the behavior of the protocol and to verify the correct properties the protocol should establishes. SPIN provides several form to specify the correct properties, such as the assert states and LTL formula. The properties or the parameter we choose may not adapt to the model, so we need to change the model's behavior or the verification parameter. Finally, we compare the result with other formal methods and present the work we should do in the future.