The SET Protocol Payment Process Analysis And Model Checking

In the electronic commerce field, the security problem is a very sensitive but important problem, it is the key that the electronic commerce can develop healthily. The SET( the Secure Electronic transaction) electronic commerce protocols are the safety Electronic exchange norm that was established by two big and international credit card companies of MasterCard and Visa in 1996. It provided attestation to the consumer, merchant and bank, insuring the confidentiality, reliability non-denial property, assuring the safety of using credit card for on-line shopping under open the network environment, having already acquired the extensive application, and producing the huge economic benefits and social benefits from here. But it is very delicate for the security problem of protocols, some protocols are not complicated in oneself but their security flawscan not discover until have used very long time . Therefore, to analyze SET thoroughly, finding out the flaws or verifying the security, will do benefit for the protocol' s further application and development.The main research purpose of this paper is to adopt the model checking tool SMV to validate the SET payment protocols. Under the condition of which Lu & Smolka set up the simplification model of the payment process to the SET protocol for research object, build up its formal model and finite state machine model, as well as CTL formulations of the security properties are presented. Under the assumption of the network environment being controlled by the intruder, the protocols is analyzed by SMV model checking tool. The results show that Lu & Smolka set up the simplification model of the payment process to the SET protocol have discovered two attacks, that allows a dishonest user to purchase a good debiting the amount to another user. The main key technique and the work that we do is as follows: Study the method of verifying the safety protocol(1) Not formal method.(2) Formal method. Study the model checking(1) Model checking technique analyzed protocol' s method .(2) Model checking tool, making sure the SMV as tool to put up the model checking to safety protocol. Introducing the symbol model checking tool SMV(1) SMV work mechanism.(2) The syntax definition of the SMV language etc.. The SET protocol and its payment process analysis(1) The main target that the SET protocol to attain, the work principle, encrypts the technique, participant etc—(2) The SET protocol's payment process mainly include purchase request , payment authorization, payment acquire three protocols, carried on the detailed analysis to performance process and its steps that these three...