| 研究課題/領域番号 |
23700024
|
|---|
| 研究機関 | 愛知工業大学 |
|---|
研究代表者 |
河辺 義信 愛知工業大学, 情報科学部, 准教授 (80396184)
|
|---|
| キーワード | プライバシ / 形式検証 / 定理証明 / セキュリティプロトコル |
|---|
| 研究概要 |
従来，プログラム理論やソフトウェア工学の分野においては，ソフトウェアの正しさを論理的に検証する手法（形式手法，数理的技法とも呼ばれる）が研究されており，当該分野の中心テーマの一つとなっている．なかでも，暗号プロトコルを対象とした形式手法が世界的な注目を集めており，秘匿性（盗聴した暗号文をどのように組み合わせても平文を取り出せないこと）などが研究されている．
本研究では，セキュリティの重要な性質である「プライバシ」を，形式手法を用いて自動検証する技術を確立することで，安全・安心なICT社会の構築に貢献することを目指している．本年度は，匿名通信路（Mixnet，Onion routingなどが有名）のうち，Crowdsと呼ばれる匿名ウェブアクセスシステムを対象としたプライバシ検証を行った．具体的には，前年度からすすめていた形式化（分散アルゴリズムの理論として知られるI/O-オートマトンの上で定式化）をもとにして，定理証明ソフトウェアを用いた検証を実施した．Crowdsでは，ある種のコンピュータウィルスに感染した状態（「corrupt」と呼ばれる）に陥ったルータまでも考慮する必要がある．そのような状況を考慮した上で，Crowdsシステムのプライバシ（送信者・受信者が外部にわからないこと）を自動検証することができた．
なお，上記の検証実験においては定理証明ソフトウェアを用いているが，これはユーザの判断を必要とする半自動の検証である．これに対し，SATソルバを用いた全自動の検証も考えられる．これについて，今年度は，Alloyと呼ばれるSATソルバ上にI/O-オートマトン理論のフォワードシミュレーション手法を実装し，自動検証を試みた．本研究で用いるプライバシ検証手法はフォワードシミュレーション手法の応用である．すなわち，プライバシ検証の全自動化に向けての基礎実験を完了できた．
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
プライバシに属する様々な性質（無証拠性，耐買収生，狭義のプライバシなど）は匿名性の一種とみなせることから，本研究では，既存の匿名性検証手法（研究代表者らは，システムの実行ステップ数に関する帰納法で匿名性を検証する手法を提案している）をプライバシの検証に適用することを目指している．
平成24年度は，Crowdsと呼ばれる匿名通信路の形式化をもとに，プライバシの検証実験を行った．これは，当初は平成25年度に計画していたものだが，今年度に先行して行ったものである．上記の検証実験は定理証明ソフトウェアを用いて行われたが，一方で，Alloyと呼ばれるSATソルバを用いたトレース包含の証明実験も行い，プライバシ検証の全自動化に向けた予備実験を行うことが出来た．
上記の状況から，研究はおおむね順調に進展したものと考える．
|
| 今後の研究の推進方策 |
今後は，他のセキュリティプロトコル，分散システム，あるいは分散アルゴリズムを題材とした形式モデリングや検証実験（事例研究）を引き続き続けてゆく方針である．さらには，これらの事例研究を通じて，プライバシ検証をする際に必要となる各種の前提条件を明らかにするとともに，効率的にプライバシを自動検証するための方法論を確立する．とくに，検証技術のツール上での実装方法を確立するとともに，検証されたプロトコルの実装技術についても明らかにしたい．
|
| 次年度の研究費の使用計画 |
最終年度にあたる次年度では，研究費は研究成果の発表等を行うための旅費・学会参加費・準備（論文の英文添削など）に使用する計画である．また，研究成果の発表やデモ実施に用いる計算機（主に，ノート型PC），および必要に応じて仮想化ソフトウェアなどの購入を計画している．
|
