实例化空间逻辑在安全协议验证中语义及研究应用.pdf

实例化空间逻辑在安全协议验证中的语义研究与应用 专 业： 计算机软件与理论 博士生： 肖茵茵 指导老师： 苏开乐教授 摘要 安全协议是在开放网络中借助密码体制达到密钥分配、身份认证、信息保 密等特定目标的通信规范，其正确性对网络应用的安全至关重要．安全协议的 手工分析十分困难，容易出错，因此，使用严谨的形式化验证方法和高效可靠的 自动验证工具来分析协议是当前安全协议研究的热点．从协议验证的目的划分． 安全协议的形式化验证方法可分为证伪法和证真法：前者的目标在于寻找协议 的漏洞和潜在攻击的路径：后者用于验证协议是否能够满足某些安全性质以及 证明协议的正确性． 实例化空间逻辑(InstantiationSpace 模型下对安全协议进行形式化验证的证真法．ISL以实例化空间为语义模型， 拥有一组尽可能完备的一阶逻辑公理集，能够验证工业级复杂协议的认证性、 秘密性等相关安全性质．但是，ISL的普适性还有待理论上的验证．ISL的公 Protocol 理集在算法上是可实现的，其相应的自动化验证工具为SPV(Security 消息格式．该工具使用知识推理方法，调用SAT求解器，能够高效验证安全协议 Authentication Protocol 是否满足CAPSL(Common SpecificationLanguage)协 议规范及单层、多层认知规范． 协议的验证是个不可判问题，因此，无法直接对一个安全协议验证逻辑公 理系统进行严格的完备性证明，只能通过实验或其它的方式对其普适性进行检 验．为了对实例化空间逻辑ISL的语义表达能力给出理论上和实践上的衡量与 评价，本文对ISL的语义及其应用进行了研究．目前，对安全协议形式化验证逻 辑语义方面的研究工作为数不多，因此该工作在一定程度上填补了这方面研究 的空白．我们通过在实例化空间语义模型下解释其它主流安全协议验证逻辑的 实例化空间逻辑在安全协议验证中的语义研究与应用 方法，说明了ISL具有较强的语义表达能力．ISL较强的语义表达能力使其具有 实用性：在不同应用领域下，我们给出了一些重要工业级协议的合理简化模型 和转换方法，利用SPV对这些协议进行完全自动化的证明，针对协议验证结果 的不足，对协议进行了某些改进．我们还对原有的ISL理论进行扩展，使其能够 验证更多类型的协议，这体现了ISL的语义可扩展性．原有的ISL语义与应用都 是基于Dolev-Yao模型的，为使ISL适用于计算能力更强、更贴近协议实际运行 击者模型的转换打下了重要基础． 本文的主要工作如下： 的性质，也未描述异或算子XOR的性质．我们基于扩展的加密消息交换模 型、扩展的安全协议形式化描述和扩展的实例化空间，对ISL的公理系统 进行补充，增加了与DH密钥假设相关的核心公理和与异或相关的主要公 理．在不影响原有公式和公理的前提下，扩展的ISL具有更强的表达能力， 足以验证包含DH密钥加密消息和带异或算子的安全协议． ·为了从理论上衡量ISL的普适性，我们选择另一种实用的基于证真的安全 协议验证法组合协议逻辑PCL，对ISL和PCL之间的关系进行了分析．在此 基础上，将PCL的语义模型转换为ISL的实例化空间语义模型，在实例化空 间下对PCL的主要公式、定理、推导规则做了语义解释．研究表明，实例化 空间能够完全表示PCL的语义，且ISL的语义表达能力强于PCL．新的模型 解释使PCL更易于扩展，且使得用PCL理论验证的协议能够利用SPV自动 验证． Electronic ·电子商务领域中的安全电子交易Secure Transaction，SET)协 议是目前最复杂的工业级协议之一，其原始文档有上千页，简化过程相当 困难，相