|
JAIST Repository >
School of Information Science >
JAIST Research Reports >
Research Report - School of Information Science ： ISSN 0918-7553 >
IS-RR-2007 >
Please use this identifier to cite or link to this item:
https://hdl.handle.net/10119/8415
|
| Title: | Algebraic approaches to formal analysis of the mondex electronic purse system |
| Authors: | Kong, Weiqiang
Ogata, Kazuhiro
Futatsugi, Kokichi |
| Issue Date: | 2007-03-23 |
| Publisher: | 北陸先端科学技術大学院大学情報科学研究科 |
| Magazine name: | Research report (School of Information Science, Japan Advanced Institute of Science and Technology) |
| Volume: | IS-RR-2007-004 |
| Start page: | 1 |
| End page: | 43 |
| Abstract: | Mondex is a payment system that utilizes smart cards as electronic purses for financial transactions. The 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 with 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. |
| URI: | https://hdl.handle.net/10119/8415 |
| Material Type: | publisher |
| Appears in Collections: | IS-RR-2007
|
Files in This Item:
| File |
Description |
Size | Format |
|---|
| IS-RR-2007-004.pdf | | 2653Kb | Adobe PDF | View/Open |
|
All items in DSpace are protected by copyright, with all rights reserved.
|
