Research On Security Of E-Commerce Protocols Based On UPPAAL

E-commerce is gradually gaining large-scale application with the fast development of network. Meanwhile, e-commerce security is becoming more and more serious and has become the major concern of shoppers when paying online with credit cards. No e-commerce is acceptable without security. While secure e-commerce protocols are fundamental to e-commerce, a seemingly secure protocol often has security flows. Hence, analysis of various types should be carried out on the properties of an e-commerce protocol, among which protocol verification is of great importance.As an automated verification tool based on time automata, UPPAAL has been successfully used for analyzing the security and liveliness of communication protocols. But it was known that UPPAAL was seldom used to analyze the security of e-commerce protocols.This paper's main contribution is the failure analysis of e-commerce protocol using UPPAAL. The contributions include: the ISI protocal is verified, verification results show that fairness does not hold for ISI payment protocol; A model concerning the participants of the anonymous and retrievable fair exchange protocol is built by UPPAAL, verification results show that fair exchange protocol satisfy liveness and time efficiency. The security properties of single run of fair exchange protocol Franklin/Reiter in unreliable environments are analyzed by UPPAAL. Result show that when running in unreliable environments, the secure e-commerece protocol may become insecure, in which case the message sequence given by UPPAAL is utilized to investigate the reasons and carry out corresponding modifications to obtain a secure protocol again. All results in this paper show that UPPAAL is specifically applicable to unreliable environments and can improve the protocol by utilizing the generated message sequence.