知識の形成過程の分析による暗号プロトコルの安全性検証法に関する研究

2014 年度 実施状況報告書

• 研究課題/領域番号: 26330076
• 研究機関: 筑波大学
• 研究代表者: 長谷部 浩二 筑波大学, システム情報系, 助教 (80470045)
• 研究期間 (年度): 2014-04-01 – 2017-03-31
• キーワード: 仕様記述・検証 / 数理的技法 / 暗号プロトコル / 安全性検証 / 論理推論体系

研究実績の概要

本研究は、暗号プロトコルの安全性検証法を、数理的技法（形式手法、formal methods）の一つである論理推論をもとに構築することを目的としている。特に、知識論理と呼ばれる推論体系の一種である動的知識論理（Dynamic Epistemic Logic）を用いて、プロトコルの実行における参加者間での知識の形成過程を分析することにより、プロトコルの安全性を示す検証法の確立を目指している。
今年度は、動的知識論理をもとに、暗号プロトコルの安全性検証のための論理言語と公理系を与えることを目標に研究を遂行した。特に、参加者間で成り立つ知識命題がプロトコルの実行過程でどのように形成され、またその知識命題と安全性との間で成り立つ一般的な性質を明らかにするため、なるべく単純な論理体系によって定式化することを試みてきた。現時点では、先行研究などをもとに概ねこの論理体系が得られているが、プロトコルで扱われるメッセージの組み合わせが無限にあることから、基本となる命題が述語論理に頼らざるを得なくなっている。しかしながら、先に述べたなるべく単純な論理体系を与えるという意味では、命題論理をもとにした動的知識論理へと単純化するか、あるいは動的様相を排した一階述語論理をもとにした知識論理によって定式化するかを行う必要があると考えられる。現時点では、こうした論理体系の単純化が課題として残されており、特に前者のアプローチでの単純化を目指して研究を遂行している。

現在までの達成度 (区分)

3: やや遅れている

理由

今年度は、プロトコルの実行過程を記述しうる論理体系の構築を主な目標とし、さらにそれに伴う意味論の構築やプロトコルの分析なども目指して研究を行ってきた。先に述べたように、論理体系の構築は行われたものの、プロトコルの分析を行うためには更なる単純化が求められている。そのため、当初予定していたプロトコルの分析なども今後の課題として残されており、来年度は、これらの解決を早急に行う必要があると考えている。

今後の研究の推進方策

前述の通り、今後はまず、これまでに得られた論理体系の単純化を目指し研究を遂行する予定である。また、この作業がある程度進んだ段階で、健全な意味論を与えるとともに、この体系を使って暗号プロトコルを分析することを目指す。この分析においては、Dolev-Yaoモデルと呼ばれる攻撃者のモデルの範囲内での安全性のみを扱い、また比較的単純なプロトコルを対象とするところから出発する。これにより、知識命題と安全性との間で一般的に成り立つ性質を、推論体系におけるメタ定理として示す。ここでは特に、安全性の判定に有益な、いくつかの単純な性質の発見を目標としている。こうしたメタ定理を用いて、あるパターン化された命題を証明することによって、プロトコルの安全性を示す検証法を構築する。以上で述べた計画が達成された後には、以上で得られた検証法を他の様々なプロトコルに適用する。特にここで対象とするのは、契約署名プロトコルや合理的秘密分散プロトコルである。これらのプロトコルについては、先の認証プロトコルと異なり、秘匿性や公平性といった性質が問題となる。こうした性質についても扱いうる検証法へと拡張することが主要な課題となる。さらに、以上で得られた成果をもとに、証明図の拡張や合成によるプロトコルの安全性検証法や、証明可能な知識命題による安全性概念の階層化、また安全でないプロトコルをこの検証法を用いて改良する方法などについても検討する。また一方で、計算論的安全性検証法への応用も検討することを予定している。

次年度使用額が生じた理由

当初予定していた研究成果の発表が遅れたため、発表のために必要となる旅費等の予算を翌年度で使用できるようにしたため。

次年度使用額の使用計画

次年度使用額は、主に研究発表のための旅費として支出する予定である。