2017 Fiscal Year Annual Research Report
A Study on Security Verification Method of Cryptographic Protocols by Analysis of Knowledge Formation Process
| 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）を用いて、プロトコルの実行における参加者間での知識の形成過程を分析することにより、プロトコルの安全性を示す検証法の確立を目指している。このような検証法においては、参加者間で成り立つ知識命題の形成過程に関する十分な記述力と、知識命題と安全性との間で成り立つ一般的な性質を分析できるだけの単純さが求められる。
昨年度予定していた研究実施内容を、今年度も継続して実施した。特に今年度は、見通しの良い単純な論理体系を得るためのアプローチとして、命題論理をもとにした動的知識論理や、動的様相を配した一階述語論理による定式化を目指した。前者のアプローチについては、昨年度に引き続きプロトコルの記述力が問題となり、本研究で対象とするような暗号プロトコルそのものについての十分な検証法を得ることは難しかった。しかしながら、分散システムにおける合意形成などに使われるある種のプロトコルの検証法などへの応用の可能性を示唆する結果をえることができた。また、後者のアプローチについては、体系が複雑になるという問題はあるものの、プロトコルの実行に関していくつかの仮定を置くことで、検証法として有用な体系に近づくことができた。今後は、これらの成果を取りまとめ、国際会議等で発表することを計画している。
|
Research Products
(1 results)
