Formal analysis of an anonymous fair exchange e-commerce protocol

Weiqiang Kong, Kazuhiro Ogata, Jianwen Xiang, Kokichi Futatsugi

研究成果: 著書/レポートタイプへの貢献会議での発言

1 引用 (Scopus)

抄録

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
出版物ステータス出版済み - 2004
外部発表Yes
イベントProceedings - The Fourth International Conference on Computer and Information Technology (CIT 2004) - Wuhan, 中国
継続期間: 9 14 20049 16 2004

その他

その他Proceedings - The Fourth International Conference on Computer and Information Technology (CIT 2004)
中国
Wuhan
期間9/14/049/16/04

Fingerprint

Network protocols
Specification languages

All Science Journal Classification (ASJC) codes

  • Engineering(all)

これを引用

Kong, W., Ogata, K., Xiang, J., & Futatsugi, K. (2004). Formal analysis of an anonymous fair exchange e-commerce protocol. : D. Wei, H. Wang, Z. Peng, A. Kara, & Y. He (版), 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). 版 / D. Wei; H. Wang; Z. Peng; A. Kara; Y. He. 2004. p. 1100-1107.

研究成果: 著書/レポートタイプへの貢献会議での発言

Kong, W, Ogata, K, Xiang, J & Futatsugi, K 2004, Formal analysis of an anonymous fair exchange e-commerce protocol. : D Wei, H Wang, Z Peng, A Kara & Y He (版), 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. : Wei D, Wang H, Peng Z, Kara A, He Y, 編集者, 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). 編集者 / 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 -