Study on Formal Security Verification of Blockchain-related Technologies

• Project/Area Number: 25K15110
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Multi-year Fund
• Section: 一般
• Review Section: Basic Section 60070:Information security-related
• Research Institution: Shinshu University
• Principal Investigator: 岡崎 裕之 信州大学, 学術研究院工学系, 准教授 (50432167)
• Co-Investigator(Kenkyū-buntansha): 布田 裕一 東京工科大学, コンピュータサイエンス学部, 教授 (50706223) ; 荒井 研一 長崎大学, 総合生産科学研究科(情報データ科学系), 准教授 (60645290)
• Project Period (FY): 2025-04-01 – 2029-03-31
• Project Status: Granted (Fiscal Year 2025)
• Budget Amount: ¥4,550,000 (Direct Cost: ¥3,500,000、Indirect Cost: ¥1,050,000); Fiscal Year 2028: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000); Fiscal Year 2027: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000); Fiscal Year 2026: ¥1,300,000 (Direct Cost: ¥1,000,000、Indirect Cost: ¥300,000); Fiscal Year 2025: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
• Keywords: 形式手法 / 暗号理論 / 安全性検証 / ブロックチェーン / マルコフチェーン

Outline of Research at the Start

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