Research On Formal Analysis Method Of The Security Of E-commerce Protocol

E-commerce protocol is designed to fulfill business flow and prtotect the attender's profit using cryptography technical. So, it is a common sense that the formal analysis of the security of E-commerce protocols is an important and difficult problem.The study of formal analysis methods for E-commerce protocol security is later than that for traditional cryptographic protocol. There are many active formal analysis methods for E-commerce protocol, such as:Kailar logic, SVO logic, model checking using SMV, game analysis based on ATL/ATS system and methods proposed by Prof. Si-Han Qing, which could be used to analyze or prove the security of two party or multiple party fair exchange protocols. Some of these methods focus on the analysis of the message or focus on the structure of the protocol. Few formal analysis method could consider the message and the structure of a protocol at the same time. At present, formal analysis methods of E-commerce protocol is still a hot research area.The first part of this paper researchs the major game logic systems, for example:ATL, ATEL, ATL-A/ATEL-A, MMAL, and found that these game logic system model the status of game agent with fixed state machine. Based on this finding, IA(Intelligent Agent) model is proposed, in which the agent update its status based on message he received and the logical inference rules. And in every status, the agent reason about what could he send using the inference rules. Multiple IAs constitute one MCGS(Message based Concurrent Game System). ATL-B, which includes epistemic logic propositions, extended from ATL, is used to model the system strategies. IA, MCGS, ATL-B together constitute a tool of modeling the system, known as the MIAG (Multiple Intelligent Agent Game) system which is characterized by that the game agent interact through message only and each agent has its own logical inference rules for the renewal of its state.In the second part, Using MIAG, this paper built a new E-commerce protocol analysis model, in which the game agent update its epistemic state using the logical inference rules; ATL-B strategy formula could express different security goals, for different E-commerce protocol. In the new model, participates are divided into honest agent set and dishonest agent set. Then, given every trace of the honest agent in the target protocol, the strategy of dishonest agent are analyzed to check weather it has strategy to get more benefit then the honest agent. In this paper, four typical attack strategies are identified which is more reality then those defined in the other formal analysis methods proposed before.In third part, one fair exchange protocol, Nenadi04, and one non-central E-voting protocol, Su-Vot are analysised using the new model. Flaws are found in these protocols, which confirmed the validity of the new model. When analyzing Nenadi04, we found that the non-repudiation evidence dose not satisfy accountability and also, the initiator of Nenadi04 could launch a number of recovery sub-protocols to confuse the responder with messages for different instance, thereby break the fairness of Nenadi04. The analysis of Nenadi04 exemplified that the new model could analyze fair exchange protocols from both the message and structure point of view at the same time. The dishonest voter in Su-Vote protocol could modify the voting result and have strategy to control weather the protocol could finish in time.In the last part of this paper, we propose and define the traceability of concurrent signature to bind the signer and message together to prevent the abuseness. Based on improved Perfect Concurrent Signature proposed by Guilin Wang, this paper designed one concurrent signature scheme, which satisfy the traceability, based on which one fair exchange protocol without trusted third party is proposed.