2014 Fiscal Year Research-status Report
セキュリティプロトコルの時間匿名性に対する形式検証法の研究
| Project/Area Number |
26330166
|
|---|
| Research Institution | Aichi Institute of Technology |
|---|
Principal Investigator |
河辺 義信 愛知工業大学, 情報科学部, 准教授 (80396184)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
伊藤 暢浩 愛知工業大学, 情報科学部, 准教授 (40314075)
|
|---|
| Project Period (FY) |
2014-04-01 – 2017-03-31
|
| Keywords | 匿名性 / 実時間システム / 時間匿名性 / 形式検証 / セキュリティプロトコル |
|---|
| Outline of Annual Research Achievements |
従来，プログラム理論やソフトウェア工学の分野においては，ソフトウェアの正しさを論理的に検証する手法（形式手法，数理的技法，あるいはフォーマルメソッドなどと呼ばれる）が研究されており，当該研究分野の中心テーマのひとつとなっている．なかでも，暗号プロトコルを対象とした形式手法とした世界的な注目を集めており，秘匿性（盗聴した暗号文をどのように組み合わせても平文を取り出すことができないこと）などが研究されている．
本研究では，スマートフォン，ロボット，車載ソフトウェア等のいわゆる実時間システムに対する匿名性（「誰がやったのかがわからない」ことを示す，プライバシの基本的な性質），すなわち時間匿名性を対象とし，そのモデル化と効率的な検証手法の開発を行うことで，安全・安心なＩＣＴ社会の構築に貢献することを目指している．初年度である平成２６年度では，どのような時間匿名性の定義を行えば妥当なものになるのかを検討するため，まずは例題ベースに実時間システムの具体的なモデル化を行った．例題としては，車載ソフトウェアの一種であるエンジン制御ユニットの動作をＩ／Ｏオートマトンモデルを用いて記述した．この記述は通常のＩ／Ｏオートマトンモデルに時間パラメータを導入する形で行われた．すなわち，従来の匿名性検証手法が直接適用可能な形となっている．一方で，災害救助ロボットの制御アルゴリズムを検討するロボカップレスキューの分野や，モデルカーＡＩの分野を対象とした，いくつかのモデル化実験を行った．これらは限られた時間内に目標（ロボカップレスキューであれば人命救助，あるいは，モデルカーＡＩであればモーター制御）を行わなければならず，実時間システムの典型例と言える．これらのモデル化を通して，今後の時間匿名性の自動検証技術の構築に向けての基礎実験を完了することができた．
|
| Current Status of Research Progress |
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 |
「旅費」「人件費・謝金」「その他」については，ほぼ当初計画通りの使用となっている．一方，「物品費」については，当初計画していた実験用コンピュータの購入について販売日の変更が生じたため，未使用となった．この金額が次年度使用額として出ている．
|
| Expenditure Plan for Carryover Budget |
準備ができ次第，実験用コンピュータ購入をすすめたい．
|
