|
研究目的と研究実施計画に基づき、今年度はフェーズ2のフェイルセーフ安全性を持つ具体的な暗号プロトコルの構成に取り組んだ。成果として、フェイルセーフ安全性を持つ実用的な暗号プロトコルとして、動的マルチキャスト鍵配送について、フェイルセーフ安全性のモデル化と具体的方式の構成を行った。また、形式検証による安全性自動証明にも取り組み、グーグル社のブラウザ上で暗号化通信に用いられているQUICについて安全性解析を行い、従来の安全性モデルの不備を発見した。
動的マルチキャスト鍵配送のモデルでは、過去のセッション鍵・長期秘密鍵・短期秘密鍵・セッション中の内部状態が運用ミスなどによって漏洩したとしても、組み合わせ次第によっては、セッション鍵の秘匿性が保たれるように定式化した。方式では、暗号文ポリシー属性ベース暗号を利用することにより、セッション鍵や内部状態のアップデートを可能にしたため、一度長期秘密鍵が漏洩したとしても、一定の期間後には無効化され、安全な状態に復帰することができる。また、サーバを中心としたスタートポロジーのネットワーク構造を採用したため、各ユーザの通信量・計算量はユーザ数によらず、定数オーダーに抑えられることを示した。
QUICの検証では、QUICの仕様からプロトコルの動作を形式化し、検証ツールProVerifとAkissを用いて検証を行った結果、従来のモデルではモデルが強すぎるため、ある種の不可避のなりすまし攻撃が成立することを示した。
本研究で得られた成果について、国内研究会2件、国際会議2件で対外発表を行った。
|
