Logical foundation and formal verification of quantum-resistant security protocols

• 研究課題/領域番号: 24KK0185
• 研究種目: 国際共同研究加速基金(海外連携研究)
• 配分区分: 基金
• 審査区分: 中区分60:情報科学、情報工学およびその関連分野
• 研究機関: 北陸先端科学技術大学院大学
• 研究代表者: 緒方 和博 北陸先端科学技術大学院大学, 先端科学技術研究科, 教授 (30272991)
• 研究分担者: DO CanhMinh 北陸先端科学技術大学院大学, 先端科学技術研究科, 助教 (00981143) ; 高木 翼 北陸先端科学技術大学院大学, 先端科学技術研究科, 准教授 (30994769)
• 研究期間 (年度): 2024-09-09 – 2028-03-31
• 研究課題ステータス: 交付 (2024年度)
• 配分額: 20,930千円 (直接経費: 16,100千円、間接経費: 4,830千円); 2027年度: 5,330千円 (直接経費: 4,100千円、間接経費: 1,230千円); 2026年度: 5,330千円 (直接経費: 4,100千円、間接経費: 1,230千円); 2025年度: 5,330千円 (直接経費: 4,100千円、間接経費: 1,230千円); 2024年度: 4,940千円 (直接経費: 3,800千円、間接経費: 1,140千円)
• キーワード: 形式検証 / サイバーセキュリティ / セキュリティプロトコル / 耐量子 / 量子通信

研究開始時の研究の概要

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