论文部分内容阅读
安全协议是在开放网络中借助密码体制达到密钥分配、身份认证、信息保密等特定目标的通信规范，其正确性对网络应用的安全至关重要。安全协议的手工分析十分困难，容易出错，因此，使用严谨的形式化验证方法和高效可靠的自动验证工具来分析协议是当前安全协议研究的热点。从协议验证的目的划分,安全协议的形式化验证方法可分为证伪法和证真法：前者的目标在于寻找协议的漏洞和潜在攻击的路径；后者用于验证协议是否能够满足某些安全性质以及证明协议的正确性。
实例化空间逻辑(ISL)是一个在Dolev-Yao攻击者模型下对安全协议进行形式化验证的证真法。ISL以实例化空间为语义模型，拥有一组尽可能完备的一阶逻辑公理集，能够验证工业级复杂协议的认证性、秘密性等相关安全性质。但是，ISL的普适性还有待理论上的验证.ISL的公理集在算法上是可实现的，其相应的自动化验证工具为SPV(Security ProtocolVerifier).SPV能够处理包含公钥、私钥、共享密钥和hash密钥嵌套加密的复杂消息格式。该工具使用知识推理方法，调用SAT求解器，能够高效验证安全协议是否满足CAPSL(Common Authentication Protocol Specification Language)协议规范及单层、多层认知规范。
协议的验证是个不可判问题，因此，无法直接对一个安全协议验证逻辑公理系统进行严格的完备性证明，只能通过实验或其它的方式对其普适性进行检验。为了对实例化空间逻辑ISL的语义表达能力给出理论上和实践上的衡量与评价，本文对ISL的语义及其应用进行了研究.目前，对安全协议形式化验证逻辑语义方面的研究工作为数不多，因此该工作在一定程度上填补了这方面研究的空白.我们通过在实例化空间语义模型下解释其它主流安全协议验证逻辑的方法，说明了ISL具有较强的语义表达能力.ISL较强的语义表达能力使其具有实用性：在不同应用领域下，我们给出了一些重要工业级协议的合理简化模型和转换方法，利用SPV对这些协议进行完全自动化的证明，针对协议验证结果的不足，对协议进行了某些改进.我们还对原有的ISL理论进行扩展，使其能够验证更多类型的协议，这体现了ISL的语义可扩展性.原有的ISL语义与应用都是基于Dolev-Yao模型的，为使ISL适用于计算能力更强、更贴近协议实际运行的Computational攻击者模型，我们还定义了ISL的计算语义，为ISL理论实现攻击者模型的转换打下了重要基础。
本文的主要工作如下：
⑴原有的ISL理论将Diffie-Hellman密钥抽象为共享密钥，未讨论DH密钥本身的性质，也未描述异或算子XOR的性质。我们基于扩展的加密消息交换模型、扩展的安全协议形式化描述和扩展的实例化空间，对ISL的公理系统进行补充，增加了与DH密钥假设相关的核心公理和与异或相关的主要公理.在不影响原有公式和公理的前提下，扩展的ISL具有更强的表达能力，足以验证包含DH密钥加密消息和带异或算子的安全协议。
⑵为了从理论上衡量ISL的普适性，我们选择另一种实用的基于证真的安全协议验证法组合协议逻辑PCL，对ISL和PCL之间的关系进行了分析。在此基础上，将PCL的语义模型转换为ISL的实例化空间语义模型，在实例化空间下对PCL的主要公式、定理、推导规则做了语义解释。研究表明，实例化空间能够完全表示PCL的语义，且ISL的语义表达能力强于PCL.新的模型解释使PCL更易于扩展，且使得用PCL理论验证的协议能够利用SPV自动。
⑶电子商务领域中的安全电子交易(SET)协议是目前最复杂的工业级协议之一，其原始文档有上千页，简化过程相当困难，相关研究较少，已有的一些简化模型也不够完整。我们在花费大量时间研究SET协议原始文档的基础上，为该协议提出了合理的化简规则，给出了比以往更贴近原协议的简化模型，利用ISL的自动化验证工具SPV实现了对SET协议秘密性、认证性等安全性质的自动化验证，并对协议进行了改进.该工作充分说明了ISL和SPV足以处理复杂的工业级协议。
⑷由于Web服务安全(WS-Security)协议与传统网络安全协议的描述方式不同，因此无法直接使用原有的安全协议验证技术对WS-Security协议进行形式化验证。实际上，到目前为止，仍无完整、实用的理论和方法可以证明WS-Security协议的安全性质是否能在协议的任意无穷会话中被满足.我们提出了一个对WS-Security协议的认证性进行自动化验证的方法：我们在一些自动化工具的支持下将WS-Security协议转换为传统协议消息格式，利用ISL理论将该协议的认证性描述为认知规范，最后使用SPV实现了对WS-Security协议的认证性进行自动化验证，并根据验证结果讨论了协议的安全性.该工作从一个新的角度研究了Web服务安全，也为WS-Security协议的设计与改进提供了帮助。
⑸ISL原先的语义是基于Dolev-Yao模型的，较为抽象和符号化。我们基于Computational模型，引入概率随机性，为ISL构建新的语义模型，定义新的计算语义。计算语义具有不同于符号化层面的一些新特性(例如Computational模型下的秘密性由不可区分性刻画)，基于计算语义，ISL能够使用原来的证明系统在符号化层面对安全协议进行验证，但验证过程将比原来更贴近协议的实际运行情况.该工作是将ISL从Dolev-Yao模型转换到Computational模型下的研究中最重要的一步。