セキュリティプロトコルの形式的検証の計算論的健全性に関する研究

暗号プロトコルの検証には、形式的手法と計算論的手法がある。形式的手法では、メッセーシが記号表現に抽象化され、攻撃者は記号表現に対する限られた操作しか実行できないため、プロトコル検証は単純で自動化しやすいが、暗号を解読するような攻撃は考慮されない。一方、計算論的手法では、計算量理論に基づいて暗号プリミティブの脆弱性を考慮するため、プロトコル検証は、いかなる攻撃も見逃さないが、複雑で間違いやすい。近年、形成的手法の計算論的健全性(computational soundness)、すなわち「プロトコルで用いられる暗号プリミティブが一定の計算量的安全性を満たすならば、形式的手法によるプロトコル検証がいかなる攻撃も見逃さない」という性質の研究が盛んである。本研究では、昨年度に考案した計算論的健全性の証明技法を発展させ、より大きなプロトコルのクラスに対して計算論的健全性の結果を得ることができた。具体的には、プロトコル実行中に生成された多項式個の鍵をネットワークから受け取って暗号文を生成するような場合を扱えるようにした。また、動的コラプトを扱える計算論的に健全な記号モデルについても検討し、計算論的に健全な排他的論理和の記号モデルを得るために必要なプロトコルに対する制限を明らかにした。

暗号プロトコルの検証には、形式的手法と計算論的手法がある。形式的手法では、メッセーシが記号表現に抽象化され、攻撃者は記号表現に対する限られた操作しか実行できないため、プロトコル検証は単純で自動化しやすいが、暗号を解読するような攻撃は考慮されない。一方、計算論的手法では、計算量理論に基づいて暗号プリミティブの脆弱性を考慮するため、プロトコル検証は、いかなる攻撃も見逃さないが、複雑で間違いやすい。近年、形成的手法の計算論的健全性(computational soundness)、すなわち「プロトコルで用いられる暗号プリミティブが一定の計算量的安全性を満たすならば、形式的手法によるプロトコル検証がいかなる攻撃も見逃さない」という性質の研究が盛んである。本研究では、昨年度に考案した計算論的健全性の証明技法を発展させ、より大きなプロトコルのクラスに対して計算論的健全性の結果を得ることができた。具体的には、プロトコル実行中に生成された多項式個の鍵をネットワークから受け取って暗号文を生成するような場合を扱えるようにした。また、動的コラプトを扱える計算論的に健全な記号モデルについても検討し、計算論的に健全な排他的論理和の記号モデルを得るために必要なプロトコルに対する制限を明らかにした。