形式的手法による暗号プロトコル検証に適した形式的体系の開発

点击翻译按钮获取中文摘要

形式的手法に基づく安全性検証では,数学的に厳密な証明を与えることが可能である。そのため,セキュリティ分野で重要な役割を担う暗号プロトコル等の安全性検証への応用が広く期待されている。本研究は暗号プロトコル検証に,形式的手法の観点からプログラミング言語理論研究の手法を応用することにより新たな検証手法を開拓することを目指している。前年度の研究における枠組みは,完全暗号仮定の上でのDolev-Yaoモデルに基づくものであったが,より現実的な検証を行うことを目指して,今年度は,暗号化手法の評価とプロトコルの評価を統合的に,かつ計算量的議論も組み入れて行うための形式的枠組みについての研究に取り組んだ。具体的にはBellare&Rogaway(Eurocrypt,2006)の論文で提案されている手法を定理証明ツール上で実装した。この提案は,暗号分野における標準的な証明スタイルであるゲームを利用した議論を,より正確に行うためにプログラミング言語の利用を促すものである。ここで,この提案を実際に有用な形で実現するためには,このプログラミング言語は形式的に厳密に定義されたものでなくては無意味である。そこで,本研究では定理証明支援系Coq上で命令型プログラミング言語を定義し,確率的操作的意味論を与えた。この言語を使って,ゲームを記述し,その一方でゲームの変換についての補題をCoq上で証明すれば,ゲームに対してその補題を適用する形で安全性証明を形式的に与えることができる。この枠組みを適用した具体例としてまず,ブロック暗号などの安全性証明に用いられる定理であるPRF/PRP switching補題について,Coq上での証明を与えた。