Formal analysis of an anonymous fair exchange e-commerce protocol

Author

Kong, Weiqiang ; Ogata, Kazuhiro ; Xiang, Jianwen ; Futatsugi, Kokichi

Author_Institution

Japan Adv. Inst. of Sci. & Technol., Japan

fYear

2004

fDate

14-16 Sept. 2004

Firstpage

1100

Lastpage

1107

Abstract

Fair exchange and anonymity are important requirements of e-commerce protocols. We have formally analyzed an e-commerce protocol, which is claimed to satisfy the two requirements. The protocol, together with the intruder, has been modeled as an OTS, a kind of transition system. Then the OTS has been written in CafeOBJ, an algebraic specification language. Although most part of the two requirements can be expressed as safety properties, liveness properties are needed to fully express them. We have expressed the safety part of the two requirements in CafeOBJ and partly verified that the OTS satisfies the safety part by writing proof scores in CafeOBJ.

Keywords

algebraic specification; electronic commerce; electronic data interchange; formal verification; protocols; specification languages; CafeOBJ; OTS; algebraic specification language; anonymous fair exchange e-commerce protocol; formal analysis; liveness properties; proof scores; safety properties; transition system; Business; Equations; Protocols; Safety; Security; Specification languages; State-space methods; Writing;

fLanguage

English

Publisher

ieee

Conference_Titel

Computer and Information Technology, 2004. CIT '04. The Fourth International Conference on

Print_ISBN

0-7695-2216-5

Type

conf

DOI

10.1109/CIT.2004.1357342

Filename

1357342