経路保証プロトコルの効率的な安全性検証手法の開発

2022 Fiscal Year Research-status Report

• Project/Area Number: 21K11866
• Research Institution: Osaka Institute of Technology
• Principal Investigator: 小島 英春 大阪工業大学, 情報科学部, 准教授 (90610949)
• Co-Investigator(Kenkyū-buntansha): 矢内 直人 大阪大学, 大学院情報科学研究科, 准教授 (30737896)
• Project Period (FY): 2021-04-01 – 2024-03-31
• Keywords: 安全性検証 / 経路保証プロトコル / モデル検査 / 無線マルチホッププロトコル

Outline of Annual Research Achievements

本研究では，経路保証プロトコルの安全性の検証を行う．対象となる経路保証プロトコルは，無線アドホックネットワークや無線センサネットワーク上で動作することを想定しており，端末が動的にネットワークへ参加や離脱を行うことが考えられる．このようなネットワークでは，さまざまな経路が構築される可能性がある．どのような経路が構築されても，適切に経路保証を行うことができることを示す．検証を行うにあたって，端末数が増加すると構築可能な経路の数が爆発的に増加することが挙げられる．その場合，全ての構築可能な経路を対象に検証を行うことは非常に難しい．そこで，効率的に検証を行う方法を開発する．検証を行うために，安全性を検証するためのツールを用い，そのツールのためのモデルを構築する．このモデルは，経路保証プロトコルの動作を表しており，端末間の接続状況を用いてどのような経路が構築されているかを表すネットワークトポロジも表現する．このトポロジを表現する際に，トポロジ形状が同じ場合には，同じ状態とみなすことで，検証の対象となる経路を削減することを目指す．対象となる経路削減方法を開発し，その方法を用いて安全性検証を行う．ツールにその方法を適用し，実行時間の比較，使用メモリ量の比較を行うことで，効率的に検証を行うことが可能であることを示す．

Current Status of Research Progress

2: Research has progressed on the whole more than it was originally planned.

Reason

対象とするプロトコルのモデル作成を行い，このモデルを用いてツールでの実行を行なっている．端末数増加に伴う経路数の増加を抑制する方法の開発を行なっており，この手法を用いた結果を論文としてまとめ，投稿する予定である．

Strategy for Future Research Activity

開発した手法をもとに論文の作成を行う．また，国際会議，論文誌への投稿を予定している．

Causes of Carryover

新型コロナウィルス感染症に伴い，国際会議の投稿を自重しており，初年度に計上している旅費分がそのまま，残金として繰り越している状況である．2023度では，国際会議への投稿を進めることで，参加費や旅費として使用していく予定である．