SET支払いプロトコルの秘匿性検証(セキュリティプロトコル・電子公証)(<特集>新たな脅威に立ち向かうコンピュータセキュリティ技術)
スポンサーリンク
概要
- 論文の詳細を見る
セキュリティ・プロトコルの安全性を証明によって検証する論理的検証は,プロトコル仕様記述の柔軟性と検証の完全性の点で優れている.特にPaulsonによる帰納的方法は,実際に使用されているプロトコルの検証の実績があり,証明スクリプトも公開されている.しかしこの方法では大きなプロトコル仕様記述が繁雑になりやすいという欠点があった.本論文ではプロトコル仕様を簡潔に記述する言語と,この言語で記述したプロトコル仕様を帰納的方法の論理式に変換する方法を提案する.これにより大きなプロトコルを検証する際にも帰納的方法の証明スクリプトの多くをそのまま利用でき,検証を効率的に行うことができる.本論文ではさらに,これをSET(Secure Electronic Transaction)の支払いプロトコルの検証に適用し,カード番号の秘匿性を検証することができた.その際,検証を現実的な時間内で可能にするために,検証を目指すセキュリティから参照されない部分を省略して簡略化されたプロトコル仕様を得た.
- 一般社団法人情報処理学会の論文
- 2003-08-15
著者
関連論文
- モデル検査を用いたタグVLANの設定検査(ネットワークサービス基礎)
- タグスイッチネットワークのモデル検査による漏曳検査(セッション3)
- SET支払いプロトコルの秘匿性検証(セキュリティプロトコル・電子公証)(新たな脅威に立ち向かうコンピュータセキュリティ技術)
- ゲーム列による安全性証明の形式化と自動化(数理的技法による情報セキュリティ)
- 関数部分知識と匿名性検証(理論,数理的技法による情報セキュリティ,平成19年研究部会連合発表会)
- 攻撃者を考慮した匿名性検証法 (第20回 回路とシステム軽井沢ワークショップ論文集) -- (形式的手法)
- プロセス代数を用いたセキュリティ・プロトコル記述
- 文脈計算の環境計算による解釈
- 電子投票プロトコルに対する無証拠性の定理証明
- フォーマルメソッドによるセキュリティ&プライバシ (特集 20周年を迎えたコミュニケーション科学)
- 電子投票プロトコルに対する無証拠性の定理証明 (特集 人と共存するコンピュータセキュリティ技術)