| 研究概要 |
暗号プロトコルの安全性自動検証手法APSGに基づく自動検証ツールCryptoVerifの証明能力を検証するために,ランダムオラクルからの情報漏洩をモデル化して,代表的な暗号プロトコル(FDH署名,Bellare-Rogawayの公開鍵暗号方式,RSA-KEM鍵配送方式)の安全性証明を試みた。情報漏洩のモデルとして,ハッシュ関数の安全性を議論するために成果を挙げているサブオラクルアプローチを採用した。既に知られていた4つのモデル(LRO,TRO,ERO,RO)に加えて,新たに弱EROモデルを定義して,それぞれのモデルにおける暗号プロトコルの安全性証明をCryptoVerifを用いて試みた。実験の結果,人手による証明結果と一致したのは,TROモデルの場合のみであった。ただし,一致しなかったのは,人手では証明可能と判定されているプロトコルに,CryptoVerifを用いては証明がつかないケースのみである。すなわち,安全でないプロトコルを安全と誤判定することはなかった。本実験により,既存の項書換え規則の拡充が必要な箇所,検証系の機能拡張が必要な箇所等,新たな知見が得られた。
低資源向き認証プロトコルとして,処理量が少ないHB法が有望視されている。一方,被認証側を低資源な装置で実装すると秘密情報が漏洩する危険性が高まるので,その対策として,回路製造時の個体差に注目した処理を行うことで,秘密情報の保持を不要とできる物理的複製困難関数(PUF)という技術が注見されている。本研究では,これらを組み合わせた認証方式(HB-PUF法)の安全性を解析した。計算量を削減したHB系の殆どの方式において具体的な攻撃手順を指摘した。計算量の僅かな増加を許容し,僅かなタンパーなメモリ領域を用いることで,証明可能安全なアルゴリズム的耐タンパー認証装置を実現可能なことを示した。
|
