2020 Fiscal Year Annual Research Report
Developing Automated formal Verification System for Cryptology
| Project/Area Number |
17K00182
|
|---|
| Research Institution | Shinshu University |
|---|
Principal Investigator |
岡崎 裕之 信州大学, 学術研究院工学系, 助教 (50432167)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
布田 裕一 東京工科大学, コンピュータサイエンス学部, 准教授 (50706223)
師玉 康成 信州大学, 学術研究院工学系, 教授 (20226129) [Withdrawn]
荒井 研一 長崎大学, 工学研究科, 助教 (60645290)
|
|---|
| Project Period (FY) |
2017-04-01 – 2021-03-31
|
| Keywords | 形式検証 / 安全性証明 / 暗号システム / Mizar / ProVerif |
|---|
| Outline of Annual Research Achievements |
形式検証技術を応用した暗号システムの自動安全性評価技術に関する研究を行った。Society ５.０実現の為に暗号技術は必要不可欠であり、利用用途の幅、および社会の依存度が今後ますます増加していくと予想されるが、暗号技術に精通した技術者は不足している。そこで計算機援用による暗号技術を利用したシステムやプロトコルの設計および安全性検証を支援するツールの開発とその普及は有意義である。
特に繰り返しや関数呼び出しを含む暗号モジュールの実装技術の安全性検証方法に関する提案、評価を行った。ProVerifをはじめとするモデル探索による暗号プロトコル安全性検証ツールでは、前述のような抽象度の低い実装に即した安全性検証を行うことは困難であったが、本研究で提案した検証手法により、暗号学的ハッシュ関数の構成法として知られるMD変換やスポンジ構造、さらにはCBCモードに代表される秘密鍵暗号の利用モード等の形式モデル化と安全性検証に関する報告を行った。
一方で、定理証明支援システムMizarを用いた暗号の安全性証明自動検証システムの開発も継続して進めており、攻撃成功確率等の評価の為に逆関数に関する諸定理の形式化数学ライブラリを開発した。
さらに暗号システム以外の安全性検証へ本研究の応用範囲を広げるために、ネットワークセキュリティ分野においても学内および学外の研究者との共同研究を進めている。
なお、本研究の成果の一部は民間企業との共同研究でIoT機器を利用したセキュアなシステム設計に特化した安全性検証支援ツールとしての実用化を進めている。
|
