Developing Automated formal Verification System for Cryptology
| Project/Area Number |
17K00182
|
|---|
| Research Category |
Grant-in-Aid for Scientific Research (C)
|
| Allocation Type | Multi-year Fund |
|---|
| Section | 一般 |
|---|
| Research Field |
Information security
|
|---|
| Research Institution | Shinshu University |
|---|
Principal Investigator |
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
布田 裕一 東京工科大学, コンピュータサイエンス学部, 准教授 (50706223)
師玉 康成 信州大学, 学術研究院工学系, 教授 (20226129)
荒井 研一 長崎大学, 工学研究科, 助教 (60645290)
|
|---|
| Project Period (FY) |
2017-04-01 – 2021-03-31
|
| Project Status |
Completed (Fiscal Year 2020)
|
| Budget Amount *help |
¥4,550,000 (Direct Cost: ¥3,500,000、Indirect Cost: ¥1,050,000)
Fiscal Year 2020: ¥1,040,000 (Direct Cost: ¥800,000、Indirect Cost: ¥240,000)
Fiscal Year 2019: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2018: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
Fiscal Year 2017: ¥1,170,000 (Direct Cost: ¥900,000、Indirect Cost: ¥270,000)
|
|---|
| Keywords | 暗号理論 / 形式的安全性検証 / 形式的定理証明 / モデル検査 / Mizar / ProVerif / 形式検証 / 安全性証明 / 暗号システム / アルゴリズムの計算量形式化 / 安全性要件形式化 / 繰り返しおよび再帰形式化 / 統計的識別不能性形式化 / アルゴリズムのステップ数形式化 / 攻撃モデル形式化 / 暗号・認証等 / 応用数学 |
|---|
| Outline of Final Research Achievements |
In this research, we developed a practical computer-assisted formal verification system for security of cryptographic systems using a formal theorem prover Mizar and a security model checker ProVerif. By using Mizar, we has developed formalized mathematical library related to cryptology. Since this result is a formalization of the basics of computer science such as probability, statistics, functional analysis, calculation algorithms and computational complexity, it can be applied to other than cryptology. On the other hand, by using ProVerif, we proposed a security verification method not only for basic cryptographic protocols but also for models suit for actual systems and implementations. Our proposed method has made it possible to provide design support and formal security verification during development of actual cryptographic modules such as cryptographic hash functions and block cipher modes of operation.
|
| Academic Significance and Societal Importance of the Research Achievements |
本研究では、形式的定理証明系Mizarとモデル検査器ProVerifを用いて、実用的な計算機援用による暗号システムの安全性形式的評価システムの開発を行った。前者は主に暗号理論の専門家が安全性証明を行う際に、証明の正しさを計算機によって検証することに利用できる。後者は暗号理論の専門家ではないネットワークやIoT技術のような暗号技術の利用者が、セキュアなシステム開発の際に、正しく暗号技術を利用するための支援や暗号技術の学習に利用でき、いずれもSociety5.0の発展に貢献できるものである。
|
Report
(5 results)
Research Products
(30 results)
