Analysis And Research Of Electronic Commerce Protocol Property Based On Logic

Currently, electronic commerce is the heat point of the research and development in each country, Popularization and acceptance of electronic commerce mainly depends on solution of the following properties: security, atomic, privacy and anonymity. Electronic commerce protocol is the comprising framework of electronic commerce, and its security is the key factor to decide the development of electronic commerce. Formal description and analysis are an efficient way to describe electronic commerce protocol and verify their properties. The research in electronic commerce protocols and their security is helpful for designing safe electronic commerce protocols and promoting the development of electronic commerce.Modal logic, as one of formal methods, is perhaps the best known and most influential method, which consists of various statements about belief in or knowledge about messages in a distributed system, as well as inference rules for deriving new beliefs from available belief and /or new knowledge from available knowledge and beliefs. The former corresponds to logic belief, while the latter logic of logic knowledge is useful in analyzing the properties of protocols. BAN is one of logics that got a big frame for its success in analyzing security protocols.In this paper, BAN logic and the extended BAN logic are primarily introduced, and studied in their advantages and weakness. Combing the advantages, we apply a new formal logic language to analyze electronic commerce protocol and their properties. The language has a strong logic and can be applied easily. A famouselectronic micro-payment protocol--NetBill protocol is also simply introduced andabstracted , At last, the abstracted protocol is especially analyzed and verified completely by the new logic.