Model-based analysis of money accountability in electronic purses

Il Gon Kim; Young Joo Moon; Inhye Kang; Ji Yeon Lee; Keun Hee Han; Jin Young Choi

doi:10.1007/11600930_34

Model-based analysis of money accountability in electronic purses

Il Gon Kim, Young Joo Moon, Inhye Kang, Ji Yeon Lee, Keun Hee Han, Jin Young Choi

School of Cybersecurity

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

Abstract

The Common Electronic Purse Specifications (CEPS) define requirements for all components needed by an organization to implement a globally interoperable electronic purse program. In this paper we describe how we model purchase transaction protcol in CEPS using formal specification language. We define and verify the money accountability property of the CEPS, and we address its violation scenario in the presence of communication network failures. Using model checking technique we find that transaction record stored in the trusted-third party plays a essential role in satisfying the accountability property.

Original language	English
Title of host publication	Internet and Network Economics - First International Workshop, WINE 2005, Proceedings
Publisher	Springer Verlag
Pages	346-355
Number of pages	10
ISBN (Print)	3540309004, 9783540309000
DOIs	https://doi.org/10.1007/11600930_34
Publication status	Published - 2005
Event	1st International Workshop on Internet and Network Economics, WINE 2005 - Hong Kong, China Duration: 2005 Dec 15 → 2005 Dec 17

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	3828 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Other

Other	1st International Workshop on Internet and Network Economics, WINE 2005
Country/Territory	China
City	Hong Kong
Period	05/12/15 → 05/12/17

Keywords

CEPS
Casper
E-commerce protocol
FDR
Formal specification and verification
Model checking
Money accountability
Security

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Access to Document

10.1007/11600930_34

Cite this

Kim, I. G., Moon, Y. J., Kang, I., Lee, J. Y., Han, K. H., & Choi, J. Y. (2005). Model-based analysis of money accountability in electronic purses. In Internet and Network Economics - First International Workshop, WINE 2005, Proceedings (pp. 346-355). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 3828 LNCS). Springer Verlag. https://doi.org/10.1007/11600930_34

Model-based analysis of money accountability in electronic purses. / Kim, Il Gon; Moon, Young Joo; Kang, Inhye et al.

Internet and Network Economics - First International Workshop, WINE 2005, Proceedings. Springer Verlag, 2005. p. 346-355 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 3828 LNCS).

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

Kim, IG, Moon, YJ, Kang, I, Lee, JY, Han, KH & Choi, JY 2005, Model-based analysis of money accountability in electronic purses. in Internet and Network Economics - First International Workshop, WINE 2005, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 3828 LNCS, Springer Verlag, pp. 346-355, 1st International Workshop on Internet and Network Economics, WINE 2005, Hong Kong, China, 05/12/15. https://doi.org/10.1007/11600930_34

Kim IG, Moon YJ, Kang I, Lee JY, Han KH, Choi JY. Model-based analysis of money accountability in electronic purses. In Internet and Network Economics - First International Workshop, WINE 2005, Proceedings. Springer Verlag. 2005. p. 346-355. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/11600930_34

Kim, Il Gon ; Moon, Young Joo ; Kang, Inhye et al. / Model-based analysis of money accountability in electronic purses. Internet and Network Economics - First International Workshop, WINE 2005, Proceedings. Springer Verlag, 2005. pp. 346-355 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{d40fd051932542179bdcaffa3a8d7934,

title = "Model-based analysis of money accountability in electronic purses",

abstract = "The Common Electronic Purse Specifications (CEPS) define requirements for all components needed by an organization to implement a globally interoperable electronic purse program. In this paper we describe how we model purchase transaction protcol in CEPS using formal specification language. We define and verify the money accountability property of the CEPS, and we address its violation scenario in the presence of communication network failures. Using model checking technique we find that transaction record stored in the trusted-third party plays a essential role in satisfying the accountability property.",

keywords = "CEPS, Casper, E-commerce protocol, FDR, Formal specification and verification, Model checking, Money accountability, Security",

author = "Kim, {Il Gon} and Moon, {Young Joo} and Inhye Kang and Lee, {Ji Yeon} and Han, {Keun Hee} and Choi, {Jin Young}",

year = "2005",

doi = "10.1007/11600930_34",

language = "English",

isbn = "3540309004",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "346--355",

booktitle = "Internet and Network Economics - First International Workshop, WINE 2005, Proceedings",

}

TY - GEN

T1 - Model-based analysis of money accountability in electronic purses

AU - Kim, Il Gon

AU - Moon, Young Joo

AU - Kang, Inhye

AU - Lee, Ji Yeon

AU - Han, Keun Hee

AU - Choi, Jin Young

PY - 2005

Y1 - 2005

N2 - The Common Electronic Purse Specifications (CEPS) define requirements for all components needed by an organization to implement a globally interoperable electronic purse program. In this paper we describe how we model purchase transaction protcol in CEPS using formal specification language. We define and verify the money accountability property of the CEPS, and we address its violation scenario in the presence of communication network failures. Using model checking technique we find that transaction record stored in the trusted-third party plays a essential role in satisfying the accountability property.

AB - The Common Electronic Purse Specifications (CEPS) define requirements for all components needed by an organization to implement a globally interoperable electronic purse program. In this paper we describe how we model purchase transaction protcol in CEPS using formal specification language. We define and verify the money accountability property of the CEPS, and we address its violation scenario in the presence of communication network failures. Using model checking technique we find that transaction record stored in the trusted-third party plays a essential role in satisfying the accountability property.

KW - CEPS

KW - Casper

KW - E-commerce protocol

KW - FDR

KW - Formal specification and verification

KW - Model checking

KW - Money accountability

KW - Security

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

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

U2 - 10.1007/11600930_34

DO - 10.1007/11600930_34

M3 - Conference contribution

AN - SCOPUS:33744935256

SN - 3540309004

SN - 9783540309000

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 346

EP - 355

BT - Internet and Network Economics - First International Workshop, WINE 2005, Proceedings

PB - Springer Verlag

T2 - 1st International Workshop on Internet and Network Economics, WINE 2005

Y2 - 15 December 2005 through 17 December 2005

ER -

Model-based analysis of money accountability in electronic purses

Abstract

Publication series

Other

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this