鍵交換プロトコルにおける推論的形式分析手法

• Item type: Journal(1)
• 公開日: 2015-03-15
• タイトル: 鍵交換プロトコルにおける推論的形式分析手法
• タイトル / 言語: en
• タイトル: A Formal Analysis Method with Reasoning for Key Exchange Protocols
• 言語: jpn
• キーワード / 主題Scheme: Other
• キーワード / 主題: [特集：学生・若手研究者論文] 暗号プロトコル，鍵交換プロトコル，形式分析，前向き推論
• 資源タイプ / 資源タイプ識別子: http://purl.org/coar/resource_type/c_6501
• 資源タイプ: journal article
• 著者所属: 埼玉大学大学院理工学研究科
• 著者所属: 埼玉大学大学院理工学研究科
• 著者所属: 埼玉大学大学院理工学研究科
• 著者所属(英): en
• 著者所属(英): Graduate School of Science and Engineering, Saitama Uniersity
• 著者所属(英): en
• 著者所属(英): Graduate School of Science and Engineering, Saitama Uniersity
• 著者所属(英): en
• 著者所属(英): Graduate School of Science and Engineering, Saitama Uniersity
• 著者名: 我妻, 和憲; 後藤, 祐一; 程, 京徳
• 著者名(英): Kazunori, Wagatsuma; Yuichi, Goto; Jingde, Cheng
• 論文抄録 / 内容記述タイプ: Other
• 論文抄録 / 内容記述: 暗号プロトコルの安全性を事前に検討するために形式分析が使用されている．モデル検証や定理証明などの従来の証明的形式分析手法において，ある暗号プロトコルに，ある欠陥がないことを検証する際には，その欠陥を分析前に分析者が列挙できていなければならない．これら証明的形式分析手法では，分析者が分析前に列挙していない欠陥は検証できない．このため，分析前に分析対象の欠陥を列挙せずに前向き推論を用いてプロトコルの仕様に暗黙的に含まれる欠陥を導出するという推論的形式分析手法のアイデアが提案され，また，分析における前向き推論を基礎づける論理体系が示された．しかし，推論的形式分析手法の具体的な手法はいまだ確立されていない．本論文では，暗号プロトコルの一種である鍵交換プロトコルにおいて，推論的形式分析手法を提案し，提案手法が有用であることを実証した．証明的形式分析手法で分析者が分析前に欠陥を列挙していなかった鍵交換プロトコルにおいて，提案手法により，分析前に列挙していなかった欠陥を検出できることを確認した．したがって，提案手法は分析者が見落とした欠陥の検出に有用であるといえる．さらに，提案手法は様々な暗号プロトコルに適用させるように拡張が可能であることを示した．
• 論文抄録(英) / 内容記述タイプ: Other
• 論文抄録(英) / 内容記述: Formal analysis of cryptographic protocols is used to find flaws before using the protocols. In traditional formal analysis method with proving such as model checking and theorem proving, analysts must enumerate flaws before analysis when they verify that a cryptographic protocol has not those flaws. In other words, those methods can detect only flaws that analysts enumerate. An idea of formal analysis to use forward reasoning to detect flaws of cryptographic protocols was proposed and logic systems underlying forward reasoning were presented. However, its concrete method is not established. This paper presents a concrete method of formal analysis with reasoning for key exchange protocols and shows its effectiveness. By the proposed method, we analyzed a key exchange protocol and detect flaws that analysts did not enumerate in traditional formal analysis method with proving. Therefore, the proposed method is effective for detecting flaws that analysts overlooked. Finally, we discussed that the proposed method can be extended to various cryptographic protocols.
• 書誌レコードID / 収録物識別子タイプ: NCID
• 書誌レコードID / 収録物識別子: AN00116647
• 書誌情報: 情報処理学会論文誌; 巻 56, 号 3, p. 903-910, 発行日 2015-03-15
• ISSN / 収録物識別子タイプ: ISSN
• ISSN / 収録物識別子: 1882-7764