loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Fourth International Conference on Computer and Information Technology (CIT'04)
Formal Analysis of an Anonymous Fair Exchange E-Commerce Protocol
Wuhan, China
September 14-September 16
ISBN: 0-7695-2216-5
ASCII Text
x 
 
Weiqiang Kong, Kazuhiro Ogata, Jianwen Xiang, Kokichi Futatsugi, "Formal Analysis of an Anonymous Fair Exchange E-Commerce Protocol," Computer and Information Technology, International Conference on, pp. 1100-1107, Fourth International Conference on Computer and Information Technology (CIT'04), 2004.
 
 
BibTex
x
 
@article{ 10.1109/CIT.2004.1357342,
author = {Weiqiang Kong and Kazuhiro Ogata and Jianwen Xiang and Kokichi Futatsugi},
title = {Formal Analysis of an Anonymous Fair Exchange E-Commerce Protocol},
journal ={Computer and Information Technology, International Conference on},
volume = {0},
year = {2004},
isbn = {0-7695-2216-5},
pages = {1100-1107},
doi = {http://doi.ieeecomputersociety.org/10.1109/CIT.2004.1357342},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Computer and Information Technology, International Conference on
TI - Formal Analysis of an Anonymous Fair Exchange E-Commerce Protocol
SN - 0-7695-2216-5
SP1100
EP1107
A1 - Weiqiang Kong,
A1 - Kazuhiro Ogata,
A1 - Jianwen Xiang,
A1 - Kokichi Futatsugi,
PY - 2004
KW - null
VL - 0
JA - Computer and Information Technology, International Conference on
ER -
 
Weiqiang Kong, Japan Advanced Institute of Science and Technology
Kazuhiro Ogata, Japan Advanced Institute of Science and Technology and NEC Software Hokuriku, Ltd.
Jianwen Xiang, Japan Advanced Institute of Science and Technology
Kokichi Futatsugi, Japan Advanced Institute of Science and Technology
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.
Citation:
Weiqiang Kong, Kazuhiro Ogata, Jianwen Xiang, Kokichi Futatsugi, "Formal Analysis of an Anonymous Fair Exchange E-Commerce Protocol," cit, pp.1100-1107, Fourth International Conference on Computer and Information Technology (CIT'04), 2004
Usage of this product signifies your acceptance of the Terms of Use.