2019 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) [Withdrawn]
荒井 研一 長崎大学, 工学研究科, 助教 (60645290)
|
|---|
| Project Period (FY) |
2017-04-01 – 2021-03-31
|
| Keywords | アルゴリズムの計算量形式化 / 安全性要件形式化 / 繰り返しおよび再帰形式化 / 統計的識別不能性形式化 / 形式的安全性検証 |
|---|
| Outline of Annual Research Achievements |
暗号の安全性を形式的定理証明検証や形式的自動証明等の計算機援用による形式的評価を用いて行う試みが注目を集めている。本研究では、形式的定理証明系Mizar等を用いて、特定のモデルや証明方法に依存しない、汎用性の高い暗号理論に関わる基礎的な形式化数学ライブラリを開発することで、実用的な計算機援用による暗号システムの安全性形式的評価システムの開発を目的とする。令和元年度は平成30年度に引き続き(1)暗号理論で必要となる数学、および計算機科学に関する形式化ライブラリ開発、(2)モデル検査器による暗号プロトコルおよび暗号アルゴリズムに関する形式化を行った。
(1)については平成30年度の成果をさらに発展させ、確率論形式化の礎となる関数の微分可能性に関する形式化数学ライブラリを開発し、査読付き論文として公開した。また、平成30年度に進めていたアルゴリズムと計算量の評価の形式化のための形式化数学ライブラリ(単純ループ構造によるアルゴリズム)を行査読付き論文として公開した。さらに、暗号で利用されるより複雑なアルゴリズム評価の準備のために、アフィン座標上の楕円曲線演算に関する形式化数学ライブラリを開発し、査読付き論文として公開した。
(2)については平成30年度に引き続き暗号プロトコルの安全性自動検証ツールであるProVerifでの暗号機能の形式化をさらに進め国際会議、および国内会議で発表を行った。具体的にはProVerifでは通常形式記述することが出来ない動的な繰り返しや関数呼び出しを形式モデル化する方法を提案し、MD変換や秘密鍵暗号のラウンド処理の形式的安全性検証を実現した。
さらに平成30年度に国内会議rePiT2019 in 愛媛において優秀教育実践賞を受賞した、ProVerifを用いた暗号プロトコルに関する教育実践成果を査読付き論文として公開した。
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
令和元年度は(1)暗号理論で必要となる数学、および計算機科学に関する形式化ライブラリ開発、については確率論形式化の礎となる関数のリプシッツ連続性および陰関数の微分可能性に関する形式化、計算慮評価のための単純なループ構造のアルゴリズム形式化、楕円曲線暗号で用いられる有限体アフィン座標系上での演算についての形式化についてそれぞれ形式化数学ライブラリ開発し、順調に進展している。
ただし、本研究課題遂行において非常に重要な課題の一つである確率分布の統計的識別不能性の形式化については、形式化数学ライブラリ開発はほぼ終えているが、本成果は暗号の安全性検証のみならず人工知能やデータサイエンスへの応用も見込めることが判明した。そこで、これらの関連分野の理論的礎として注目され、さらに本研究課題との密接に関連する計算代数統計の諸定義、定理を今後形式化することを見越して、統計的識別不能性の形式化数学ライブラリを拡張することにしたため成果公表が若干遅れている。しかしながらこの拡張は、本研究成果を、今後も発展が見込まれるより広い研究分野へ貢献できるため有意義であると確信している。
(2)モデル検査器による暗号プロトコルおよび暗号アルゴリズムに関する形式化については暗号プロトコルの安全性自動検証ツールであるProVerifにおける具体的な暗号モジュールの構成法の安全性検証についての提案を行い、国際会議等で発表した。これは令和元年度に提案した形式化方法を応用して、より具体的な暗号システムの仕様や実装時の安全性検証にProVerifをはじめとするモデル検査器を利用する試みである。令和元年度は、平成30年度よりさらに抽象度を下げた、より実際の設計や実装時に近い形式モデルでの検証を実現し、順調に進展している。
|
| Strategy for Future Research Activity |
(1)暗号理論で必要となる数学、および計算機科学に関する形式化ライブラリ開発、については当初の計画通り暗号理論の基礎となる数学、および計算機科学に関する形式化ライブラリの開発を進める。令和2年度は特に、確率分布の統計的識別不能性の形式化数学ライブラリの完成を目指す。統計的識別不能性の形式化数学ライブラリそのものに関しては令和元年度当初の研究方針通りにほぼ完成しているが、統計学、特に計算統計代数分野の知見を取り込むために完成済の形式化ライブラリに修正を加えるとともに、今後の形式的安全性検証の発展に有用となる統計学・計算統計代数に関する形式化数学ライブラリの開発も併せて行う予定である。
また、計算量評価のためのアルゴリズム形式化については、令和元年度の成果を基として進めていく。令和元年度までに、計算アルゴリズムの最大ステップ数の形式化は実現しているが、ステップ毎の計算コストの見積もりを含めた計算量の形式化方法の検討を進め、形式化ライブラリの開発を行う予定である。
(2)モデル検査器による暗号プロトコルおよび暗号アルゴリズムに関する形式化については令和元度の成果を基にして具体的な暗号方式や暗号アルゴリズムの安全性検証を進める予定である。令和2年度は特に具体的な攻撃を回避するような設計・実装支援をProVerifをはじめとしたモデル検査器を用いて行う手法の提案を行う予定である。
|
| Causes of Carryover |
教員退職に伴う備品移管により購入予定であった計算機を確保できたこと、および感染症対策のために予定していた学会や研究打ち合わせ等の出張がキャンセルまたはオンライン開催となったため。
研究成果の公表のための国際会議投稿件数を当初予定より増やして旅費として使用することと、当初研究組織内で行う予定であった成果公表用パンフレットやWebサイト作成を外注する。
|
Research Products
(10 results)
