A New Authentication & Registration Protocol and Its Bounded Model Checking
Xi Bai, Ji-Gui Sun, Ze-Hai Li · 2006
Since formal method has features including accuracy, brevity and non-ambiguity, it plays a more and more important role in the verification of mobile communications protocols. According to the security protocol of wireless networks, a general method of finite-states-modeling was proposed and the security protocol is verified formally with the model checker SATMC. A new authentication & registration (AR) protocol was also presented here. Experiments show that the bounded model checking based on SAT is an efficient method of verifying security protocols formally. The protocol can resist the attacks of playback and masquerade and also reduce the computation complexity of the user's communication devices while the protocol is running.