The Formal Verification And Improvement Of Set Protocol Based On Model Checking

With the development of e-commerce, people have paid more attention to itssafety. The SET protocol is the key protocol in the e-commerce, the importance of itssecurity is self-evident. Formal method is the important analysis method of protocolsecurity, it has the characteristics of rigor and accuracy and it has become animportant way to verify the security of network protocol. As the very importantmethod in formal method, model checking has been successfully applied to verify thesecurity of network protocol.Because the security problem of protocol is very subtle, the vulnerabilities ofsome uncomplicated protocols need a long time to be found. Morever, analyzing thesecurity of SET protocol to find the potential safety hazard or prove its safety is ofgreat significance for the further development and application of SET protocol.In this paper, we apply model checking method to analyze formally and verifythe SET protocol. Firstly, this paper introduces the related theories.Such as the formalanalsis of protocol, Model Checking technology, verficiation tool named SPIN,Promela language, Lineral temperol logic LTL, and so on. Then, the article describesand analyzes the principle and each phase of payment process of SET protocol,adopts the process of payment based on simplified model of SET payment protocolproposed by Lu&Smolka, and the protocol is modeled formally by the Promelalanguage. Under the hypothesis of the network environment being controlled by theintruder, use SPIN to find the attacks. In order to improve the verification efficiency,we use the optimization strategies of atomic, d_step, partial order reduction and Bit–state hashing to relieve the state space explosion and reduce the storage space.Finally,improving the existing vulnerabilities of the SET protocol.Morever, using modelchecking tool SPIN to verify the validaity of the imporved the SET protocol again.