Algebraic approaches to formal analysis of the mondex electronic purse system

Weiqiang Kong; Kazuhiro Ogata; Kokichi Futatsugi

doi:10.1007/978-3-540-73210-5_21

Algebraic approaches to formal analysis of the mondex electronic purse system

Weiqiang Kong, Kazuhiro Ogata, Kokichi Futatsugi

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

15 Citations (Scopus)

Abstract

Mondex is a payment system that utilizes smart cards as electronic purses for financial transactions. This paper first reports on how the Mondex system can be modeled, specified and interactively verified using an equation-based method - the OTS/CafeOBJ method. Afterwards, the paper reports on, as a complementarity, a way of automatically falsifying the OTS/CafeOBJ specification of the Mondex system, and how the falsification can be used to facilitate the verification. Differently from related work, our work provides alternative ways of (1) modeling the Mondex system using an OTS (Observational Transition System), a kind of transition system, and (2) expressing and verifying (and falsifying) the desired security properties of the Mondex system directly in terms of invariants of the OTS.

Original language	English
Title of host publication	Integrated Formal Methods - 6th International Conference, IFM 2007, Proceedings
Publisher	Springer Verlag
Pages	393-412
Number of pages	20
ISBN (Print)	3540732098, 9783540732099
DOIs	https://doi.org/10.1007/978-3-540-73210-5_21
Publication status	Published - 2007
Event	6th International Conference on Integrated Formal Methods, IFM 2007 - Oxford, United Kingdom Duration: Jul 2 2007 → Jul 5 2007

Publication series

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

Other

Other	6th International Conference on Integrated Formal Methods, IFM 2007
Country/Territory	United Kingdom
City	Oxford
Period	7/2/07 → 7/5/07

All Science Journal Classification (ASJC) codes

Theoretical Computer Science
Computer Science(all)

Access to Document

10.1007/978-3-540-73210-5_21

Cite this

Kong, W., Ogata, K., & Futatsugi, K. (2007). Algebraic approaches to formal analysis of the mondex electronic purse system. In Integrated Formal Methods - 6th International Conference, IFM 2007, Proceedings (pp. 393-412). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4591 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-540-73210-5_21

Algebraic approaches to formal analysis of the mondex electronic purse system. / Kong, Weiqiang; Ogata, Kazuhiro; Futatsugi, Kokichi.
Integrated Formal Methods - 6th International Conference, IFM 2007, Proceedings. Springer Verlag, 2007. p. 393-412 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 4591 LNCS).

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

Kong, W, Ogata, K & Futatsugi, K 2007, Algebraic approaches to formal analysis of the mondex electronic purse system. in Integrated Formal Methods - 6th International Conference, IFM 2007, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 4591 LNCS, Springer Verlag, pp. 393-412, 6th International Conference on Integrated Formal Methods, IFM 2007, Oxford, United Kingdom, 7/2/07. https://doi.org/10.1007/978-3-540-73210-5_21

Kong W, Ogata K, Futatsugi K. Algebraic approaches to formal analysis of the mondex electronic purse system. In Integrated Formal Methods - 6th International Conference, IFM 2007, Proceedings. Springer Verlag. 2007. p. 393-412. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-540-73210-5_21

Kong, Weiqiang ; Ogata, Kazuhiro ; Futatsugi, Kokichi. / Algebraic approaches to formal analysis of the mondex electronic purse system. Integrated Formal Methods - 6th International Conference, IFM 2007, Proceedings. Springer Verlag, 2007. pp. 393-412 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{2b1e15f6b1084f59b0b0b8e03265fa4a,

title = "Algebraic approaches to formal analysis of the mondex electronic purse system",

abstract = "Mondex is a payment system that utilizes smart cards as electronic purses for financial transactions. This paper first reports on how the Mondex system can be modeled, specified and interactively verified using an equation-based method - the OTS/CafeOBJ method. Afterwards, the paper reports on, as a complementarity, a way of automatically falsifying the OTS/CafeOBJ specification of the Mondex system, and how the falsification can be used to facilitate the verification. Differently from related work, our work provides alternative ways of (1) modeling the Mondex system using an OTS (Observational Transition System), a kind of transition system, and (2) expressing and verifying (and falsifying) the desired security properties of the Mondex system directly in terms of invariants of the OTS.",

author = "Weiqiang Kong and Kazuhiro Ogata and Kokichi Futatsugi",

year = "2007",

doi = "10.1007/978-3-540-73210-5_21",

language = "English",

isbn = "3540732098",

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

publisher = "Springer Verlag",

pages = "393--412",

booktitle = "Integrated Formal Methods - 6th International Conference, IFM 2007, Proceedings",

address = "Germany",

note = "6th International Conference on Integrated Formal Methods, IFM 2007 ; Conference date: 02-07-2007 Through 05-07-2007",

}

TY - GEN

T1 - Algebraic approaches to formal analysis of the mondex electronic purse system

AU - Kong, Weiqiang

AU - Ogata, Kazuhiro

AU - Futatsugi, Kokichi

PY - 2007

Y1 - 2007

N2 - Mondex is a payment system that utilizes smart cards as electronic purses for financial transactions. This paper first reports on how the Mondex system can be modeled, specified and interactively verified using an equation-based method - the OTS/CafeOBJ method. Afterwards, the paper reports on, as a complementarity, a way of automatically falsifying the OTS/CafeOBJ specification of the Mondex system, and how the falsification can be used to facilitate the verification. Differently from related work, our work provides alternative ways of (1) modeling the Mondex system using an OTS (Observational Transition System), a kind of transition system, and (2) expressing and verifying (and falsifying) the desired security properties of the Mondex system directly in terms of invariants of the OTS.

AB - Mondex is a payment system that utilizes smart cards as electronic purses for financial transactions. This paper first reports on how the Mondex system can be modeled, specified and interactively verified using an equation-based method - the OTS/CafeOBJ method. Afterwards, the paper reports on, as a complementarity, a way of automatically falsifying the OTS/CafeOBJ specification of the Mondex system, and how the falsification can be used to facilitate the verification. Differently from related work, our work provides alternative ways of (1) modeling the Mondex system using an OTS (Observational Transition System), a kind of transition system, and (2) expressing and verifying (and falsifying) the desired security properties of the Mondex system directly in terms of invariants of the OTS.

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

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

U2 - 10.1007/978-3-540-73210-5_21

DO - 10.1007/978-3-540-73210-5_21

M3 - Conference contribution

AN - SCOPUS:37549063858

SN - 3540732098

SN - 9783540732099

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

SP - 393

EP - 412

BT - Integrated Formal Methods - 6th International Conference, IFM 2007, Proceedings

PB - Springer Verlag

T2 - 6th International Conference on Integrated Formal Methods, IFM 2007

Y2 - 2 July 2007 through 5 July 2007

ER -

Algebraic approaches to formal analysis of the mondex electronic purse system

Abstract

Publication series

Other

All Science Journal Classification (ASJC) codes

Access to Document

Other files and links

Fingerprint

Cite this