A model checking method for secure routing protocols

2022 Fiscal Year Annual Research Report

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

Outline of Annual Research Achievements

本課題では，センサネットワークにおける，経路保証プロトコルの効率的な形式検証の開発を行った．対象となる経路保証プロトコルが，どのような経路でも適切に構築することが可能かどうかを確かめるにあたって，形式検証ツールであるSPINを用いて検証を行った．検証を行うにあたって，ネットワーク内の端末数が増加すると，可能な経路が爆発的に増加し，全ての経路構築が可能かどうかを検証することは，計算時間や利用可能な主記憶領域の制限により非常に困難である．
端末数が増加すると，構築可能な経路数が爆発的に増加するが，これは，検証を行うにあたっては，状態の爆発的な増加を表すことになる．状態数の爆発的な増加は，それらの状態を保存する主記憶領域の増大を表し，端末間のメッセージのやり取りによって生じる状態遷移の増加を引き起こす．その結果，全ての状態遷移を走査するための実行時間が増加することとなる．
この状態数の爆発を抑制することで，実行時間や主記憶利用量の削減を行う必要が生じる．
状態数の爆発抑制にあたって，ネットワークトポロジに注目する．メッセージのやり取りにより，構築される経路は端末の接続状況を表すが，その形状が同じである場合は同じ状態とみなすことで，端末数が増加したとしても状態数の爆発を抑制することが可能となった．
対象が経路保証プロトコルであり，経路保証のためにディジタル署名を用いているため，ネットワークトポロジの形状が同じだとしても，署名自体は異なるものになる可能性がある．そこで，署名も含めて同じ状態とみなすことができるような方法を開発した．
この方法を形式検証ツールであるSPINに組み込み，開発した手法を用いる場合と用いない場合の計算時間や主記憶利用量を比較したところ，計算時間，主記憶利用量ともに大きく削減することができ，開発した手法は，効率的に経路保証プロトコルを検証することができることを示した．