Developing Automated formal Verification System for Cryptology

2020 Fiscal Year Final Research Report

• 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: Okazaki Hiroyuki 信州大学, 学術研究院工学系, 助教 (50432167)
• Co-Investigator(Kenkyū-buntansha): 布田 裕一 東京工科大学, コンピュータサイエンス学部, 准教授 (50706223) ; 師玉 康成 信州大学, 学術研究院工学系, 教授 (20226129) ; 荒井 研一 長崎大学, 工学研究科, 助教 (60645290)
• Project Period (FY): 2017-04-01 – 2021-03-31
• 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.

Free Research Field

情報セキュリティ

Academic Significance and Societal Importance of the Research Achievements

本研究では、形式的定理証明系Mizarとモデル検査器ProVerifを用いて、実用的な計算機援用による暗号システムの安全性形式的評価システムの開発を行った。前者は主に暗号理論の専門家が安全性証明を行う際に、証明の正しさを計算機によって検証することに利用できる。後者は暗号理論の専門家ではないネットワークやIoT技術のような暗号技術の利用者が、セキュアなシステム開発の際に、正しく暗号技術を利用するための支援や暗号技術の学習に利用でき、いずれもSociety5.0の発展に貢献できるものである。