| 研究概要 |
本研究では,暗号プロトコルにとって望ましい強さの計算量的安全性を保証するUC安全性を形式的に検証するための基盤技術と,検証システムの開発を目的とする.本年度は具体的には以下の研究を行った.
1.記号論的モデルと計算論的に健全な検証法の拡張
UC安全性のモデルのうち,昨年度定式化したGUCモデルの等価な簡易版であるEUCモデルを対象とし,記号論的モデルを定義した.EUCモデルは,GUCモデルと同様にPKI環境下の強固な安全性を保証しつつ、各種概念が簡明となっている.それらの概念を記号論的に対応する形で定義した.さらに,インターネットにおいて必須となる鍵交換プロトコルと認証プロトコルの安全性判定問題が決定可能となるための十分条件を導出し,その十分条件下で計算論的に健全な検証法を設計した.
2.再設計支援に有用となる攻撃の検討と攻撃導出法の設計
暗号プロトコルの計算量的安全性の根拠として,様々な数学問題の困難性が仮定されている,安全性を保証するためには,基となる数学的構造を理想化したGeneric model(GM)において困難性仮定に対する攻撃の有無を判定する必要がある.そこで,GMにおける攻撃の有無判定・導出法を設計した.
3.検証技術の主要部分の試作
攻撃有無判定・導出法を数式処理システムMapleにより実装した,さらに,暗号分野における代表的な論文アーカイブであるCryptology ePrint Archive へ最近1年間に投稿された論文(713本)で言及された困難性仮定に適用し,攻撃の有無を確認した.これにより,査読による検証が行われていない ePrint上の困難性仮定の信頼性向上に寄与した.
|
