Algebraic approaches to formal analysis of the mondex electronic purse system

Weiqiang Kong, Kazuhiro Ogata, Kokichi Futatsugi

Research output: Chapter in Book/Report/Conference proceedingConference contribution

11 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 languageEnglish
Title of host publicationIntegrated Formal Methods - 6th International Conference, IFM 2007, Proceedings
PublisherSpringer Verlag
Pages393-412
Number of pages20
ISBN (Print)3540732098, 9783540732099
DOIs
Publication statusPublished - 2007
Event6th International Conference on Integrated Formal Methods, IFM 2007 - Oxford, United Kingdom
Duration: Jul 2 2007Jul 5 2007

Publication series

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

Other

Other6th International Conference on Integrated Formal Methods, IFM 2007
CountryUnited Kingdom
CityOxford
Period7/2/077/5/07

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Algebraic approaches to formal analysis of the mondex electronic purse system'. Together they form a unique fingerprint.

  • 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