2017 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 |
暗号の安全性を形式的定理証明検証や形式的自動証明等の計算機援用による形式的評価を用いて行う試みが注目を集めている。暗号プロトコルの安全性評価に関する国際規格ISO/IEC 29128では、高いセキュリティレベルを保障するためには形式的評価を行うことが求められている。本研究では、形式的定理証明系Mizar等を用いて、特定のモデルや証明方法に依存しない、汎用性の高い暗号理論に関わる基礎的な形式化数学ライブラリを開発することで、実用的な計算機援用による暗号システムの安全性形式的評価システムの開発を目的とする。平成29年度は(1)暗号理論で必要となる数学、および計算機科学に関する形式化ライブラリ開発、(2)暗号プリミティブ、暗号システムに関する形式化を行った。
(1)については確率論の形式化を進めるための礎となる関数のリプシッツ連続性に関する形式化数学ライブラリを開発し、査読付き論文として公開した。また、アルゴリズムと計算量の評価、計算問題間の帰着関係の形式化のために、アルゴリズムの動作を形式的に記述し、計算量を評価する方法を検討した。具体的には、木構造を用いたアルゴリズムの中間値の動きを表現し、中間値のエッジを数え上げることで計算量を見積もる方法を検討した。
(2)については平成30年度より行う予定であった、暗号プロトコルの安全性自動検証ツールである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
平成29年度の当初目的は(1)暗号理論で必要となる数学、および計算機科学に関する形式化ライブラリ開発、については確率論、確率的関数の形式化を進める事であったが、関数の連続性に関する形式化ライブラリの開発が進んでいる。関数の連続性については確率論のみならず、安全性評価の際に必要となる関数間の距離の形式についても必要となる為本研究課題遂行において非常に有用である。
(2)暗号プリミティブ、暗号システムに関する形式化については当初計画では平成30年度より行う予定であった、暗号プロトコルの安全性自動検証ツールであるProVerifでの形式化の計画を前倒して先行させたが、ProVerifにおける攻撃モデルの形式化や、特にブロックチェーン技術の形式化の際に困難であると予想していた再帰的実行に関する形式化の実現方法を提案出来たことは大きな成果である。
|
| Strategy for Future Research Activity |
当初の計画通り暗号理論の基礎となる数学、および計算機科学に関する形式化ライブラリの開発を進める。平成30年度は特に、平成29年度の成果で述べた検討結果に基づいて、アルゴリズムの形式化、計算量評価の形式化を重点的に進める。また、暗号プロトコルの安全性自動検証ツールProVerifにおける暗号プロトコルの形式化成果との連携を進めていく予定である。
|
| Causes of Carryover |
発表予定国際会議の変更に伴い旅費、参加費等の使用予定が年度をまたいでしまったため。
未使用分は研究計画を当初予定と変更し次年度に開催される国際会議の参加資金に充てる。
本年度分の使用計画は当初計画の通り執行する予定である。
|
