|
形式的手法に基づく安全性検証では、数学的に厳密な証明を与えることが可能である。そのため、セキュリティ分野で重要な役割を担う暗号プロトコル等の安全性検証への応用が広く期待されている。本研究は暗号プロトコル検証に、形式的手法の観点からプログラミング言語理論研究の手法を応用することにより新たな検証手法を開拓することを目指している。その前半として、今年度は、先行研究を手掛りに暗号プロトコル検証に求められる安全性要件とその形式的記述、また妥当な攻撃者モデルについての検討を行うことに取り組んだ。
先行研究として、Paulsonによる暗号プロトコルTLS(Transport Security Layer)のトレースモデルに基づく形式的検証について詳細な分析を行ない、そこで証明されている安全性性質とモデル化形式との関連性について検討を行なっている。Paulsonの結果の分析については、もともとは自動定理証明ツールIsabelle/HOL上で行われていた検証を、型理論に基づく証明支援系Coq上に移植するという作業を通じて行なった。このような過程を経ることによりPaulsonの結果の汎用性を確認し、また比較的汎用性の低い部分を明確に捉えることが出来た。現時点ではまだいくつか分析すべき項目が残っており、今後も攻撃者モデルなどについて検討を進める。その結果をもとに、来年度では形式的体系を厳密に定義し、暗号プロトコルの安全性検証に応用する。また時間が許せば、定義された形式的体系に対する計算量的拡張についても検討したい。
現時点までの本研究の結果については、2件の研究報告を行ない、うち一件は来年度に予稿集発行の予定である。また現在、論文誌へも投稿準備中である。
|
