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