Analyzing for Fairness Electronic Commerce Protocol Formally

Abstract

A new approach is proposed for analyzing fairness and non-repudiation of electronic commerce protocols in this paper. The authentication E-mail protocol (Certified electronic mail) is modeled as finite state machine, and analyzed in two vital aspects: Fairness and non-repudiation using Symbol Model Verification. The Analysis shows that, the certified electronic mail protocol is unfair, so we need to improve it. This result shows that it is effective to analyze and check the new features of electronic commerce protocols using model checker of Symbol Model Verification.