A Study on Security Verification Method of Cryptographic Protocols by Analysis of Knowledge Formation Process

2017 Fiscal Year Final Research Report

• Project/Area Number: 26330076
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Multi-year Fund
• Section: 一般
• Research Field: Software
• Research Institution: University of Tsukuba
• Principal Investigator: Hasebe Koji 筑波大学, システム情報系, 准教授 (80470045)
• Project Period (FY): 2014-04-01 – 2018-03-31
• Keywords: 仕様記述・検証 / 数理的技法 / 暗号プロトコル / 安全性検証 / 論理推論体系

Outline of Final Research Achievements

This research aimed at establishing a verification method showing the safety of cryptographic protocols by analyzing the formation process of knowledge among participants in the execution of protocols using epistemic logic.
In this research, formalization with the Propositional Dynamic Epistemic Logic and formalization with First-Order Predicate Epistemic Logic excluding dynamic modal operators were conducted. As a result, problems concerning the expressiveness of the logical system and the complexity of the system were clarified. However, the results suggested the possibility of application to verification methods of some protocols in distributed systems. Moreover, by putting some assumptions about the execution of the protocol, it seems that we could obtain a system useful as a verification method.

Free Research Field

数理的技法