Algebraic approaches to formal analysis of the mondex electronic purse system

• 資料種別: 文書・図像類
• タイトル: Algebraic approaches to formal analysis of the mondex electronic purse system
• 著者・編者: Kong, Weiqiang; Ogata, Kazuhiro; Futatsugi, Kokichi
• 著者標目: Kong, Weiqiang; Ogata, Kazuhiro; Futatsugi, Kokichi
• 出版事項: 北陸先端科学技術大学院大学情報科学研究科
• 出版年月日等: 2007-03-23
• 出版年（W3CDTF）: 2007-03-23
• タイトル（掲載誌）: Research report (School of Information Science, Japan Advanced Institute of Science and Technology)
• 巻号年月日等（掲載誌）: IS-RR-2007-004
• 掲載巻: IS-RR-2007-004
• 掲載ページ: 1-43
• ISSN（掲載誌）: ISSN : 0918-7553
• 本文の言語コード: eng
• 対象利用者: 一般
• 一般注記: 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.; リサーチレポート（北陸先端科学技術大学院大学情報科学研究科）; identifier:https://dspace.jaist.ac.jp/dspace/handle/10119/8415
• 記録形式（IMT）: application/pdf
• 一次資料へのリンクURL: https://dspace.jaist.ac.jp/dspace/bitstream/10119/8415/1/IS-RR-2007-004.pdf
• オンライン閲覧公開範囲: 限定公開
• 連携機関・データベース: 国立情報学研究所 : 学術機関リポジトリデータベース（IRDB）（機関リポジトリ）; https://irdb.nii.ac.jp
• 提供元機関・データベース: 北陸先端科学技術大学院大学 : JAIST学術研究成果リポジトリ