| 研究課題/領域番号 |
17K00182
|
|---|
| 研究種目 |
基盤研究(C)
|
| 配分区分 | 基金 |
|---|
| 応募区分 | 一般 |
|---|
| 研究分野 |
情報セキュリティ
|
|---|
| 研究機関 | 信州大学 |
|---|
研究代表者 |
岡崎 裕之 信州大学, 学術研究院工学系, 助教 (50432167)
|
|---|
| 研究分担者 |
布田 裕一 東京工科大学, コンピュータサイエンス学部, 准教授 (50706223)
師玉 康成 信州大学, 学術研究院工学系, 教授 (20226129)
荒井 研一 長崎大学, 工学研究科, 助教 (60645290)
|
|---|
| 研究期間 (年度) |
2017-04-01 – 2021-03-31
|
| 研究課題ステータス |
完了 (2020年度)
|
| 配分額 *注記 |
4,550千円 (直接経費: 3,500千円、間接経費: 1,050千円)
2020年度: 1,040千円 (直接経費: 800千円、間接経費: 240千円)
2019年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)
2018年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)
2017年度: 1,170千円 (直接経費: 900千円、間接経費: 270千円)
|
|---|
| キーワード | 暗号理論 / 形式的安全性検証 / 形式的定理証明 / モデル検査 / Mizar / ProVerif / 形式検証 / 安全性証明 / 暗号システム / アルゴリズムの計算量形式化 / 安全性要件形式化 / 繰り返しおよび再帰形式化 / 統計的識別不能性形式化 / アルゴリズムのステップ数形式化 / 攻撃モデル形式化 / 暗号・認証等 / 応用数学 |
|---|
| 研究成果の概要 |
本研究では、形式的定理証明系Mizarとモデル検査器ProVerifを用いて、計算機援用による暗号システムの安全性形式的評価システムを開発した。
Mizarでは暗号理論に関わる形式化数学ライブラリを開発した。本成果は確率、統計、関数解析、計算アルゴリズムや計算量等の計算機科学の基礎の形式化であるので、暗号理論以外にも応用できる。
一方、ProVerifでは、基本的な暗号プロトコルのみならず、従来より抽象度が低くより現実のシステムや実装に近いモデルでの安全性検証手法を提案した。これにより暗号学的ハッシュ関数やブロック暗号の利用モード等の開発時の設計支援や形式的安全性検証を行うことが可能となった。
|
| 研究成果の学術的意義や社会的意義 |
本研究では、形式的定理証明系Mizarとモデル検査器ProVerifを用いて、実用的な計算機援用による暗号システムの安全性形式的評価システムの開発を行った。前者は主に暗号理論の専門家が安全性証明を行う際に、証明の正しさを計算機によって検証することに利用できる。後者は暗号理論の専門家ではないネットワークやIoT技術のような暗号技術の利用者が、セキュアなシステム開発の際に、正しく暗号技術を利用するための支援や暗号技術の学習に利用でき、いずれもSociety5.0の発展に貢献できるものである。
|
