形式手法に基づくセキュリティプロトコルの匿名性検証法に関する研究

• 研究課題/領域番号: 19700018
• 研究種目: 若手研究(B)
• 配分区分: 補助金
• 研究分野: 情報学基礎
• 研究機関: 愛知工業大学 (2008-2009); 日本電信電話株式会社NTTコミュニケーション科学基礎研究所 (2007)
• 研究代表者: 河辺 義信 愛知工業大学, 情報科学部, 准教授 (80396184)
• 研究期間 (年度): 2007 – 2009
• 研究課題ステータス: 完了 (2009年度)
• 配分額: 3,380千円 (直接経費: 2,900千円、間接経費: 480千円); 2009年度: 910千円 (直接経費: 700千円、間接経費: 210千円); 2008年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円); 2007年度: 1,300千円 (直接経費: 1,300千円)
• キーワード: 暗号系 / セキュリティ検証 / 匿名性 / フォーマルメソッド / 定理証明 / 形式検証 / I / O-オートマトン / 0-オートマトン

研究概要

本研究では,新たな匿名性の検証手法を提案した.この手法は,プログラム理論やソフトウェア工学の分野で注目を浴びる「形式手法」(数理的技法,フォーマルメソッドとも呼ばれる)を用いている.具体的には,匿名シミュレーション法と呼ばれる匿名性の証明法を,確率的匿名性や能動的攻撃者を許す場合にも扱えるように拡張した.さらに,Crowdsと呼ばれる通信ルータの匿名性やLee電子投票の「無証拠性(匿名性の拡張)」を検証した.

研究成果

• [雑誌論文] Probabilistic anomymity via coalgebraic simulations (2010)
  • 著者名/発表者名: Ichiro Hasuo, Yoshinobu Kawabe, Hideki Sakurada
  • 雑誌名: Theoretical Computer Science volume411,No.22-24 ページ: 2239-2259
  • 査読あり
• [雑誌論文] Probabilistic Anonymity via Coalgebraic Simulations (2010)
  • 著者名/発表者名: I.Hasuo, Y.Kawabe, H.Sakurada
  • 雑誌名: Theoretical Computer Science 411 ページ: 2239-2259
  • NAID: 120002511338
  • 査読あり
• [雑誌論文] On backward-style anonymity verification (2008)
  • 著者名/発表者名: Yoshinobu Kawabe, Ken Mano, Hideki Sakurada, Yasuyuki Tsukada
  • 雑誌名: IEICE Transactions volumeE91-A,No.9 ページ: 2597-2606
  • NAID: 10026851999
  • 査読あり
• [雑誌論文] An adversary model for simulation-based anonymity proof (2008)
  • 著者名/発表者名: Yoshinobu Kawabe, Hideki Sakurada
  • 雑誌名: IEICE Transactions volumeE91-A,No.4 ページ: 1112-1120
  • NAID: 10026848731
  • 査読あり
• [雑誌論文] On backward-style anonymity verification (2008)
  • 著者名/発表者名: Y. Kawabe, K. Mano, H. Sakurada, Y. Tsukada
  • 雑誌名: IEICE Trans. Vol.E91A, No.9 ページ: 2597-2606
  • NAID: 10026851999
  • 査読あり
• [雑誌論文] An adversary model for simulation-based anonymity proof (2008)
  • 著者名/発表者名: Y.Kawabe, H.Sakurada
  • 雑誌名: IEICE Trans. Vol.E91A,No.4 ページ: 1112-1120
  • NAID: 10026848731
  • 査読あり
• [学会発表] 無証拠的プロトコルのフォーマルな記述について (2009)
  • 著者名/発表者名: 河辺義信
  • 学会等名: 第21回電気関係学会東海支部連合大会
  • 発表場所: 愛知県豊田市
  • 年月日: 2009-09-11
• [学会発表] 無証拠的プロトコルのフォーマルな扱いについて (2009)
  • 著者名/発表者名: 河辺義信
  • 学会等名: 第21回 電気関係学会東海支部連合大会
  • 発表場所: 愛知工業大学
  • 年月日: 2009-09-10
