Analyzing a Fair Exchange E-commerce Protocol Using CSP and FDR

Author

Wang, Zhangkai

Author_Institution

Dept. of Comput. Sci. Eng., Shanghai Jiao Tong Univ., Shanghai, China

fYear

2010

fDate

22-24 Jan. 2010

Firstpage

303

Lastpage

307

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;

fLanguage

English

Publisher

ieee

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

Type

conf

DOI

10.1109/IC4E.2010.96

Filename

5432444