|
H29年度の研究目的は、メッセージングサービスなどにおけるエンドツーエンド暗号化通信の初めての数理的モデル化と実用されている既存方式の分類学的な安全性評価である。研究実施計画に基づき、①攻撃パターンの網羅的分類、②形式手法に基づく記号論的安全性モデルの定式化、に取り組んだ。
特にエンドツーエンド暗号化通信の代表的な方式として、LINE encryptionを取り上げ、既知のなりすまし攻撃（spoofing）と再送攻撃（reply）を調査を行い、形式手法に基づく安全性を定式化した。定式化は一般的な中間者攻撃を捉えるため、Dolev-Yaoモデルに基づいて行った。さらに、長期鍵が漏れた後の安全性を保証するフォワード安全性についても、定式化を行った。
ホワイトペーパーを用いてLINE encryptionの仕様を調査し、定式化した記号論的安全性モデルを満たしているかの検証を行った。自動検証ツールとしては、扱える安全性の汎用性を考慮し、ProVerifを用いた。なりすまし攻撃、再送攻撃、フォワード安全性についてそれぞれ検証を行ったところ、なりすまし攻撃と再送攻撃については既知の攻撃を検出した。またフォワード安全性については、既存研究では明示的な攻撃は示されていなかったが、ProVerifにより新たな攻撃を発見した。
検証結果については、国内学会（暗号と情報セキュリティシンポジウム）で発表を行い、公知化した。
|
