2022 Fiscal Year Final Research Report
A model checking method for secure routing protocols
| Project/Area Number |
18K11262
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Review Section |
Basic Section 60060:Information network-related
|
|---|
| Research Institution | Osaka Institute of Technology (2022)
Osaka University (2018-2021) |
|---|
Principal Investigator |
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
矢内 直人 大阪大学, 大学院情報科学研究科, 准教授 (30737896)
|
|---|
| Project Period (FY) |
2018-04-01 – 2023-03-31
|
| Keywords | モデル検査 / 状態爆発抑制 / 経路保証プロトコル |
|---|
| Outline of Final Research Achievements |
In this research, we developed a method to suppress state explosion that occurs during formal verification of secure routing protocols used in sensor networks and ad hoc networks. The basic idea is to reduce the number of states to be traversed by regarding that states with the same network topology shape are equivalent. Since the target protocol uses signatures to guarantee the correctness of routes, the developed method incorporates a method that signatures included in the equvalent states are considered equivalent. We applied this method to the model checker SPIN to verify the secure routing protocol, and showed that the number of states is reduced and the execution time is shortened.
|
| Free Research Field |
情報学
|
| Academic Significance and Societal Importance of the Research Achievements |
センサネットワークやアドホックネットワークが社会で展開されることを考えると，経路が構築されること，情報の通信経路が信頼できることが重要である．経路保障プロトコルは，それらを実現するものである．これを用いるにあたって，正しく動作するかどうかを事前に検証することが必要である．従来の方法では，状態爆発により検証の完了が困難である場合があることや検証に必要な実行時間が長くなることがあるが，本研究で開発した手法を用いて状態爆発を抑制することで，検証に必要な時間を削減することが可能となった．
|
