暗号プロトコルの数理的構造と検証補完に関する基礎研究

2002 Fiscal Year Annual Research Report

• Project/Area Number: 14780225
• Research Institution: Kyushu University
• Principal Investigator: 森 雅生 九州大学, 大学院・システム情報科学研究院, 助手 (20284549)
• Keywords: 暗号プロトコル / 仕様検証

Research Abstract

本年の研究では以下の2点について、暗号プロトコルについて安全性と冗長性の観点から研究を進めた。
○モノイドによる暗号プロトコルの代数的モデル化…
暗号プロトコルの数理的モデル化、特に代数系を用いたモデル化を行った。通信メッセージ集合をモノイド(文字列)として定式化し、プロトコルの実行を通信と時系列関係によりグラフとして捉えるようにしている。安全なプロトコルの実行パターンを今回新たにいくつか発見し、現在モデル上での検証を行っている。
○安全性と冗長性に関する考察…
新たに発見した安全なプロトコル実行パターンについて安全性の検証を行っているが、この検証研究とは別に、プロトコル記述の冗長性の特徴について、現在提案されている各種の暗号プロトコルをもとに調査している。
平成14年12月にロンドン大学で行われたFormal Aspects of Security 2002に参加(情報収集)し、セキュリティ理論の研究者と、本研究での安全なプロトコル実行のパターンについて討論した。この学会では、各々の暗号プロトコルの検証と補完についての研究発表があったが、多くの研究成果に私の発見したパターンを見出すことができ、このことについて各研究者と意見交換した。これをもとにより一般的なモデルを構築し、発見している安全な実行パターンが妥当なものであることを証明することが課題となっている。