ブロックチェーン関連技術の形式的安全性検証に関する研究

• 研究課題/領域番号: 25K15110
• 研究種目: 基盤研究(C)
• 配分区分: 基金
• 応募区分: 一般
• 審査区分: 小区分60070:情報セキュリティ関連
• 研究機関: 信州大学
• 研究代表者: 岡崎 裕之 信州大学, 学術研究院工学系, 准教授 (50432167)
• 研究分担者: 布田 裕一 東京工科大学, コンピュータサイエンス学部, 教授 (50706223) ; 荒井 研一 長崎大学, 総合生産科学研究科(情報データ科学系), 准教授 (60645290)
• 研究期間 (年度): 2025-04-01 – 2029-03-31
• 研究課題ステータス: 交付 (2025年度)
• 配分額: 4,550千円 (直接経費: 3,500千円、間接経費: 1,050千円); 2028年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円); 2027年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円); 2026年度: 1,300千円 (直接経費: 1,000千円、間接経費: 300千円); 2025年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)
• キーワード: 形式手法 / 暗号理論 / 安全性検証 / ブロックチェーン / マルコフチェーン

研究開始時の研究の概要

ブロックチェーン関連技術の安全性評価技術の一つとして、計算機援用による形式的安全性検証が期待されている。本研究課題では、これまで形式化技法を駆使して複雑な暗号システムの形式的安全性検証の研究を行ってきた経験、およびその研究成果を用いて、①モデル検査器ProVerifによるブロックチェーンの形式モデル化と、その安全性要件の網羅探索による検証が終了可能な形式的安全性検証手法の開発、②形式的定理証明系Mizarによる前述の①の為の形式モデル化および、検証結果の妥当性、信頼性の形式的証明用数学ライブラリの開発を行い、ブロックチェーンを用いたアプリケーションの形式的安全性検証の実用化に貢献する。