形式記述による暗号プロトコルの自動検証の研究

点击翻译按钮获取中文摘要

研究計画の第1段階として挙げた新規プリミティブに対するより強い攻撃者のTask-PIOAフレームワークを用いた定式化を達成した.新規プリミティブとして「電子署名」,より強い攻撃者として「能動的攻撃者」の定式化を試みた.具体的には,適応的選択文書攻撃者に対するFDH署名の存在的偽造不可能性をTask-PIOAフレームワークを用いて証明することに成功した.上記の攻撃者モデルは電子署名における最も強力な能動的攻撃者とされているものであり,今回の成果によってTask-PIOAフレームワークでも実用的な安全性検証が可能であることが明らかになった.また,その過程において,落とし戸付き関数の計算量的一方向性のTask-PIOAでの表現法を提案した.Task-PIOAフレームワークは,有望な安全性自動検証技術であるとされているものの,具体的検証例が少ないため記述能力に不明な点が多かったが,今回の結果により,その記述能力の一端が解明されたといえる.また,落とし戸付き関数の計算量的一方向性は電子署名以外のプリミティブ(OAEP暗号など)の安全性証明にも用いられるため,今回Task-PIOAでの定義を与えたことにより,今後具体的検証例のさらなる拡充を目指す場合にも,再利用可能であるという利点がある.また,Task-PIOAフレームワークに基づく自動検証ツールを開発する際には動作チェックのための検証例としての活用も見込まれる.