1998 Fiscal Year Annual Research Report

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

Research Project

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

Research Products
(6 results)

All Other

All Publications (6 results)

[Publications] 張漢明: "A Proposal of 4W Diagram Notation for Requirements Definition Processes" Proc. of International Workshop on Principles of Software Evolution. 188-191 (1998)
[Publications] 田口研治: "A Calculus Based on the Agent-Place Model" Proc. Int'l Conf. on Formal Engineering Methods ‘98. 56-63 (1998)
[Publications] 田中俊行: "Formal Specification and Verification of Security Protocols using RSL" ICSE‘98 Int'l Workshop on Computing and Communication in the Presence of Mobility. (1998)
[Publications] 田中俊行: "SSL プロトコルの形式仕様記述と検証" 情報処理学会数理モデルと問題解決研究会. 23-5. 25-30 (1999)
[Publications] 程京徳: "Temporal Relevant Logic as the Logic Basis for Reasoning about Dynamics of Concurrent Systems" Proc. 1998 IEEE-SMC Annual Int'l Conf. on Systems, Man, and Cybernetics. Vol.1. 794-799 (1998)
[Publications] 高田司郎: "リリース・コンシステンシ・モデルとその実現の形式的仕様記述について" 情報処理学会論文誌(数理モデル化と問題解決). 印刷中. (1999)

1998 Fiscal Year Annual Research Report

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

Principal Investigator

荒木 啓二郎 九州大学, 大学院システム情報科学研究科, 教授 (40117057)

Research Products

[Publications] 張 漢明: "A Proposal of 4W Diagram Notation for Requirements Definition Processes" Proc. of International Workshop on Principles of Software Evolution. 188-191 (1998)

[Publications] 田口 研治: "A Calculus Based on the Agent-Place Model" Proc. Int'l Conf. on Formal Engineering Methods ‘98. 56-63 (1998)

[Publications] 田中 俊行: "Formal Specification and Verification of Security Protocols using RSL" ICSE‘98 Int'l Workshop on Computing and Communication in the Presence of Mobility. (1998)

[Publications] 田中 俊行: "SSL プロトコルの形式仕様記述と検証" 情報処理学会数理モデルと問題解決研究会. 23-5. 25-30 (1999)

[Publications] 程 京徳: "Temporal Relevant Logic as the Logic Basis for Reasoning about Dynamics of Concurrent Systems" Proc. 1998 IEEE-SMC Annual Int'l Conf. on Systems, Man, and Cybernetics. Vol.1. 794-799 (1998)

[Publications] 高田 司郎: "リリース・コンシステンシ・モデルとその実現の形式的仕様記述について" 情報処理学会論文誌(数理モデル化と問題解決). 印刷中. (1999)

荒木啓二郎九州大学, 大学院システム情報科学研究科, 教授 (40117057)

[Publications] 張漢明: "A Proposal of 4W Diagram Notation for Requirements Definition Processes" Proc. of International Workshop on Principles of Software Evolution. 188-191 (1998)

[Publications] 田口研治: "A Calculus Based on the Agent-Place Model" Proc. Int'l Conf. on Formal Engineering Methods ‘98. 56-63 (1998)

[Publications] 田中俊行: "Formal Specification and Verification of Security Protocols using RSL" ICSE‘98 Int'l Workshop on Computing and Communication in the Presence of Mobility. (1998)

[Publications] 田中俊行: "SSL プロトコルの形式仕様記述と検証" 情報処理学会数理モデルと問題解決研究会. 23-5. 25-30 (1999)

[Publications] 程京徳: "Temporal Relevant Logic as the Logic Basis for Reasoning about Dynamics of Concurrent Systems" Proc. 1998 IEEE-SMC Annual Int'l Conf. on Systems, Man, and Cybernetics. Vol.1. 794-799 (1998)

[Publications] 高田司郎: "リリース・コンシステンシ・モデルとその実現の形式的仕様記述について" 情報処理学会論文誌(数理モデル化と問題解決). 印刷中. (1999)