| 研究概要 |
本研究では,暗号プロトコルの最も望ましい強さの計算量的安全性であるUC安全性を形式的に検証するための基盤技術と,検証システムの開発を目的とする.
本年度は具体的には以下の研究を行った.
1. UC安全に対する新たな記号論的モデルの定義
UC安全性のモデルのうち,多くの暗号プロトコルの機能の定式化に利用されている最初に提案されたUCモデルと最も拡張されたGUCモデルを対象とし,それぞれに対する記号論的モデルを定義した.その特徴は,UC/GUCモデルにおける各種概念を記号論的に対応する形で定義したことである.これによって,暗号プロプロトコルとUC安全性の記号論的定義が直観的となる.
2. 定義した記号論的モデルに基づく検証法の設計と計算論的健全性の証明
検証法では,まず検証対象プロトコルとその計算論的安全性を記号的記述に変換する必要がある.従来の検証対象に加えて,新たな種類のプロトコルとその計算論的安全性を記号的記述に変換する手法を提案した.これによって,多くのプロトコルの基となる非常に重要なプロトコル(コミットメントプロトコル)も検証できるようになった.さらに,記号論的安全性が健全となるための十分条件を示した.これによって,検証における最初の処理の自動化方針が定まった.本結果は検証における手間の大幅な削減に繋がる.
3. 検証技術の主要部の試作
検証では,記号的記述への変換後,記号的プロトコルが記号的安全性を満たすか否かを判定する.その判定で繰り返し実行される部分処理を試作し,代表的な検証例に対して実行時間を計測した.その結果,数分以内で判定が終了することが分かり,十分実用的であることを確認できた.
|
