2018 Fiscal Year Research-status 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)
荒井 研一 長崎大学, 工学研究科, 助教 (60645290)
|
|---|
| Project Period (FY) |
2017-04-01 – 2021-03-31
|
| Keywords | アルゴリズムのステップ数形式化 / 安全性要件形式化 / 攻撃モデル形式化 |
|---|
| Outline of Annual Research Achievements |
暗号の安全性を形式的定理証明検証や形式的自動証明等の計算機援用による形式的評価を用いて行う試みが注目を集めている。本研究では、形式的定理証明系Mizar等を用いて、特定のモデルや証明方法に依存しない、汎用性の高い暗号理論に関わる基礎的な形式化数学ライブラリを開発することで、実用的な計算機援用による暗号システムの安全性形式的評価システムの開発を目的とする。平成30年度は平成29年度に引き続き(1)暗号理論で必要となる数学、および計算機科学に関する形式化ライブラリ開発、(2)暗号プリミティブ、暗号システムに関する形式化を行った。
(1)については平成29年度の成果をさらに発展させ、確率論形式化の礎となる関数のリプシッツ連続性に関する形式化数学ライブラリを開発し、査読付き論文として公開した。また、平成29年度に検討したアルゴリズムと計算量の評価、計算問題間の帰着関係の形式化のための形式化数学ライブラリを開発し、査読付き論文として公開した。具体的には単純なループ構造によるアルゴリズム（ユークリッド互除法や高速べき乗剰余演算）の形式化と繰り返しステップ数の評価に関する形式化を行った。また、高速べき乗剰余演算アルゴリズム等を記述するために整数のバイナリ表現に関する形式化数学ライブラリを開発した。
(2)については平成29年度に引き続き暗号プロトコルの安全性自動検証ツールであるProVerifでの暗号機能の形式化をさらに進め国際会議、および国内会議で発表を行った。さらにその成果の一部を利用した暗号プロトコルに関する教育の試みが、第5回 実践的IT教育シンポジウム rePiT2019 in 愛媛（ソフトウェア科学会、enPit2共催）において優秀教育実践賞を受賞した。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
平成30年度は(1)暗号理論で必要となる数学、および計算機科学に関する形式化ライブラリ開発、についてはユークリッド互除法や高速べき乗剰余演算の形式化とステップ数の評価に関する形式化を行った（ただし査読期間の都合上令和元年度の成果として採録予定である）。この形式化手法は前述のアルゴリズムに限らず単純なループ構造のアルゴリズムであれば適用可能である事を確認している。さらに本研究課題遂行において非常に重要な課題である確率分布の統計的識別不能性の形式化方針が確定し、令和元年度に向けて形式化数学ライブラリ開発を進めている。
(2)暗号プリミティブ、暗号システムに関する形式化については暗号プロトコルの安全性自動検証ツールであるProVerifにおける安全性要件や攻撃モデルの形式化についての提案を行い、国際会議等で発表した。ProVerifでは元々サポートされていないループ構造や再起呼び出しを含むプロトコルを内部プロセス間の通信として扱うことによって形式モデル化を行い、マークル木やチェイン構造等の検証を行う方法を提案した。このモデル化方法を利用して、暗号学的ハッシュ関数の構成法であるMD変換や、ブロック暗号の利用モードなどの形式化を実現した。ProVerifは本来理想的な暗号モジュールを用いた構成させた暗号プロトコルの安全性を検証するツールであるが、具体的な暗号モジュールの構成法の安全性検証にも応用可能であることを示唆したことは大きな成果である。
|
| Strategy for Future Research Activity |
(1)暗号理論で必要となる数学、および計算機科学に関する形式化ライブラリ開発、については当初の計画通り暗号理論の基礎となる数学、および計算機科学に関する形式化ライブラリの開発を進める。令和元年度は特に、確率分布の統計的識別不能性の形式化数学ライブラリの完成を目指す。既に開発済である確率分布や確率変数、および無視可能関数に関する形式化ライブラリを利用して2つの確率変数、あるいは標本が同じ分布の母集合に属することを形式化する。この際に確率変数、あるいは標本間に距離尺度を導入する必要があるが、これに統計学、特にノンパラメトリック検定の統計量を採用する。我々の知る限り統計的識別不能性の定義にはインフォーマルな部分が含まれるものしか知られていないので、本テーマは単なる形式化ライブラリ開発だけにとどまらず統計的識別不能性の厳格な定義の提案を行うことになる。
また、計算量評価のためのアルゴリズム形式化については、単純なループだけでなく分岐や再帰等を含むアルゴリズムの形式化を平成30年度の成果を基として進めていく。これには節点の要素として上述の単純なループを持つような木構造として形式化を行う予定である。
(2)暗号プリミティブ、暗号システムに関する形式化については平成30年度の成果を基にしてＭＤ変換以外の具体的な暗号モジュールの形式モデル化および、それらのモデルを利用した暗号モジュールの安全性検証、さらには新たな暗号モジュールの設計支援を試みる予定である。
|
| Causes of Carryover |
【次年度使用額が生じた理由】信州大学にて購入予定であった計算機が、学科管理計算機のリプレイスにより岡崎、師玉の所属する研究室に移管された計算機で代用できたため。
【使用計画】既に国際会議発表が1件決定しており、それを含めた旅費などに充てる。
|
