1999 Fiscal Year Annual Research Report
セキュリティプロトコルの形式的記述および検証に関する基礎的研究
| Project/Area Number |
10680358
|
|---|
| Research Institution | KYUSHU UNIVERSITY |
|---|
Principal Investigator |
荒木 啓二郎 九州大学, 大学院・システム情報科学研究科, 教授 (40117057)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
田口 研治 筑紫女学園大学, 文学部, 助教授 (30294903)
後藤 幸功 九州大学, 大学院・システム情報科学研究科, 助手 (40315130)
岡村 耕二 九州大学, 情報処理教育センター, 助教授 (70252830)
張 漢明 (財)九州システム情報技術研究所, 第二研究室, 研究員
福田 晃 奈良先端科学技術大学院大学, 情報科学研究科, 教授 (80165282)
|
|---|
| Keywords | セキュリティプロトコル / 形式仕様記述 / 検証 / 並行動作システム / 振舞い記述 / なりすまし / 認証 / Secure Socket Layer (SSL)プロトコル |
|---|
| Research Abstract |
本研究では、大規模複雑化するソフトウェアシステムの機能や品質を保証するために形式手法を適用する研究の一環として、上記のネットワークセキュリティを具体的な問題対象として、その形式仕様記述と検証を行った。平成11年度では、自然言語による仕様記述が与えられているSecure Socket Layer(SSL)を具体的なセキュリティプロトコルの対象として、形式仕様記述言語を用いた厳密な仕様記述を行い、正規の通信者同士の通信は成功し、不正行為者による通信は失敗することを証明した。
また、より一般的に、ネットワークセキユリティおよび認証のための方式を提案して、実験ネットワーク上でその機能を確認し評価した。ネットワークセキュリティや認証を必要とするアプリケーションの例として、マルチメディアコンテンツの配送システムを想定し、そのための通信方式の提案と試作システムの開発を行った。このアプリケーションの上で、ユーザ認証およびセキュリティ保護機能をどのように実現するかについては今後の課題である。
さらに、セキュリティプロトコルに限定せずに、並行動作システムの形式仕様記述を行うために、形式仕様記述言語zとプロセス代数とを統合した記述法を提示し、分散処理システムにおけるメモリー貫性モデルの記述と検証に適用した。
|
-
[Publications] 荒木啓二郎: "情報通信システムの先進的事例と情報化における問題点"URC都市科学. 41. 14-24 (1999)
-
[Publications] 田中俊行: "形式手法による配電線自動制御システムのドメイン分析"ソフトウェア工学の基礎VI. 13-17 (1999)
-
[Publications] 張漢明: "モデル形式支援のための仕様記述変換技術"情報処理学会論文誌(数理モデル化と応用). 40・SIG9. 18-29 (1999)
-
[Publications] 後藤幸功: "インターネットにおけるQoS保証された動画配送システムの設計と実装"情報処理学会論文誌. 40・11. 4127-4142 (1999)
-
[Publications] 田中俊行: "SSL プロトコルの形式仕様記述と検証"情報処理学会論文誌(数理モデル化と応用). 40・SIG9. 51-61 (1999)
-
[Publications] 高田司郎: "リリース・コンシステンシ・モデルとその実現の形式的仕様記述について"情報処理学会論文誌(数理モデル化と応用). 40・SIG9. 1-17 (1999)
-
[Publications] 荒木啓二郎(共編): "IFM'99-Proceedings of the 1st International Conference on Integrated Formal Methods"Springer-Verlag. xiv,477 (1999)
