概要
本研究では，定理証明器 Isabelle/HOL を用いて，電子現金プロトコルを帰納的
にモデル化し，その仕様を検証した．

電子現金方式に要求される仕様は，「完全情報化」，「安全性」，「プライバ
シー」，「オフライン性」，「譲渡可能性」，「分割利用可能性」の6条件であ
り，このすべての仕様を満たす電子現金方式が提案されている．この方式の１つ
を帰納的手法によってモデル化し，「安全性」，「分割利用可能性」の仕様が満
たされていることを検証した．

対象とする方式では，電子現金はBinary Tree Approach により実現されており，
分割利用するための操作がこの二分木上で定義されている．また，ビットコミッ
トメントを使うことで二重使用を防止している．これらの仕組みを取り込んだデー
タ構造や関数を帰納的に定義した．プロトコルのモデル化は，Paulson の帰納的
アプローチに基づき，送受信イベントのトレースとして，リストに格納する形で
すべて帰納的に記述した．検証においては，モデル化に対応した仕様の解釈を行っ
た．「安全性」は「誰かが二重使用を行った場合，必ず発覚する」と解釈し，
「分割利用可能性」は「ある金額から任意の金額を使用した場合，残りの金額も
正当な電子現金である」と解釈し，それぞれ検証した．

この結果，定理証明器を電子現金プロトコルの検証に使える可能性を示すことが
できた．(Isabelle/HOL によるモデル化と検証結果)

発表論文
"定理証明を用いたWide Mouth Frog Protocolの検証"
日本ソフトウェア科学会第23回大会, September, 2006.

"帰納的アプローチを用いた時間感知型暗号プロトコルの検証"
第3回システム検証の科学技術シンポジウム，pp.67--73, October, 2006.

"定理証明器による電子現金プロトコルの検証," 
情報処理学会第67回プログラミング研究会発表資料, January, 2008.