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 proceedingConference contribution

1 Citation (Scopus)

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 languageEnglish
Title of host publicationProceedings - The Fourth International Conference on Computer and Information Technology (CIT 2004)
EditorsD. Wei, H. Wang, Z. Peng, A. Kara, Y. He
Pages1100-1107
Number of pages8
Publication statusPublished - 2004
Externally publishedYes
EventProceedings - The Fourth International Conference on Computer and Information Technology (CIT 2004) - Wuhan, China
Duration: Sep 14 2004Sep 16 2004

Other

OtherProceedings - The Fourth International Conference on Computer and Information Technology (CIT 2004)
CountryChina
CityWuhan
Period9/14/049/16/04

Fingerprint

Network protocols
Specification languages

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)

Formal analysis of an anonymous fair exchange e-commerce protocol. / Kong, Weiqiang; Ogata, Kazuhiro; Xiang, Jianwen; Futatsugi, Kokichi.

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.

Research output: Chapter in Book/Report/Conference proceedingConference 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). 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
Kong, Weiqiang ; Ogata, Kazuhiro ; Xiang, Jianwen ; Futatsugi, Kokichi. / 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
@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",
language = "English",
isbn = "0769522165",
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)",

}

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

Y1 - 2004

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

SN - 0769522165

SN - 9780769522166

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.

ER -