概要
本研究では，理想的電子現金方式をモデル化し，その性質について証明支援系
Isabelle/HOL を用いた検証を行った．理想的電子現金方式とは，「完全情報化」
「安全性」「プライバシー」「オフライン性」「譲渡可能性」「分割利用可能性」
の 6 条件を満足する電子現金プロトコルである．ここでは，プロトコルレベル
とデータ構造レベルに分けてモデル化を行い，安全性と分割利用可能性について
の検証を行った．

プロトコルレベルでは，Isabelle/HOL においてプロトコルの安全性証明に広く
用いられる帰納的アプローチを利用した．電子現金プロトコルの安全性には，支
払い金額などの量的な情報が絡んでおり，モデル化の際にはそれらを具体的な
データとして与える必要がある．本研究では，具体的なデータを含んだモデルに
ついて，帰納的アプローチの適用を試みることにより，このアプローチの限界を
示唆する結果を得た．

一方データ構造レベルでは，自然数と二分木という異なる帰納構造に対し，帰納
的な変換と，両者の間の性質についての帰納的な証明を与えた．ここでは中間
データとして二進数を利用したが，一般に異なる帰納スキームにまたがる性質を
扱う際にも，問題の性質に適した中間データを用意することによって，証明を帰
納的推論によって導ける可能性を示すことができた．

これらの結果により，Isabelle/HOL の応用範囲の拡大への貢献が期待できる．

発表論文
 
``Formalization of Data Conversion for Inductive Proof,''
Tunisia-Japan Workshop on Symbolic Computation in Software Science (SCSS 2009),
pp.135-150, September, 2009.

``電子現金の分割利用可能性の形式化と帰納的証明,''
情報処理学会第74回プログラミング研究会発表資料, June, 2009.

``異なる帰納スキームにまたがる性質の定理証明手法,''
日本ソフトウェア科学会第26回大会, September, 2009.

``帰納的アプローチに基づく理想的電子現金方式のモデル化および証明支援系 Isabelle/HOL による安全性の証明,''
情報処理学会第78回プログラミング研究会発表資料, March, 2010.