Model checking of SSL 3.0 protocol based on SPIN

Model checking is to check whether a bounded state system can meet their design specifications using state-space search approach automatically. This paper describes the key exchange protocol SSL 3.0, and conducts a formalized analysis and modeling and verification of the protocol by using the famous model checker tool SPIN. The LTL property is dynamically changed during the verification which can reduce the transition of model space and make the search more efficiently. The experimental results show that this method of verification is correct, certificate the safety and feasibility of the protocol itself, and improve the verification efficiency of the protocol.