Symbolic model checking analysis for CMP1 protocol
Mei Zhang · Journal of Naval University of Engineering · 2005
A new approach is proposed for analyzingthe non-repudiation and fairnessproperty of E-commerce protocols. The authentication E-mail protocol CMP1 is modeled as finite state machine, and their two vital aspects of non-repudiationpropertyand fairness propertyare analyzed byusing SMV. It is found that the fairness property can not be satisfied, and thus some corrections are made on the finite state machine of CMP1 protocols. This result shows that it is effective to analyze and check the new property of E-commerce protocolsby the symbolmodel checker.