Secure E-commerce Protocol Logic Analysis Method

Currently, electronic commerce is the heat point of the research and development in each country. Electronic commerce protocol is the comprising framework of electronic commerce, and its security is the key factor to decide the development of electronic commerce. Security electronic commerce protocol which uses the cryptographic methods for network communication, its goal is to provide security services in the complex and insecure environment. The purpose of the security electronic commerce protocol is to ensure the security of the information. But if there are some leaks in the protocol itself, attackers will use the leaks to cause harm to the legitimate communications. Hence we need to analyze and test the protocol to verify that the protocol is expected to achieve its security goals.Kailar logic and Qing-Zhou logic have been proved to be the very useful formal methods for analyzing security electronic commerce protocols, but there are still some limitations. And they can not rightly analyze the accountability when the replay attack happens. We have made the following aspects of work on the basis of the study of the formal methods:(1) We have studied the security property of the security electronic commerce protocols, in particular the atomicity,the accountability and the fairness.(2) We have studied the common attacks to the security electronic commerce protocols. This paper analyses IBS and CMP when the replay attack happens, and gives the scheme of the improving CMP.(3) This paper analyses the limitations of Kailar logic and Qing-Zhou logic. An improved logic is put forward to analyze security electronic commerce protocols. At last, two abstracted protocols are especially analyzed and verified completely by the improved logic.