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

2016 Fiscal Year Research-status Report

• Project/Area Number: 26330076
• Research Institution: University of Tsukuba
• Principal Investigator: 長谷部 浩二 筑波大学, システム情報系, 助教 (80470045)
• Project Period (FY): 2014-04-01 – 2018-03-31
• Keywords: 仕様記述・検証 / 数理的技法 / 暗号プロトコル / 安全性検証 / 論理推論体型

Outline of Annual Research Achievements

本研究は、暗号プロトコルの安全性検証法を、数理的技法（形式手法、またはformal method）の一つである論理推論をもとに構築することを目的としている。特に、知識論理と呼ばれる推論体型の一種である動的知識論理（Dynamic Epistemic Logic）を用いて、プロトコルの実行における参加者間での知識の形成過程を分析することにより、プロトコルの安全性を示す検証法の確立を目指している。
このような検証法においては、参加者間で成り立つ知識命題の形成過程に関する十分な記述力と、知識命題と安全性との間で成り立つ一般的な性質を分析できるだけの単純さが求められる。
昨年度に引き続き、今年度も、上記のような性質を持つ論理体系を求めて研究を遂行した。特に、これまで試みてきた一階述語論理の言語を用いた動的知識論理をもとにすることにより生じる様々な困難に鑑み、今年度は命題論理の言語をもとにした動的知識論理への単純化と、動的様相を排した一階述語論理による定式化を目指した。前者については、プロトコルの実行過程に関する表現をかなり限定すればある程度の分析が可能となることが分かったが、プロトコルで送受信されるメッセージの形式は基本的に無限にあることから、命題論理の言語ではどうしても表現しきれない部分があるという課題が残されている。また、後者の一階述語論理の言語をもとにするアプローチでは、様相概念と一階述語論理を組み合わせることから生じる意味論的問題があることが判明した。以上のことから、来年度は前者のアプローチをさらに推し進めることを計画している。

Current Status of Research Progress

4: Progress in research has been delayed.

Reason

今年度も、プロトコルの実行過程と、プロトコルの参加者の知識状態および推論過程を記述しうる論理体型の構築を目標に研究を遂行してきた。先に述べたように、今年度は、命題論理言語をもとにした動的知識論理による定式化と、一階述語論理言語をもとにした（動的様相を排した）知識論理による定式化の２つのアプローチを試みた。しかしながら、十分な記述力と分析のための見通しの良さを兼ね備えた論理体型を得るには至っていない。今年度の研究により、前者のアプローチが有力であることが明らかになってきたことから、来年度はこの方向で研究を継続する予定である。
なお、当初は研究実施期間を３年間として計画したが、上述のように予定よりも研究の進行が遅れていることから、１年間研究期間を延長することとした。

Strategy for Future Research Activity

前述の通り、来年度においても引き続き、これまでに得られた知見をもとに目標とする論理体系の構築を目指し研究を遂行する予定である。当初、本研究課題の研究期間は３年間として計画されていたが、残念ながら、目標としていた論理体系が得られていないことから、実施期間を１年間延長して研究を継続することを計画している。
今後は、目標とする論理体系を年度の前半までに構築し、後半では、それまでに得られた論理体系に対する健全な意味論を与えるとともに、この体系を使った具体的な暗号プロトコルの分析を行う予定である。ここで対象とする暗号プロトコルは段階的に選択する。すなわち、最初は比較的単純なものから扱い、徐々により複雑な契約署名プロトコルや合理的秘密分散プロトコルなどへと応用することを目指している。

Causes of Carryover

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

Expenditure Plan for Carryover Budget

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