2018 Fiscal Year Annual Research Report
Study on tamper-resistant software technology with theoretic security evaluation
| Project/Area Number |
15K00183
|
|---|
| Research Institution | Tokyo University of Technology |
|---|
Principal Investigator |
布田 裕一 東京工科大学, コンピュータサイエンス学部, 准教授 (50706223)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
宮地 充子 大阪大学, 工学研究科, 教授 (10313701)
CHEN Jiageng 北陸先端科学技術大学院大学, 情報科学研究科, 助教 (90640748) [Withdrawn]
|
|---|
| Project Period (FY) |
2015-04-01 – 2019-03-31
|
| Keywords | White-Box Cryptography / 耐タンパー技術 / 形式検証 / ProVerif |
|---|
| Outline of Annual Research Achievements |
White-Box Cryptography(以下でWBCと略記)技術は、プログラムや実行中のデータのすべてにアクセス可能な攻撃者に最も有利な状況においてもセキュリティを維持する技術であるため重要である。平成30年度は、1.AES暗号及び公開鍵暗号のWBC技術の方式案の検討及び2.WBC技術の安全性や計算量の評価における形式検証で必要な形式検証モデルの検討を実施した。
1に関しては、WBC技術に対する攻撃モデルとして、Gray-boxに近いもの (プログラム動作中の中間値の漏洩を制限したモデル)を引き続き検討した。また、WBC技術の対象となる共通鍵暗号の暗号解析を実施した。一方、WBC技術の対象となる公開鍵暗号では耐量子公開鍵暗号の性質が必須である。最終年度は有力な耐量子暗号の候補である符号ベースの暗号の解析も実施した。
2に関しては、処理フローをチェーンとみなした木構造を含めたモデルを、自動検証ツールProVerifにおいて検討した。WBC技術の計算量の評価を形式検証ツールMizarで検証するために、計算量の形式化を検討した。バイナリ法とユークリッドアルゴリズムの計算量評価を実施する形式化ライブラリを作成した。さらに、アルゴリズム中の分岐やサブルーチンコールの形式化方法を検討した。計算量評価のために、分岐及びサブルーチンを表現した木構造を用いる方法を検討した。WBC技術の安全性の形式検証のために、Mizarにおいて確率分布の識別不可能性の形式化を検討した。
補助事業期間全体を通じて、WBC技術の演算テーブルの識別不可能性を満たすために、テーブルの入出力関係が全単射である性質をなくす必要性を見出し、その方式モデルを考案した。識別不可能性の検証のため、ProVerifの観測等価性を利用したWBCの攻撃モデルの記述方法を検討した。さらに、WBC技術の対象となる暗号の解析を実施した。
|
