On The Model Checking And Analysis Of Wireless Authentication Protocol

The environment of mobile electronic commerce protocol is more complicated because of the characteristics of mobile devices and wireless network, which makes it more error-prone and brings new challenges for its formal analysis.This paper studies the wireless authentication protocols with Model Checking technology SPIN. It introduces concepts and classification of cryptographic protocols, and gives classification of wireless networks and the implementation of environmental, and then presents theory technology to analyze cryptographic protocols. This paper researches analysis method about Model Checking tool SPIN and Promela language in detail. Based on Model Checking technology, this paper explores the use of SPIN for the modeling and checking of Aziz-Diffie protocol. The existing authentication flaw of the protocol is discovered and the improved protocol is analyzed using model checking too.