電子現金の分割利用可能性の形式化と帰納的証明

概要

論文の詳細を見る
本研究では,二分木構造を持つ電子現金について帰納的なモデルを与え,定理証明器Isabelle/HOLを用いて仕様の検証を行った.電子現金方式のうち,「完全情報化」,「安全性」,「プライバシ」,「オフライン性」,「譲渡可能性」,「分割利用可能性」の6条件を満足するものを「理想的電子現金方式」と呼ぶ.ここでは,理想的電子現金方式として提案されている一方式を形式化し,分割利用可能性についての検証を試みた.分割利用可能性とは,1度発行された電子現金を,利用合計金額が額面の金額になるまで何度でも使うことができる,という性質である.本研究で扱う方式では,電子現金を二分木によって構成し,二分木上の操作を定義することにより,これを実現している.モデル化の際も同様に,二分木に基づくデータ構造や関数を帰納的に定義した.また,分割利用可能性については「ある電子現金から任意の金額を支払った結果,残りの電子現金の金額はその差額に等しい」と解釈し,これを証明した.なお,自然数と二分木という異なる帰納スキームを持つデータ間の対応関係を帰納法を使って証明するために,中間的なデータ構造として二進法を利用した.そのため,本発表ではIsabelle/HOLでの二進数の扱い方についても言及する.
2009-11-20

電子現金の分割利用可能性の形式化と帰納的証明

スポンサーリンク

概要

著者

関連論文

スポンサーリンク