• [学会発表] Anonymity, privacy, onymity and identity: a modal logic approach (2009)
  • 著者名/発表者名: Yasuyuki Tsukada, Ken Mano, Hideki Sakurada, Yoshinobu Kawabe
  • 学会等名: IEEE International Conference on Privacy, Security, Risk and Trust (PASSAT-09)
  • 発表場所: カナダ・バンクーバー市
  • 年月日: 2009-08-29
• [学会発表] I/O-オートマトンによる無証拠性の形式化について (2009)
  • 著者名/発表者名: 河辺義信, 真野健, 櫻田英樹, 塚田恭章
  • 学会等名: 電子情報通信学会2009年暗号と情報セキュリティシンポジウム
  • 発表場所: 滋賀県大津市
  • 年月日: 2009-01-23
• [学会発表] 1/0-オートマトンによる無証拠性の形式化について (2009)
  • 著者名/発表者名: 河辺, 真野, 櫻田, 塚田
  • 学会等名: 電子情報通信学会2009年暗号と情報セキュリティシンポジウム
  • 発表場所: 大津プリンスホテル(滋賀県大津市)
  • 年月日: 2009-01-23
• [学会発表] 匿名性・プライバシ・顕名性・アイデンティティへの知識論理的アプローチ (2008)
  • 著者名/発表者名: 塚田恭章, 真野健, 櫻田英樹, 河辺義信
  • 学会等名: 情報処理学会第11回コンピュータセキュリティシンポジウム
  • 発表場所: 沖縄県宜野湾市
  • 年月日: 2008-10-08
• [学会発表] 能動的な攻撃者が存在するシステムに対する匿名性の検証について (2008)
  • 著者名/発表者名: 河辺義信, 真野健, 櫻田英樹, 塚田恭章
  • 学会等名: 電子情報通信学会2008年暗号と情報セキュリティシンポジウム
  • 発表場所: 宮崎県宮崎市
  • 年月日: 2008-01-23
• [学会発表] 能動的な攻撃者が存在するシステムに対する匿名性の検証について (2008)
  • 著者名/発表者名: 河辺, 真野, 櫻田, 塚田
  • 学会等名: 電子情報通信学会2008年暗号と情報セキュリティシンポジウム
  • 発表場所: 宮崎シーガイアコンベンションセンター・サミット
  • 年月日: 2008-01-23
• [学会発表] A formal approach to designing anonymous software (2007)
  • 著者名/発表者名: Yoshinobu Kawabe, Hideki Sakurada
  • 学会等名: 5th International Conference on Software Engineering Research, Management and Applications (SERA '07)
  • 発表場所: 韓国釜山市
  • 年月日: 2007-08-21
• [学会発表] A formal approach to designing anonymous software (2007)
  • 著者名/発表者名: Y.Kawabe, H.Sakurada
  • 学会等名: 5th International Conference on Software Engineering Research, Management and Applications (SERA'07)
  • 発表場所: ヘウンデ・グランドホテル(韓国釜山市)
  • 年月日: 2007-08-21
• [学会発表] 攻撃者を考慮した匿名性検証法 (2007)
  • 著者名/発表者名: 河辺義信, 櫻田英樹
  • 学会等名: 電子情報通信学会第20回回路とシステム軽井沢ワークショップ
  • 発表場所: 長野県軽井沢町
  • 年月日: 2007-04-23
• [備考] 研究代表者のウェブページ. ここでは, Lee電子投票の無証拠性の証明スクリプト(バッチファイルのようなもの)を公開している. 用いた定理証明器は, LP(Larch Prover)である
  • URL: http://aitech.ac.jp/~kawabe/
• [備考]
  • URL: http://aitech.ac.jp/~kawabe/
• [備考]
  • URL: http://aitech.ac.jp/~kawabe/
• [備考]
  • URL: http://www.brl.ntt.co.jp/cs/ninri-g/security/index-j.html