Formal Analysis And Vulnerability Detection Of E-Commerce Protocol

Electronic commerce (E-commerce) protocol, which is the key of security system, provides safe guard for the e-commerce. Besides some common security properties like secrecy and authentication, e-commerce protocol also need to meet atomicity, anonymity and non-repudiation, etc. The e-commerce protocol’s design and vulnerability detection is the main focus and difficult point of current research, therefore analyzing whether an e-commerce protocol is safe and effective, as well as fixing the security vulnerabilities, is very important. This paper’s research is mainly about e-commerce protocol’s formal analysis and vulnerability detection, and the main innovations are as follows:Firstly, based on briefing model checking tool FDR and modeling tool Casper, this paper analyzed the intruder’s abilities and its actor model in the protocol system generated by Caper/FDR.Secondly, it extended the model checking method for analyzing e-commerce protocol, and found several unknown security problem from an e-commerce protocol, security vulnerabilities were fixed and their mechanism were discussed.Thirdly, based on giving two e-commerce protocol’s enhancive definitions, it proposed formal analysis for extend atomicity with CSP theory, the unconventional model was set and checked by FDR, and improvements for the protocol were proffered as well.Lastly, this paper proposed a new model checking method based on CSP theory for analyzing e-commerce protocol’s anonymity, it also gave a model frame which is suitable for model checking method with CSP/FDR, and though the experiment on a specific e-commerce protocol it showed the detailed modeling and analysis process.The research result indicated that using CSP theory and relevant model checking tools Casper and FDR2 which are based on the finite state machine concept, will efficiently detect whether the significant properties such as secrecy, authentication and anonymity are satisfied or not in the e-commerce protocol. This method will play an important role in ensuring the protocol runs smoothly.