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

使用形式化方法开发适合密码协议验证的形式化系统

基本信息

批准号：
18760293
负责人：
田中三貴
金额：
$ 1.15万
依托单位：
National Institute of Advanced Industrial Science and Technology (2007)National Institute of Information and Communications Technology (2006)
依托单位国家：
日本
项目类别：
Grant-in-Aid for Young Scientists (B)
财政年份：
2006
资助国家：
日本
起止时间：
2006 至 2007
项目状态：
已结题

来源：
https://kaken.nii.ac.jp/grant/KAKENHI-PROJECT-18760293/
关键词：
形式的手法安全性検証暗号プロトコル形式言語

项目摘要

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

基于正式方法的安全验证可以给出数学严格的证据。因此，人们普遍期望将其用于对加密协议的安全验证，该协议在安全领域中起着重要作用。这项研究旨在通过从形式方法的角度应用编程语言理论研究方法来开发一种新的验证方法。上一年的研究中的框架是基于Dolev-yao模型的完整加密假设，但旨在进行更现实的验证，今年，我们对加密方法和协议进行了评估。在集成评估中整合评估并结合计算讨论。具体而言，在定理证明工具上实施了Bellare＆Rogaway（Eurocrypt，2006年）中提出的方法。该建议促进了使用编程语言的使用，以更准确的讨论使用游戏，这是密码字段中的标准证明风格。在这里，为了以实际上有用的方式实现此建议，如果将其正式定义为正式定义，则该编程语言将毫无意义。因此，在这项研究中，在定理证明支持系统COQ上定义了命令式编程语言，从而提供了随机的操作意义理论。如果您使用此语言来描述游戏并在Coq上证明游戏的标题，则可以通过将标题应用于游戏来正式提供安全证明。作为该框架的一个特定示例，COQ上的证明是给PRF/PRP开关字幕的，该字幕是用于安全证明的定理，例如块密码。