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

2021 Fiscal Year Research-status Report

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

Outline of Annual Research Achievements

本研究課題では，経路保証プロトコルを対象に経路構築が正しくできること，構築した経路自体が正しいことを検証する効率的な手法を開発することを目的としている．検証にあたっては，モデル検査を用いて形式的に検証を行う．経路を正しく構築することができることに加えて，構築した経路が正しいことも検証する必要がある．そのため，安全性の検証を可能とするツールの１つであるProverifを用いて検証を行う．対象とするプロトコルは，センサネットワークやアドホックネットワークなどの端末の動的な参加や離脱を考慮する必要があるネットワークを想定しており，このようなネットワークにおいてモデル検査を行うにあたって，端末数の増加により状態数が爆発することが考えられる．状態爆発が生じると非常に長い計算時間が必要になることや主記憶領域の枯渇などが生じ検証が完了しないことが考えられる．そのため，本研究では，状態爆発を抑制しつつ経路保証プロトコルの安全性の検証を効率的に行う手法を開発する．
2021年度では，検証を行うためのツールであるProverifを用いて経路保証プロトコルのモデル化を進めた．対象とするプロトコルであるISDSRはDSRを元にしているため，DSRのモデル化を行い，そこに経路保証のメカニズムを組み込んだモデルを作成している．このモデルを用いて，状態爆発の抑制手法の開発や効率的な安全性の検証を行うことを考えている．
また，2021年度では，コロナ対策関連の業務に時間を割く必要があり，状態爆発の抑制を行う手法を進めることが難しかった．しかし，安全性の検証を行うためのモデル構築は順調に進んでいる．

Current Status of Research Progress

3: Progress in research has been slightly delayed.

Reason

本研究では，安全性の検証に用いられるツールProverifを用いて対象とする経路保証プロトコルの安全性検証を行うことが目的である．そのために対象とするプロトコルのモデルの作成，検証時に生じる状態爆発の抑制手法の開発が必要である．2021年度では，コロナ関連対策などに時間を割く必要があり，当初予定していた状態爆発抑制手法の開発に取り掛かれなかったことが進捗の遅れの理由であると考えている．2021年度では，対象とするプロトコルのモデル作成を主におこなっており，モデル完成に向けておおよその目処が立ったところである．

Strategy for Future Research Activity

本研究では，安全性の検証に用いられるツールであるProverifを用いて対象となる経路保証プロトコルの安全性検証を行う．そのために，モデル作成，検証時の状態爆発抑制手法，状態爆発抑制手法適用時の経路保証アルゴリズムの改良が必要である．
モデル作成については，完成の目処が立っており，研究代表者は，状態爆発抑制手法の開発に着手し，2022年度中の完成を目指す．合わせて，研究分担者は，経路保証アルゴリズムの改良に着手する．これらの開発や改良を進めることで，国際会議などに投稿を行う予定である．
また，2023年度では，それらの成果をまとめて論文誌に投稿を行う予定である．

Causes of Carryover

2021年度では，コロナ対策関連の業務に時間を割く必要があり，状態爆発の抑制を行う手法を進めることが難しかったため，論文投稿の進捗が芳しくなく，参加費の使用が想定より少なかった．また，社会情勢を鑑みて研究会や国際会議がオンラインで開催されたため，旅費を使用する機会がなかったためと考えられる．2022年度では，状況が改善されることを想定しており，その際には現地での発表を行うことを考えているため，旅費の使用機会が生じると考えられる．繰り越しの多くが旅費であるため，積極的に投稿を行い，現地での発表回数を増加させることを考えている．