| 研究課題/領域番号 |
10680358
|
|---|
| 研究機関 | 九州大学 |
|---|
研究代表者 |
荒木 啓二郎 九州大学, 大学院・システム情報科学研究科, 教授 (40117057)
|
|---|
| 研究分担者 |
田口 研治 筑紫女学園大学, 文学部, 助教授 (30294903)
後藤 幸功 九州大学, 大学院・システム情報科学研究科, 助手 (40315130)
岡村 耕二 九州大学, 情報処理教育センター, 助教授 (70252830)
張 漢明 (財)九州システム情報技術研究所, 第二研究室, 研究員
福田 晃 奈良先端科学技術大学院大学, 情報科学研究科, 教授 (80165282)
|
|---|
| キーワード | セキュリティプロトコル / 形式仕様記述 / 検証 / 並行動作システム / 振舞い記述 / なりすまし / 認証 / Secure Socket Layer (SSL)プロトコル |
|---|
| 研究概要 |
本研究では、大規模複雑化するソフトウェアシステムの機能や品質を保証するために形式手法を適用する研究の一環として、上記のネットワークセキュリティを具体的な問題対象として、その形式仕様記述と検証を行った。平成11年度では、自然言語による仕様記述が与えられているSecure Socket Layer(SSL)を具体的なセキュリティプロトコルの対象として、形式仕様記述言語を用いた厳密な仕様記述を行い、正規の通信者同士の通信は成功し、不正行為者による通信は失敗することを証明した。
また、より一般的に、ネットワークセキユリティおよび認証のための方式を提案して、実験ネットワーク上でその機能を確認し評価した。ネットワークセキュリティや認証を必要とするアプリケーションの例として、マルチメディアコンテンツの配送システムを想定し、そのための通信方式の提案と試作システムの開発を行った。このアプリケーションの上で、ユーザ認証およびセキュリティ保護機能をどのように実現するかについては今後の課題である。
さらに、セキュリティプロトコルに限定せずに、並行動作システムの形式仕様記述を行うために、形式仕様記述言語zとプロセス代数とを統合した記述法を提示し、分散処理システムにおけるメモリー貫性モデルの記述と検証に適用した。
|
