Symbolic Model Checking and Analysis for E-Commerce Protocol
Jinghua Wen, Mei Zhang, Xiang Li · Journal of Electronic Science and Technology · 2005
A new approach is proposed for analyzing non-repudiation and fairness of e-commerce protocols. The authentication e-mail protocol CMP1 is modeled as finite state machine and analyzed in two vital aspects - non-repudiation and fairness using SMV. As a result, the CMP1 protocol is not fair and we have improved it. This result shows that it is effective to analyze and check the new features of e-commerce protocols using SMV model checker. The widely use of networks and e-commerce has brought great convenience to our daily life. The basis of normal e-commerce transaction between the seller and customers is the secure e-commerce protocols which must also include the two important properties, namely, non-repudiation and fairness, in addition to those basic properties such as secrecy, security, authentication and integrity (1) . So there are special and higher demands of the performance and function of the e-commerce protocol. To attain this goal, the e-commerce protocols must be analyzed with special formal analyzing tools. BAN logic method (was published first by Burrows, Abadi and Needham), stand space method, process algebra, computing information theory method and Petri net method are some influential ones in the past years. In the middle 1990s, Kailar noticed the importance of the formal analyzing of accountability and non-repudiation in e-commerce protocols firstly, and he advanced the famous Kailar logic. But Kailar logic has so many non-formal hypotheses and cannot be used to analyze fairness. Model checking method check whether a finite state system meets its design specification automatically using the state space searching methods (2) . The advantages of the method lies in its automatic checking process and high checking speed and efficiency, and it can give the reason why a certain property doesn't meet the needs, according to which the system can be improved. The method has greatly developed since its birth. Model checking doesn't have those disadvantages existing in Kailar logic, and has been used in the security protocol checking area gradually. But e-commerce protocol checking with model checking is staying in elementary level, mainly used in conventional properties checking such as security, authentication and integrity. This paper will model, analyze and check the new features of e-commerce, that is, no repudiation and fairness, using the model checking method. And via the actual analysis checking of the email protocol CMP1, we have found that this protocol doesn't meet the fairness requirement.