Design And Analysis Of Electronic Commerce Security Protocols

With the development of information and network technologies, electronic commerce (e-commerce) has become an important symbol for Internet and information technologies. Meanwhile, the security problem of e-commerce is becoming more and more serious. It has been drawn attention by many scholars and engineering technologists. The e-commerce security protocols are the key technologies to ensure application and growth of e-commerce. The basic security properties of general security protocols include authentication, integrity and confidentiality. More properties are included in e-commerce security protocols e.g. non-repudiation, accountability, fairness, atomicity and anonymity. The design and analysis are more complex for e-commerce security protocols than general security protocols. Practice shows that security vulnerabilities have still existed even if the protocols are designed meticulously, and these vulnerabilities are difficult to find utilizing informal analysis methods. It is a wise choose to analyze e-commerce security protocols using formal methods. Formal analysis can find security vulnerabilities and flaws of the protocols. The analysis results can be used to guide the design of the protocols. Further more, the potential problems of the protocols can be mended. So the researches on the e-commerce security protocols and their formal analysis methods have important theories and realistic significance.The thesis does below researches around the design and logic analysis methods of the e-commerce security protocols.1. Researches on e-commerce security protocols. This thesis studies the typical logic analysis methods for the e-commerce security protocols, and discusses their advantages and disadvantages. Using SVO logic and Qing-logic, two e-commerce security protocols are analyzed. Some security vulnerabilities are found for them and several improved protocols are proposed correspondingly. The YAHALOM protocol is analyzed by using SVO logic. The analysis results show that the protocol cannot against the reply and impersonation attacks. By modifying message format and adding handshake messages, an improved YAHALOM protocol is proposed. The reason results of the improved YAHALOM protocol reveal that the protocol completes the strong goals of identity authentication and key negotiation. In response to the flaws of the CMP1 protocol, this thesis proposes a new fair accountability protocol by adopting cryptographic hash function operation to protect the confidentiality of the mail messages. The proposed protocol is verified to satisfy accountability and fairness by utilizing the extended Qing-logic.2. Researching on logical method for protocols. This thesis researches the typical method of protocols logical analysis and points out their limitations. Most of them are lack of formal semantics and analysis of hybrid cryptosystem-based protocols. In response on the above-mentioned problems, this thesis proposes a new logic analysis method, which can analyze almost all of the known security properties of the e-commerce protocols, such as authentication, secrecy of key, non-repudiation, accountability, fairness and atomicity. This thesis gives logic sentences, axioms and inference rules for new method. Combining new logic with strand space theory, this thesis describes semantics of the logic sentences in the new logic and proves the correctness of the inference rules. The validation of the new logic is verified by analyzing the anonymous e-cash payment protocol. The analysis reveals the security vulnerabilities of the protocol, which cannot satisfy non-repudiation of merchants, secrey of key, accountability, fairness and atomicity, moreover, the customers face malicious cheat of the merchants.3. A novel e-commerce protocol. In response on the existing problems of the e-commerce protocols, e.g. security goal is single, increasing security requires are not been satisfied. This thesis proposes a compound security protocol, which have general security properties required by e-commerce protocols. The new protocol includes authentication sub-protocol and payment sub-protocol. The authentication sub-protocol cannot only against personating transaction entities and messages replay attacks, but also resist DoS attacks effectively. Moreover it needs fewer messages to authenticate identities of important entity in the foremost time, as well as session keys used for transaction are negotiated efficiently. The payment sub-protocol is designed by improving the anonymous e-cash payment protocol. To realize its non-repudiation, certificates are used to prove the identities of the transaction entities. To avoid unfairness arisen by the dishonest transaction entities, the transmission of payment receipt is achieved by the trusted party. The proposed protocol uses FTP to transmit electronic cashes and payment receipts, which ensures achievement of accountability and fairness, and enhance the robustness of the protocol. The verification result of the protocol using the new logic indicates that it satisfies authentication, secrecy of key, non-repudiation, accountability, fairness and atomicity.4. Combining the above-mentioned researches, the thesis summaries the requirements of the e-commerce protocols and concludes the protocols design rules. The rules provide references for the design industrial standards of e-commerce protocols, and guide the design and application of the protocols. Implementing above rules, a typical micro-payment protocol is analyzed and redesigned. Micro-payment is a kind of the typical application of e-commerce. Its security and efficiency are regarded as the key factors in its design and implementation. The thesis studies the NMP protocol based on the conventional hash chains firstly. Some shortness or flaws are found in it, including user's malicious overdraft and executive timeliness. In addition, the use of conventional Hash chains has length limitation, so it is not easy to renew the authentication root of a Hash chain. That means the micro-payment protocols based on conventional Hash chains have low working efficiency and security. In response on the above problems, this thesis proposes a new micro-payment protocol based on self-updating Hash chains. A comparison between the proposed protocol and the NMP protocol shows that the former not only solve the latter's problems, but also improve efficiency and fairness. The analysis results show that the storage and communication load of the former is only 80 bytes longer than the latter, whereas the average computation efficiency of the former is 125 times higher than the latter under a transaction accomplishment of 10000 electron shares.