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: Hideharu Kojima 大阪工業大学, 情報科学部, 准教授 (90610949)
• Co-Investigator(Kenkyū-buntansha): 矢内 直人 大阪大学, 大学院情報科学研究科, 准教授 (30737896)
• Project Period (FY): 2018-04-01 – 2023-03-31
• Project Status: Completed (Fiscal Year 2022)
• Budget Amount: ¥4,290,000 (Direct Cost: ¥3,300,000、Indirect Cost: ¥990,000); Fiscal Year 2020: ¥910,000 (Direct Cost: ¥700,000、Indirect Cost: ¥210,000); Fiscal Year 2019: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000); Fiscal Year 2018: ¥2,210,000 (Direct Cost: ¥1,700,000、Indirect Cost: ¥510,000)
• 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.

Academic Significance and Societal Importance of the Research Achievements

センサネットワークやアドホックネットワークが社会で展開されることを考えると，経路が構築されること，情報の通信経路が信頼できることが重要である．経路保障プロトコルは，それらを実現するものである．これを用いるにあたって，正しく動作するかどうかを事前に検証することが必要である．従来の方法では，状態爆発により検証の完了が困難である場合があることや検証に必要な実行時間が長くなることがあるが，本研究で開発した手法を用いて状態爆発を抑制することで，検証に必要な時間を削減することが可能となった．

Research Products

• [Journal Article] ISDSR+: Improving the Security and Availability of Secure Routing Protocol (2019)
  • Author(s): Kojima Hideharu、Yanai Naoto、Cruz Jason Paul
  • Journal Title: IEEE Access Volume: 7 Pages: 74849-74868
  • DOI: 10.1109/access.2019.2916318
  • Peer Reviewed / Open Access
• [Presentation] A Model Checking Method for Secure Routing Protocols by SPIN with State Space Reduction (2020)
  • Author(s): Kojima Hideharu、Yanai Naoto
  • Organizer: 2020 IEEE International Parallel and Distributed Processing Symposium Workshops(APDCM2020)
  • Int'l Joint Research
• [Presentation] Implementation and Evaluation of ISDSR in Emulation Environments (2019)
  • Author(s): Shinnosuke Shimizu, Hideharu Kojima, Naoto Yanai, Tatsuhiro Tsuchiya
  • Organizer: 2019 IEEE Wireless Communications and Networking Conference, WCNC2019
  • Int'l Joint Research
• [Presentation] A State Space Suppression Method for Formal Verification of Secure Routing Protocols With SPIN (2019)
  • Author(s): Hideharu Kojima, Naoto Yanai
  • Organizer: Seventh International Symposium on Computing and Networking Workshops, CANDAR 2019 Workshops
  • Int'l Joint Research
• [Presentation] A State Space Suppression Method for Formal Verification of Secure Routing Protocols With SPIN (2019)
  • Author(s): Hideharu Kojima, Naoto Yanai
  • Organizer: IEEE International Symposium on Software Reliability Engineering Workshops, ISSRE Workshops 2019
  • Int'l Joint Research
• [Presentation] アドホックネットワークプロトコルのモデル検査における状態数削減手法 (2019)
  • Author(s): 小島英春, 矢内直人
  • Organizer: 第18回電子情報通信学会ネットワークソフトウエア研究会予稿集
• [Presentation] 経路保証プロトコルを対象にしたSPIN を用いたモデル検査にむけて (2018)
  • Author(s): 小島英春, 矢内直人
  • Organizer: 第16回電子情報通信学会ネットワークソフトウェア研究会,