Computational Logical Verification Method for Cryptographic Protocols

• Project/Area Number: 21700023
• Research Category: Grant-in-Aid for Young Scientists (B)
• Allocation Type: Single-year Grants
• Research Field: Software
• Research Institution: University of Tsukuba
• Principal Investigator: HASEBE Koji 筑波大学, システム情報系, 助教 (80470045)
• Project Period (FY): 2009 – 2011
• Project Status: Completed (Fiscal Year 2011)
• Budget Amount: ¥4,420,000 (Direct Cost: ¥3,400,000、Indirect Cost: ¥1,020,000); Fiscal Year 2011: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000); Fiscal Year 2010: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000); Fiscal Year 2009: ¥2,080,000 (Direct Cost: ¥1,600,000、Indirect Cost: ¥480,000)
• Keywords: 仕様記述 / 仕様検証 / 形式手法 / 暗号プロトコル / 安全性検証 / 論理推論 / 計算論的安全性 / 数理的技法 / 計算論的安全性証明

Research Abstract

We developed an extended inference system based on Based Protocol Logic (BPL), a variant of first order logic for proving correctness of cryptographic protocols. This extended system was obtained from BPL by adding some computational aspects of cryptography and sound with respect to a computational semantics. We also demonstrated the usefulness of this system by proving secrecy property of some protocols, such as Needham-Schroeder protocol.

Research Products

• [Presentation] 計算論的に健全な一階述語論理による暗号プロトコルの分析 (2012)
  • Author(s): Gergely Bana, 長谷部浩二, 岡田光弘
  • Organizer: 推理的技法による情報セキュリティ
  • Place of Presentation: 九州大学(福岡県)
  • Year and Date: 2012-03-08
• [Presentation] 計算論的に健全な一階述語論理による暗号プロトコルの分析 (2012)
  • Author(s): Gergely Bana, 長谷部浩二, 岡田光弘
  • Organizer: 数理的技法による情報セキュリティ
  • Place of Presentation: 九州大学(福岡県)
  • Year and Date: 2012-03-08
• [Presentation] Secrecy-Oriented Computationally Sound First-Order Logical Aanlysis of Cryptographic Protocols (2010)
  • Author(s): Gergely Bana, Koji Hasebe, Mitsuhiro Okada
  • Organizer: 6th Workshop on Formal and Computational Cryptography
  • Place of Presentation: Edinburgh, UK
  • Year and Date: 2010-07-20
• [Presentation] Secrecy-Oriented, Computationally Sound First-Order Logical Analysis of Cryptographic Protocols (2010)
  • Author(s): Gergely Bana, Koji Hasebe, Mitsuhiro Okada
  • Organizer: 6th Workshop on Formal and Computational Cryptography
  • Place of Presentation: Edinburgh, UK
  • Year and Date: 2010-07-20
• [Presentation] Recent approaches to computational semantics for first-order logical analysis of cryptographic protocols (2009)
  • Author(s): Gergely Bana, Koji Hasebe, Mitsuhiro Okada
  • Organizer: Computational and Symbolic Proofs of Security
  • Place of Presentation: 熱川ハイツ(静岡県)
  • Year and Date: 2009-04-09
• [Book] 数理的技法による情報セキュリティ (2010)
  • Author(s): 長谷部浩二, 岡田光弘, バナ・ゲルゲイ
• [Book] 「セキュリティ・プロトコルの論理的検証法」(萩谷・塚田共編『数理的技法による情報セキュリティ』第9章 (2010)
  • Author(s): 長谷部浩二, 岡田光弘, バナ・ゲルゲイ
  • Publisher: 共立出版
• [Remarks]
  • URL: http://www.cs.tsukuba.ac.jp/~hasebe/