• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 課題ページに戻る

2014 年度 実施状況報告書

セキュリティプロトコルの時間匿名性に対する形式検証法の研究

研究課題

研究課題/領域番号 26330166
研究機関愛知工業大学

研究代表者

河辺 義信  愛知工業大学, 情報科学部, 准教授 (80396184)

研究分担者 伊藤 暢浩  愛知工業大学, 情報科学部, 准教授 (40314075)
研究期間 (年度) 2014-04-01 – 2017-03-31
キーワード匿名性 / 実時間システム / 時間匿名性 / 形式検証 / セキュリティプロトコル
研究実績の概要

従来,プログラム理論やソフトウェア工学の分野においては,ソフトウェアの正しさを論理的に検証する手法(形式手法,数理的技法,あるいはフォーマルメソッドなどと呼ばれる)が研究されており,当該研究分野の中心テーマのひとつとなっている.なかでも,暗号プロトコルを対象とした形式手法とした世界的な注目を集めており,秘匿性(盗聴した暗号文をどのように組み合わせても平文を取り出すことができないこと)などが研究されている.
本研究では,スマートフォン,ロボット,車載ソフトウェア等のいわゆる実時間システムに対する匿名性(「誰がやったのかがわからない」ことを示す,プライバシの基本的な性質),すなわち時間匿名性を対象とし,そのモデル化と効率的な検証手法の開発を行うことで,安全・安心なICT社会の構築に貢献することを目指している.初年度である平成26年度では,どのような時間匿名性の定義を行えば妥当なものになるのかを検討するため,まずは例題ベースに実時間システムの具体的なモデル化を行った.例題としては,車載ソフトウェアの一種であるエンジン制御ユニットの動作をI/Oオートマトンモデルを用いて記述した.この記述は通常のI/Oオートマトンモデルに時間パラメータを導入する形で行われた.すなわち,従来の匿名性検証手法が直接適用可能な形となっている.一方で,災害救助ロボットの制御アルゴリズムを検討するロボカップレスキューの分野や,モデルカーAIの分野を対象とした,いくつかのモデル化実験を行った.これらは限られた時間内に目標(ロボカップレスキューであれば人命救助,あるいは,モデルカーAIであればモーター制御)を行わなければならず,実時間システムの典型例と言える.これらのモデル化を通して,今後の時間匿名性の自動検証技術の構築に向けての基礎実験を完了することができた.

現在までの達成度 (区分)
現在までの達成度 (区分)

2: おおむね順調に進展している

理由

今年度は,比較的取り組みやすいと考えられるテーマとして,どのような時間匿名性の定義を行えば妥当なものになるのかを検討するため,具体的な例題をいくつか用意して,それらのモデル化実験を行ったことになる.その中で我々は,従来型のI/Oオートマトンモデルに時間パラメータを加えた形でのモデル化を行う形式化を試みた.当初計画では,時間I/Oオートマトンモデルによる定式化と検証手法を考案することを検討しているが,従来型のI/Oオートマトンモデルに基づく別の有力な方向性(時間匿名性の形式化と,従来から存在する検証ツールを利用した効率的な検証)もありうることが検討できたと考えている.また,ロボカップレスキューの分野や,モデルカーAIの分野を対象とした,いくつかのモデル化実験を行うことができた.なお,今年度は,確率版のI/Oオートマトンモデルではなく,非決定版のI/Oオートマトンモデルに基づいて,モデル化実験を行っている.

今後の研究の推進方策

今後は,今年度に検討したシステムに対するモデル化やその他のセキュリティプロトコル,分散システム,あるいは分散アルゴリズム(実時間システム)を対象として,効率的な匿名性の検証法や検証実験を行っていきたい.また,今年度は通常のI/Oオートマトンモデルを出発点としたモデル化実験を行ったことになるが,当初計画にある時間I/Oオートマトンモデルに基づくモデル化や,両モデルの間の関係を検討することも,課題としては考えられる.
上記の検討課題などを通じて,形式検証ツールを用いた効率的な時間匿名性の検証技術がどのようなものになるかを,明らかにしてゆきたい.

次年度使用額が生じた理由

「旅費」「人件費・謝金」「その他」については,ほぼ当初計画通りの使用となっている.一方,「物品費」については,当初計画していた実験用コンピュータの購入について販売日の変更が生じたため,未使用となった.この金額が次年度使用額として出ている.

次年度使用額の使用計画

準備ができ次第,実験用コンピュータ購入をすすめたい.

  • 研究成果

    (5件)

すべて 2015 2014

すべて 学会発表 (5件)

  • [学会発表] Robust Location Tracking Method for Mixed Reality Robots using a Rotation Search Method2015

    • 著者名/発表者名
      Masahiro Yamamoto, Kazuhiro Suzuki, Ryosuke Ogawa, Nobuhiro Ito, Yoshinobu Kawabe
    • 学会等名
      14th IEEE/ACIS International Conference on Computer and Information Science
    • 発表場所
      Las Vegas(米国)
    • 年月日
      2015-06-28 – 2015-07-01
  • [学会発表] IOA に基づく実行可能仕様のための変換系の試作2014

    • 著者名/発表者名
      吉政徳晃,河辺義信
    • 学会等名
      第12回情報学ワークショップ (WiNF 2014)
    • 発表場所
      静岡大学浜松キャンパス(静岡県浜松市)
    • 年月日
      2014-11-29
  • [学会発表] センサーと無線モジュールを使ったデータ取得とデータ解析によるコースレイアウトの導出2014

    • 著者名/発表者名
      岡島侑大,菅谷晃宏,河辺義信
    • 学会等名
      人工知能学会 社会におけるAI 第20回 研究会
    • 発表場所
      愛知工業大学自由ヶ丘キャンパス(愛知県名古屋市)
    • 年月日
      2014-11-08 – 2014-11-09
  • [学会発表] Toward Formal Verification of ECU for Gasoline Direct Injection Engines2014

    • 著者名/発表者名
      Masato Yamauchi, Nobuhiro Ito and Yoshinobu Kawabe
    • 学会等名
      IIAI 3rd International Conference on Advanced Applied Informatics
    • 発表場所
      北九州国際会議場(福岡県北九州市)
    • 年月日
      2014-08-31 – 2014-09-04
  • [学会発表] IOA仕様から関数型言語Erlangへの自動変換2014

    • 著者名/発表者名
      吉政徳晃,河辺義信
    • 学会等名
      日本知能情報ファジィ学会 第37回東海ファジィ研究会
    • 発表場所
      蒲郡市生命の海科学館・蒲郡情報ネットワークセンター(愛知県蒲郡市)
    • 年月日
      2014-08-03 – 2014-08-04

URL: 

公開日: 2016-05-27  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi