セキュリティプロトコルの形式的記述および検証に関する基礎的研究

1999 年度 研究成果報告書概要

• 研究課題/領域番号: 10680358
• 研究種目: 基盤研究(C)
• 配分区分: 補助金
• 応募区分: 一般
• 研究分野: 計算機科学
• 研究機関: 九州大学
• 研究代表者: 荒木 啓二郎 九州大学, 大学院・システム情報科学研究科, 教授 (40117057)
• 研究分担者: 田口 研治 筑紫女学園大学, 文学部, 助教授 (30294903) ; 後藤 幸功 九州大学, 大学院・システム情報科学研究科, 助手 (40315130) ; 岡村 耕二 九州大学, 情報処理教育センター, 助教授 (70252830) ; 張 漢明 財団法人九州システム情報技術研究所, 第二研究室, 研究員 ; 福田 晃 奈良先端科学技術大学院大学, 情報科学研究科, 教授 (80165282) ; CHANG Hang-myung Inst. Of Systems and Information Technologies Researcher
• 研究期間 (年度): 1998 – 1999
• キーワード: セキュリティプロトコル / 形式仕様記述 / 検証 / 並行動作システム / 振舞い記述 / なりすまし / 認証 / Secure Socket Layer(SSL)プロトコル

研究概要

最近のコンピュータネットワークの日常社会生活の中への浸透は急激でかつ広範囲に亘っている。このため、通信システムに対する機能および性能に対する社会的な要求は、より具体的でより高いものになってきている。特に、電子商取引きや遠隔医療などにおけるコンピュータネットワーク利用では、セキュリティの保護がなされていることが本質的に要求される。しかしながら、通信システムは並列処理システムであるために非決定的な振舞いをし、セキュリティ保護も含めてその機能や性質についての保証を与えることは容易ではない。
本研究では、大規模複雑化するソフトウェアシステムの機能や品質を保証するために形式手法を適用する研究の一環として、上記のネットワークセキュリティネットワークセキュリティおよび認証のための方式を提案して、実験ネットワーク上でその機能を確認し評価した。ネットワークセキュリティや認証を必要とするアプリケーションの例として、マルチメディアコンテンツの配送システムを想定し、そのための通信方式の提案と試作システムの開発を行った。このアプリケーションの上で、ユーザ認証およびセキュリティ保護機能をどのように実現するかについては今後の課題である。また、セキュリティプロトコルに限定せずに、並行動作システムの形式仕様記述を行うために、形式仕様記述言語zとプロセス代数とを統合した記述法を提示し、分散処理システムにおけるメモリ一貫性モデルの記述と検証に適用した。

研究成果

• [文献書誌] 田口研治: "A Calculus Based on the Agent-Place Model"Proc. Int'1 Conf. on Formal Engineering Methods. 56-63 (1998)
  • 説明: 「研究成果報告書概要(和文)」より
• [文献書誌] 山崎重一郎: "信用情報と利用ポリシーの管理が可能な相互認証を実現する認証基盤の提案"情報処理学会論文誌. 40. 296-309 (1999)
  • 説明: 「研究成果報告書概要(和文)」より
• [文献書誌] 荒木啓二郎: "情報通信システムの先進的事例と情報化における問題点"URC都市科学. 41. 14-24 (1999)
  • 説明: 「研究成果報告書概要(和文)」より
• [文献書誌] 後藤幸功: "インターネットにおけるQoS保証された動画配送システムの設計と実装"情報処理学会論文誌. 40. 4127-4142 (1999)
  • 説明: 「研究成果報告書概要(和文)」より
• [文献書誌] 田中俊行: "SSLプロトコルの形式仕様記述と検証"情報処理学会論文誌(数理モデル化と応用). 40. 51-61 (1999)
  • 説明: 「研究成果報告書概要(和文)」より
• [文献書誌] 高田司郎: "リリース・コンシステンン・モデルとその実現の形式的仕様記述について"情報処理学会論文誌(数理モデル化と応用). 40. 1-17 (1999)
  • 説明: 「研究成果報告書概要(和文)」より
• [文献書誌] 荒木啓二郎: "IFM' 99- Proceedings of the 1st International Conference on Integrated Formal Methods"Springer-Verlag. xiv, 477 (1999)
  • 説明: 「研究成果報告書概要(和文)」より
• [文献書誌] Taguchi, K. and Araki, K. :: "A Calculus Based on the Agent-Place Model"Proc. Int'l Conf. on Formal Engineering Methods '98. 56-63 (1998)
  • 説明: 「研究成果報告書概要(欧文)」より
• [文献書誌] Yamasaki, S. and Araki, K. :: "A Certificate Intrastructure Model for Integrated Cross-authentication with Warranty and use Policy Control"Trans. Information Processing Society of Japan. Vol.40, No.1(in Japanese). 296-309 (1999)
  • 説明: 「研究成果報告書概要(欧文)」より
• [文献書誌] Takata, S., Taguchi, K., Joe, K. and Fukuda, A. :: "Implementation and Formal Specification of Release Consistency Models"IPSJ Trans. Mathematical Modeling and Its Applications. Vol.40, No.SIG 2(TOM 1). 33-44 (1999)
  • 説明: 「研究成果報告書概要(欧文)」より
• [文献書誌] Araki, K. :: "Advanced Applications of Information Communications Systems and Issues in Information Technologies"URC Urban Sciences. Vol.41(in Japanese). 14-24 (1999)
  • 説明: 「研究成果報告書概要(欧文)」より
• [文献書誌] Goto, Y., Nagano, N. and Araki, K. :: "Design and Implementation of Video Transport System with QoS on the Internet"Trans. Information Processing Society of Japan. Vol.40, No.11(in Japanese). 4127-4141 (1999)
  • 説明: 「研究成果報告書概要(欧文)」より
• [文献書誌] Tanaka, T., George, C., Chang, H.-M. and Araki, K. :: "Formal Specification and Verification of the SSL Protocol"IPSJ Trans. Mathematical Modeling and Its Applications. Vol.40, No.SIG9(TOM2), (in Japanese). 51-61 (1999)
  • 説明: 「研究成果報告書概要(欧文)」より
• [文献書誌] Tanaka, S., Taguchi, K., Joe, K. and Fukuda, A. :: "A Formal Specification of a Release Consistency Model and Its Implementation"IPSJ Trans. Mathematical Modeling and Its Applications. Vol.40, No.SIG9(TOM2), (in Japanese). 1-17 (1999)
  • 説明: 「研究成果報告書概要(欧文)」より
• [文献書誌] Araki, K., Galloway, A. and Taguchi, K. (eds.) :: "IFM'99 - Proceedings of the 1st International Conference on Integrated Formal Methods"Springer-Verlag. XIV + 477 (1999)
  • 説明: 「研究成果報告書概要(欧文)」より