Logical foundation and formal verification of quantum-resistant security protocols

• Project/Area Number: 24KK0185
• Research Category: Fund for the Promotion of Joint International Research (International Collaborative Research)
• Allocation Type: Multi-year Fund
• Review Section: Medium-sized Section 60:Information science, computer engineering, and related fields
• Research Institution: Japan Advanced Institute of Science and Technology
• Principal Investigator: 緒方 和博 北陸先端科学技術大学院大学, 先端科学技術研究科, 教授 (30272991)
• Co-Investigator(Kenkyū-buntansha): DO CanhMinh 北陸先端科学技術大学院大学, 先端科学技術研究科, 助教 (00981143) ; 高木 翼 北陸先端科学技術大学院大学, 先端科学技術研究科, 准教授 (30994769)
• Project Period (FY): 2024-09-09 – 2028-03-31
• Project Status: Granted (Fiscal Year 2024)
• Budget Amount: ¥20,930,000 (Direct Cost: ¥16,100,000、Indirect Cost: ¥4,830,000); Fiscal Year 2027: ¥5,330,000 (Direct Cost: ¥4,100,000、Indirect Cost: ¥1,230,000); Fiscal Year 2026: ¥5,330,000 (Direct Cost: ¥4,100,000、Indirect Cost: ¥1,230,000); Fiscal Year 2025: ¥5,330,000 (Direct Cost: ¥4,100,000、Indirect Cost: ¥1,230,000); Fiscal Year 2024: ¥4,940,000 (Direct Cost: ¥3,800,000、Indirect Cost: ¥1,140,000)
• Keywords: 形式検証 / サイバーセキュリティ / セキュリティプロトコル / 耐量子 / 量子通信

Outline of Research at the Start

Shorのアルゴリズムの考案により、量子時代には現在使用されている公開鍵暗号方式は安全でなくなることが知られている。それらを技術コンポーネントとして利用しているTLSなどのセキュリティプロトコルも安全でなくなる。この課題に対処するために、耐量子性セキュリティプロトコルが設計されている。本研究では、耐量子性セキュリティプロトコルの論理基盤の整備、そのようなプロトコルの形式検証技術の考案、考案した形式検証技術の支援ツールの作成を行う。