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

2015 年度 実施状況報告書

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

研究実績の概要

本研究は、暗号プロトコルの安全性検証法を、数理的技法（形式手法、またはformal method）の一つである論理推論をもとに構築することを目的としている。特に、知識論理と呼ばれる推論体系の一種である動的知識論理（Dynamic Epistemic Logic）を用いて、プロトコルの実行における参加者間での知識の形成過程を分析することにより、プロトコルの安全性を示す検証法の確立を目指している。
このような検証法においては、参加者間で成り立つ知識命題の形成過程に関する十分な記述力と、知識命題と安全性との間で成り立つ一般的な性質を分析できるだけの単純さが求められる。
昨年度に引き続き、今年度も、動的知識論理をもとにした目的とする推論体系の構築を目指し研究を遂行した。特に、これまでの研究で得られていなかった暗号プロトコルの実行過程を十分に記述できるような論理言語と公理系を与えることを目標としてきた。昨年度までの研究では、こうした論理体系を一階述語論理の言語をもとに構築することを実施してみたが、記述力が得られる代わりに、論理言語そのものが非常に複雑になってしまっていた。そのため今年度は、命題論理をもとにした動的知識論理への単純化と、動的様相を排した一階述語知識論理による定式化を目指した。現時点においては、まだ推論体系の確立には至っていないものの、前者のアプローチが有力であることが分かってきており、今後もこの方針で研究を遂行したいと考えている。

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

3: やや遅れている

理由

今年度も、プロトコルの実行過程と参加者の知識状態を記述しうる論理体系の構築を目標に研究を遂行してきた。先に述べたように、十分な記述力と分析のための見通しの良さを兼ね備えた論理体系のが求められているが、両者は一般に背反するため、現在においてもまだ有力な論理体系を得るに至っていない。今年度に引き続き、来年度はこうした課題の解決を早急に行う必要があると考えている。

今後の研究の推進方策

前述の通り、来年度においても引き続き、これまでに得られた知見をもとに目標とする論理体系の構築を目指し研究を遂行する予定である。また来年度は最終年度にあたることから、遅くとも後半からは、それまでに得られた論理体系に対する健全な意味論を与えるとともに、この体系を使った具体的な暗号プロトコルの分析を行う予定である。ここで対象とする暗号プロトコルは段階的に選択する。すなわち、最初は比較的単純で脆弱性についてもよく知られたプロトコルを対象とし、その後より複雑な契約署名プロトコルや合理的秘密分散プロトコルなどへと応用することを計画している。さらに、以上で得られた検証法をもとに、計算論的安全性への応用についても検討する。

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

当初予定していた研究成果の発表が遅れたため、発表のために必要となる旅費等の予算に未使用額が生じた。

次年度使用額の使用計画

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