| 研究課題/領域番号 |
10680358
|
|---|
| 研究機関 | 九州大学 |
|---|
研究代表者 |
荒木 啓二郎 九州大学, 大学院システム情報科学研究科, 教授 (40117057)
|
|---|
| 研究分担者 |
張 漢明 九州システム情報技術研究所, 第二研究室, 研究員
福田 晃 奈良先端科学技術大学院大学, 情報科学研究科, 教授 (80165282)
田口 研治 九州大学, 大学院システム情報科学研究科, 助手 (30294903)
岡村 耕二 九州大学, 情報処理教育センター, 助教授 (70252830)
程 京徳 九州大学, 大学院システム情報科学研究科, 教授 (30217228)
|
|---|
| キーワード | セキュリティプロトコル / 形式仕様記述 / 検証 / 並行動作システム / 振舞い記述 / なりすまし / Secure Socket Laver (SSL)プロトコル |
|---|
| 研究概要 |
本年度は、セキュリティプロトコルとして一般にも広く使用されてぃるSecure Socket Layer(SSL)を具体的な対象として、その形式仕様記述と不正行為防止の証明とを行った。また、より一般的な並行動作システムの振舞いを記述し分析するための基礎付けを与えた。以下に、これらについてより具体的に述べる。
(1) SSLプロトコルと不正行為の形式記述:
SSLの英文仕様書を基にして、その形式仕様をRSL(RAISE Specification Language)という形式仕様記述言語を用いて記述した。併せて、サーバへのなりすましという不正行為の形式的記述も行った。これらの記述は、手続き型と適用型との二つの異なる様式で行い、それらの特徴や相違について議論した。
(2) SSLプロトコルの検証:
上述の形式仕様のうち適用型の記述を用いて、SSLのハンドシェイクプロトコルが正規のサーバとクライアントとの間で正しく動作すること、ならびに、サーバへのなりすましという不正行為が必ず失敗することを証明した。手続き型の記述については、その動作についての机上シミュレーションにより上記の性質の確認を行った。
(3) 並行動作システムの振舞い解析:
通信プロトコルのみならずより一般的な並行動作システムの振舞いを厳密に記述して、その性質について分析および証明を行うための基礎として、時制論理、モバイルエージェント、リリースコンシステンシに関するモデル化ならびに理論を提示した。
|
