論理推論を基にした暗号プロトコルの計算論的安全性検証法の構築

2011 年度 研究成果報告書

• 研究課題/領域番号: 21700023
• 研究種目: 若手研究(B)
• 配分区分: 補助金
• 研究分野: ソフトウエア
• 研究機関: 筑波大学
• 研究代表者: 長谷部 浩二 筑波大学, システム情報系, 助教 (80470045)
• 研究期間 (年度): 2009 – 2011
• キーワード: 仕様記述 / 仕様検証

研究概要

本研究を通じ, 研究代表者は先に提案されたBasic Protocol Logicと呼ばれる一階述語論理を拡張し, 暗号プロトコルの計算論的安全性を検証するための論理体系を構築した.これは, Basic Protocol Logicに対し, 確率暗号における計算論的概念を導入したものである.また, この論理体系が健全となるような計算論的意味論を与え, Needham-Schroederプロトコルなどの秘匿性証明に適用可能であることを示した.

研究成果

• [学会発表] 計算論的に健全な一階述語論理による暗号プロトコルの分析 (2012)
  • 著者名/発表者名: Gergely Bana, 長谷部浩二, 岡田光弘
  • 学会等名: 推理的技法による情報セキュリティ
  • 発表場所: 九州大学(福岡県)
  • 年月日: 2012-03-08
• [学会発表] Secrecy-Oriented Computationally Sound First-Order Logical Aanlysis of Cryptographic Protocols (2010)
  • 著者名/発表者名: Gergely Bana, Koji Hasebe, Mitsuhiro Okada
  • 学会等名: 6th Workshop on Formal and Computational Cryptography
  • 発表場所: Edinburgh, UK
  • 年月日: 2010-07-20
• [学会発表] Recent approaches to computational semantics for first-order logical analysis of cryptographic protocols (2009)
  • 著者名/発表者名: Gergely Bana, Koji Hasebe, Mitsuhiro Okada
  • 学会等名: Computational and Symbolic Proofs of Security
  • 発表場所: 熱川ハイツ(静岡県)
  • 年月日: 2009-04-09
• [図書] 数理的技法による情報セキュリティ (2010)
  • 著者名/発表者名: 長谷部浩二, 岡田光弘, バナ・ゲルゲイ
  • 総ページ数: 185-203
• [備考]
  • URL: http://www.cs.tsukuba.ac.jp/~hasebe/