Title :
Analyzing a Fair Exchange E-commerce Protocol Using CSP and FDR
Author_Institution :
Dept. of Comput. Sci. Eng., Shanghai Jiao Tong Univ., Shanghai, China
Abstract :
In this paper, we analyze a Fair Exchange E-Commerce Protocol within the framework of CSP and its model-checking tool FDR. We model the protocol and some of its desirable properties, such as money atomicity, goods atomicity and validated receipt. However, some of these essential properties may be violated in the presence of site or communication failures. Using the model checking approach we can evaluate which failures cause the violation. The formal analysis of the results may suggest a mechanism to deal with these failures and ensure true fairness of the protocol.
Keywords :
communicating sequential processes; electronic commerce; formal verification; protocols; CSP; FDR; communicating sequential process; failure divergence refinement; fair exchange E-commerce protocol; formal analysis; model-checking tool; Computer science; Counting circuits; Cryptography; Electronic commerce; Electronic learning; Failure analysis; Helium; Internet; Protocols; CSP and FDR; e-commerce; failure; model checking;
Conference_Titel :
e-Education, e-Business, e-Management, and e-Learning, 2010. IC4E '10. International Conference on
Conference_Location :
Sanya
Print_ISBN :
978-1-4244-5680-2
Electronic_ISBN :
978-1-4244-5681-9
DOI :
10.1109/IC4E.2010.96
