On The Model Checking And Design Of Mobile Electronic Commerce Protocols

At present,mobile electronic commerce is taking on extremely driving impetus all over the world and it is developing rapidly in our country too.Security is the most important problem when people use mobile electronic commmerce.The security of mobile electronic commmerce protocol is one of the important aspects of the security of mobile electronic commmerce.Mobile electronic commerce protocol is a special kind of electronic commerce protocols.Compared with traditional electronic commerce protocols,the environment of mobile electronic commerce protocol is more complicated because of the characteristics of mobile devices and wireless networks,which mades it more error-prone and brings new challenges for its formal analysis and design.This dissertation studys the model checking and design of mobile electronic commerce protocols(including wireless authentication protocol for it is the basis of mobile electronic commerce protocols).The main results that the author obtained are as follows:(1)Wireless authentication protocol Server-specific MAKEP is analyzed using symbolic model checker—SMV.The existing authentication flaw of the protocol is discovered and the effect of the flaw is discussed.(2)For the existing authentication flaw of Server-specific MAKEP,an improvement is given and the improved protocol is analyzed using model checking too.The result shows that the improved protocol satisfies the security goals.(3)For mobile electronic commerce protocols, a modeling method based on finite automata is proposed.Using this method,a typical mobile payment protocol KSL is analyzed as an example.The fairness flaw of the protocol is discoverd and an improvement is given.(4)For the characteristics of mobile devices and wireless networks,a fair payment protocol in mobile environment is designed.Some properties such as fairness,confidentiality and timeliness of the protocol are verified using model checking.The result shows the feasibility of the protocol.