帰納的アプローチに基づく理想的電子現金方式のモデル化および証明支援系Isabelle/HOLによる安全性の証明

概要

論文の詳細を見る
本研究では,帰納的アプローチに基づいて理想的電子現金方式をモデル化し,その安全性について,証明支援系Isabelle/HOLを用いて証明を与える.理想的電子現金方式とは,「完全情報化」,「安全性」,「プライバシー」,「オフライン性」,「譲渡可能性」,「分割利用可能性」の6条件を満足する電子現金プロトコルである.この安全性は,「電子現金のコピー,偽造等による不正利用ができないこと」と定義されている.本研究の対象とするプロトコルは,電子現金のデータ構造として二分木を採用しており,支払いは金額に相当するノードを使うと定義される.また,同じ枝にあるノードを使用すると,額面以上の金額を使うという不正利用が生じるように設計されている.通常はユーザの購買に関するプライバシーを銀行を含む他者が把握することはできないが,不正利用が発覚した際に,使用されたノードの情報から不正利用者を割り出すことができる仕掛けになっており,これによって安全性を保証している.プロトコルのモデル化には,Paulsonらの提案した帰納的アプローチを用いる.しかし,彼らの構築したモデルは金額を扱ったものではない.一方,このプロトコルにおける安全性を扱うには,二分木上のノードの位置情報と電子現金の金額の考慮が不可欠である.そのため,本研究ではこれらを量的なデータとしてモデルに与え,証明を試みる.
2010-09-22

帰納的アプローチに基づく理想的電子現金方式のモデル化および証明支援系Isabelle/HOLによる安全性の証明

スポンサーリンク

概要

著者

関連論文

スポンサーリンク