定理証明器による電子現金プロトコルの検証

• Item type: Trans(1)
• 公開日: 2008-06-26
• タイトル: 定理証明器による電子現金プロトコルの検証
• タイトル / 言語: en
• タイトル: Verification of Electronic Cash Protocol Using a Theorem Prover
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: 発表概要
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: 関西学院大学
• 著者所属: 関西学院大学
• 著者所属(英): en
• 著者所属(英): Kwansei Gakuin University
• 著者所属(英): en
• 著者所属(英): Kwansei Gakuin University
• 著者名: 安田, 武史; 高橋, 和子
• 著者名(英): Takeshi, Yasuda; Kazuko, Takahashi
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 本発表では，定理証明器Isabelle/HOLを用いて，電子現金プロトコルを帰納的にモデル化しその仕様を検証する方法を示す．電子現金方式に要求される仕様は一般に，「完全情報化」，「安全性」，「プライバシ」，「オフライン性」，「譲渡可能性」，「分割利用可能性」の6つであり，このすべての仕様を満たす電子現金方式が提案されている．我々は，この方式の1つを帰納的手法を用いてモデル化し，「安全性」，「分割利用可能性」の仕様が満たされることを検証した．対象とする方式では，電子現金はBinary Tree Approachにより実現されており，分割利用するための操作がこの二分木上で定義されている．また，ビットコミットメントを使うことで二重使用を防止している．これらの仕組みを取り込んだデータ構造や関数を帰納的に定義した．プロトコルのモデル化は，Paulsonの帰納的アプローチに基づき，送受信イベントをトレースとしてリストに格納する形ですべて帰納的に記述した．検証においては，モデル化に対応した仕様の解釈を行った．「安全性」は「誰かが二重使用を行った場合，必ず発覚する」と解釈し，「分割利用可能性」は「ある金額から任意の金額を使用した場合，残りの金額も正当な電子現金である」と解釈し，それぞれ検証した．この結果，定理証明器を電子現金プロトコルの検証に使える可能性を示すことができた．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: We show inductive modeling of an electronic cash protocol and verification that its requirements are satisfied using a theoreom prover Isabelle/HOL. It is said that an electronic cash should satisfy the following six requirements: independance, security, privacy, off-line, transferability and divisability. An electronic cash scheme that satisfies all of them has been proposed. We formalize the protocol based on this scheme. The scheme is implemented using a binary tree on which the operation for divisable use is defined. Moreover, doublespending is detected by the bit-commitment. We define the data structure and recursive functions that reflect these mechanism. In modeling a protocol, we use Paulson's inductive approach, in which each event of sending/receiving is stored as a trace. We verified the security and divisability of the six requirements. As for security, we verify the assertion that if double-spending of an electronic cash occurs, then it can be detected. As for divisability, we verify the assertion that if we use some portion of a well-defined electronic cash, then the remainder is also a well-defined one. As a result, we showed the possibility that thereom provers can be applied to verification on electronic cash protocols.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AA11464814
• 書誌情報: 情報処理学会論文誌プログラミング（PRO）; 巻 1, 号 1, p. 60-60, 発行日 2008-06-26
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7802
• 出版者 / 言語: ja
• 出版者: 情報処理学会