定理証明器による電子現金プロトコルの検証
スポンサーリンク
概要
- 論文の詳細を見る
本発表では,定理証明器Isabelle/HOLを用いて,電子現金プロトコルを帰納的にモデル化しその仕様を検証する方法を示す.電子現金方式に要求される仕様は一般に,「完全情報化」,「安全性」,「プライバシ」,「オフライン性」,「譲渡可能性」,「分割利用可能性」の6つであり,このすべての仕様を満たす電子現金方式が提案されている.我々は,この方式の1つを帰納的手法を用いてモデル化し,「安全性」,「分割利用可能性」の仕様が満たされることを検証した.対象とする方式では,電子現金はBinary Tree Approachにより実現されており,分割利用するための操作がこの二分木上で定義されている.また,ビットコミットメントを使うことで二重使用を防止している.これらの仕組みを取り込んだデータ構造や関数を帰納的に定義した.プロトコルのモデル化は,Paulsonの帰納的アプローチに基づき,送受信イベントをトレースとしてリストに格納する形ですべて帰納的に記述した.検証においては,モデル化に対応した仕様の解釈を行った.「安全性」は「誰かが二重使用を行った場合,必ず発覚する」と解釈し,「分割利用可能性」は「ある金額から任意の金額を使用した場合,残りの金額も正当な電子現金である」と解釈し,それぞれ検証した.この結果,定理証明器を電子現金プロトコルの検証に使える可能性を示すことができた.
- 一般社団法人情報処理学会の論文
- 2008-06-26
著者
関連論文
- 知識変更を伴う議論システム
- 鉄道信号システムの連動装置の形式的検証向けモデル化と検証環境構築(ソフトウェア基礎, プログラム理論)
- 車車間通信を用いた車線変更と脇道にともなう交通流の円滑化を図るモデルの提案と実装
- 帰納的アプローチに基づく理想的電子現金方式のモデル化および証明支援系Isabelle/HOLによる安全性の証明
- 電子現金の分割利用可能性の形式化と帰納的証明
- 車車間通信を用いた車線変更と脇道にともなう交通流の円滑化を図るモデルの提案と実装
- Symmetry Reductionを使ったAISの確率付きモデル検査
- 定性空間推論の新しい枠組DLCSとその上での操作
- 矩形領域に基づく定性空間推論の提案と実装
- 凹凸情報と接触パターンに基づく定性空間表現
- 定理証明器による電子現金プロトコルの検証
- 信念改竄によるばれない嘘の生成
- 輻輳問題を考慮したモバイルエージェントによるアドホックネットワークルーティング(モバイル・アドホックネットワーク(1))
- 定性空間表現の二次元平面への埋め込みについて
- 定性空間表現の二次元平面への埋め込みについて
- ボードゲームBAOにおける周期的動作の解析
- ボードゲームBAOにおける周期的動作の解析(数理モデル一般)
- ボードゲームBAOにおける周期的動作の解析
- ボードゲームBAOのCCSによる記述と解析
- 性質の伝播に関する定性空間推論
- モバイルエージェントを用いた動的ネットワークルーチングシステムの拡張
- 2. 広がるすきま : E. M. ForsterのHowards End, "Only connect..."からA Passage to India, "Perhaps!"へ(日本英文学会第73回大会報告)
- 空間に埋め込まれた意味情報の記述
- マルチエージェントの連鎖的交渉を用いたスケジュール作成と調整(スケジューリング,「Webインテリジェンス」及び一般)
- マルチエージェントの連鎖的交渉を用いたスケジュール作成と調整(スケジューリング,「Webインテリジェンス」及び一般)
- 動的議論システムの意味論的考察
- Symmetry Reduction を使ったAISの確率付きモデル検査
- 「情報処理学会論文誌 : プログラミング」の編集について
- 「情報処理学会論文誌 : プログラミング」の編集について
- 矩形同士の埋め込み型重ね合わせについての定性空間推論
- 定理証明器によって証明されたCプログラムのマージャ