Formal analysis of an anonymous fair exchange e-commerce protocol

Weiqiang Kong; Kazuhiro Ogata; Jianwen Xiang; Kokichi Futatsugi

Formal analysis of an anonymous fair exchange e-commerce protocol

Weiqiang Kong, Kazuhiro Ogata, Jianwen Xiang, Kokichi Futatsugi

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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.

Original language	English
Title of host publication	Proceedings - The Fourth International Conference on Computer and Information Technology (CIT 2004)
Editors	D. Wei, H. Wang, Z. Peng, A. Kara, Y. He
Pages	1100-1107
Number of pages	8
Publication status	Published - Dec 14 2004
Event	Proceedings - The Fourth International Conference on Computer and Information Technology (CIT 2004) - Wuhan, China Duration: Sept 14 2004 → Sept 16 2004

Publication series

Name	Proceedings - The Fourth International Conference on Computer and Information Technology (CIT 2004)

Other

Other	Proceedings - The Fourth International Conference on Computer and Information Technology (CIT 2004)
Country/Territory	China
City	Wuhan
Period	9/14/04 → 9/16/04

All Science Journal Classification (ASJC) codes

Engineering(all)

Cite this

Kong, W., Ogata, K., Xiang, J., & Futatsugi, K. (2004). Formal analysis of an anonymous fair exchange e-commerce protocol. In D. Wei, H. Wang, Z. Peng, A. Kara, & Y. He (Eds.), Proceedings - The Fourth International Conference on Computer and Information Technology (CIT 2004) (pp. 1100-1107). (Proceedings - The Fourth International Conference on Computer and Information Technology (CIT 2004)).

Formal analysis of an anonymous fair exchange e-commerce protocol. / Kong, Weiqiang; Ogata, Kazuhiro; Xiang, Jianwen et al.
Proceedings - The Fourth International Conference on Computer and Information Technology (CIT 2004). ed. / D. Wei; H. Wang; Z. Peng; A. Kara; Y. He. 2004. p. 1100-1107 (Proceedings - The Fourth International Conference on Computer and Information Technology (CIT 2004)).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Kong, W, Ogata, K, Xiang, J & Futatsugi, K 2004, Formal analysis of an anonymous fair exchange e-commerce protocol. in D Wei, H Wang, Z Peng, A Kara & Y He (eds), Proceedings - The Fourth International Conference on Computer and Information Technology (CIT 2004). Proceedings - The Fourth International Conference on Computer and Information Technology (CIT 2004), pp. 1100-1107, Proceedings - The Fourth International Conference on Computer and Information Technology (CIT 2004), Wuhan, China, 9/14/04.

Kong W, Ogata K, Xiang J, Futatsugi K. Formal analysis of an anonymous fair exchange e-commerce protocol. In Wei D, Wang H, Peng Z, Kara A, He Y, editors, Proceedings - The Fourth International Conference on Computer and Information Technology (CIT 2004). 2004. p. 1100-1107. (Proceedings - The Fourth International Conference on Computer and Information Technology (CIT 2004)).

Kong, Weiqiang ; Ogata, Kazuhiro ; Xiang, Jianwen et al. / Formal analysis of an anonymous fair exchange e-commerce protocol. Proceedings - The Fourth International Conference on Computer and Information Technology (CIT 2004). editor / D. Wei ; H. Wang ; Z. Peng ; A. Kara ; Y. He. 2004. pp. 1100-1107 (Proceedings - The Fourth International Conference on Computer and Information Technology (CIT 2004)).

@inproceedings{7d86c6a4809c4d12b3b5972e8c8205f6,

title = "Formal analysis of an anonymous fair exchange e-commerce protocol",

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.",

author = "Weiqiang Kong and Kazuhiro Ogata and Jianwen Xiang and Kokichi Futatsugi",

year = "2004",

month = dec,

day = "14",

language = "English",

isbn = "0769522165",

series = "Proceedings - The Fourth International Conference on Computer and Information Technology (CIT 2004)",

pages = "1100--1107",

editor = "D. Wei and H. Wang and Z. Peng and A. Kara and Y. He",

booktitle = "Proceedings - The Fourth International Conference on Computer and Information Technology (CIT 2004)",

note = "Proceedings - The Fourth International Conference on Computer and Information Technology (CIT 2004) ; Conference date: 14-09-2004 Through 16-09-2004",

}

TY - GEN

T1 - Formal analysis of an anonymous fair exchange e-commerce protocol

AU - Kong, Weiqiang

AU - Ogata, Kazuhiro

AU - Xiang, Jianwen

AU - Futatsugi, Kokichi

PY - 2004/12/14

Y1 - 2004/12/14

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=9744281264&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=9744281264&partnerID=8YFLogxK

M3 - Conference contribution

AN - SCOPUS:9744281264

SN - 0769522165

SN - 9780769522166

T3 - Proceedings - The Fourth International Conference on Computer and Information Technology (CIT 2004)

SP - 1100

EP - 1107

BT - Proceedings - The Fourth International Conference on Computer and Information Technology (CIT 2004)

A2 - Wei, D.

A2 - Wang, H.

A2 - Peng, Z.

A2 - Kara, A.

A2 - He, Y.

T2 - Proceedings - The Fourth International Conference on Computer and Information Technology (CIT 2004)

Y2 - 14 September 2004 through 16 September 2004

ER -

Formal analysis of an anonymous fair exchange e-commerce protocol

Abstract

Publication series

Other

All Science Journal Classification (ASJC) codes

Other files and links

Fingerprint

Cite this