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

研究成果: 書籍/レポートタイプへの寄稿 › 会議への寄与

抄録

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.

本文言語	英語
ホスト出版物のタイトル	Proceedings - The Fourth International Conference on Computer and Information Technology (CIT 2004)
編集者	D. Wei, H. Wang, Z. Peng, A. Kara, Y. He
ページ	1100-1107
ページ数	8
出版ステータス	出版済み - 12月 14 2004
イベント	Proceedings - The Fourth International Conference on Computer and Information Technology (CIT 2004) - Wuhan, 中国継続期間: 9月 14 2004 → 9月 16 2004

出版物シリーズ

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

その他

その他	Proceedings - The Fourth International Conference on Computer and Information Technology (CIT 2004)
国/地域	中国
City	Wuhan
Period	9/14/04 → 9/16/04

!!!All Science Journal Classification (ASJC) codes

工学（全般）

他のファイルとリンク

引用スタイル

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 その他.
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)).

研究成果: 書籍/レポートタイプへの寄稿 › 会議への寄与

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, 中国, 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 その他. / 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

抄録

出版物シリーズ

その他

!!!All Science Journal Classification (ASJC) codes

他のファイルとリンク

フィンガープリント

引用スタイル