| "37th Statistical Report on Internet Development in China" which issued by CNNIC (China Internet Network Information Center), indicate that 42.7% of Internet users encountered network security issues in China. With the growing population of online shopping people, e-commerce security problems arouse much concern. In China, online shopping users reached 413 million, at the same time, 16.4% of consumers encountered the network consumer fraud by 2015. Thus, both network security and transaction security are important to ensure the further development of e-commerce.Trade agreements are the key point to transaction security. This article focuses on transaction security, and select B2C e-commerce model as a research object. Formal analysis and verification of e-commerce transaction protocols are based on model checking method. In order to ensure the completion of the normal, reliable and secure transactions rules between customers and merchants. Its main content is as follows:Introduce the subject background, theory foundation and the present situation that use of formal methods to analyze security protocol development process and research.Analyze e-commerce transaction protocols of B2C mode briefly. Expounds the design principle of e-commerce transaction agreement, such as anonymity, non-repudiation, fairness, safety,-etc. Then described buyers, merchant sites, third-party payment platform and bank with Promela language.Formal verification and model the transaction protocols through model checking. Then use LTL formulation to describe the e-commerce transaction protocol properties. According the transaction protocols running trace to analyze the loopholes of the B2C trading agreement.Put forward an improved model to standardize transaction process and protecting the privacy of the buyer. Add two entities to the current e-commerce transaction model of B2C mode the original model, such as the logistics and privacy proxy server. |
PDF Full Text Request