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

《实例化空间逻辑在安全协议验证中的语义研究与应用》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、实例化空间逻辑在安全协议验证中的语义研究与应用专业：计算机软件与理论博士生：肖茵茵指导老师：苏开乐教授摘要安全协议是在开放网络中借助密码体制达到密钥分配、身份认证、信息保密等特定目标的通信规范，其正确性对网络应用的安全至关重要．安全协议的手工分析十分困难，容易出错，因此，使用严谨的形式化验证方法和高效可靠的自动验证工具来分析协议是当前安全协议研究的热点．从协议验证的目的划分．安全协议的形式化验证方法可分为证伪法和证真法：前者的目标在于寻找协议的漏洞和潜在攻击的路径：后者用于验证协议是否能够满足某些安全性质以及证明协议的

2、正确性．实例化空间逻辑(InstantiationSpaceLogic，ISL)是一个在Dolev-Yao攻击者模型下对安全协议进行形式化验证的证真法．ISL以实例化空间为语义模型，拥有一组尽可能完备的一阶逻辑公理集，能够验证工业级复杂协议的认证性、秘密性等相关安全性质．但是，ISL的普适性还有待理论上的验证．ISL的公理集在算法上是可实现的，其相应的自动化验证工具为SPV(SecurityProtocolVerifier)．SPV能够处理包含公钥、私钥、共享密钥和hash密钥嵌套加密的复杂消息格式．该工具使用知识推理

3、方法，调用SAT求解器，能够高效验证安全协议是否满足CAPSL(CommonAuthenticationProtocolSpecificationLanguage)协议规范及单层、多层认知规范．协议的验证是个不可判问题，因此，无法直接对一个安全协议验证逻辑公理系统进行严格的完备性证明，只能通过实验或其它的方式对其普适性进行检验．为了对实例化空间逻辑ISL的语义表达能力给出理论上和实践上的衡量与评价，本文对ISL的语义及其应用进行了研究．目前，对安全协议形式化验证逻辑语义方面的研究工作为数不多，因此该工作在一定程度上填补

4、了这方面研究的空白．我们通过在实例化空间语义模型下解释其它主流安全协议验证逻辑的实例化空间逻辑在安全协议验证中的语义研究与应用方法，说明了ISL具有较强的语义表达能力．ISL较强的语义表达能力使其具有实用性：在不同应用领域下，我们给出了一些重要工业级协议的合理简化模型和转换方法，利用SPV对这些协议进行完全自动化的证明，针对协议验证结果的不足，对协议进行了某些改进．我们还对原有的ISL理论进行扩展，使其能够验证更多类型的协议，这体现了ISL的语义可扩展性．原有的ISL语义与应用都是基于Dolev-Yao模型的，为使IS

5、L适用于计算能力更强、更贴近协议实际运行的Computational攻击者模型，我们还定义TISL的计算语义，为ISL理论实现攻击者模型的转换打下了重要基础．本文的主要工作如下：·原有的ISL理论将Diffie-Hellman密钥抽象为共享密钥，未讨论DH密钥本身的性质，也未描述异或算子XOR的性质．我们基于扩展的加密消息交换模型、扩展的安全协议形式化描述和扩展的实例化空间，对ISL的公理系统进行补充，增加了与DH密钥假设相关的核心公理和与异或相关的主要公理．在不影响原有公式和公理的前提下，扩展的ISL具有更强的表达能

6、力，足以验证包含DH密钥加密消息和带异或算子的安全协议．·为了从理论上衡量ISL的普适性，我们选择另一种实用的基于证真的安全协议验证法组合协议逻辑PCL，对ISL和PCL之间的关系进行了分析．在此基础上，将PCL的语义模型转换为ISL的实例化空间语义模型，在实例化空间下对PCL的主要公式、定理、推导规则做了语义解释．研究表明，实例化空间能够完全表示PCL的语义，且ISL的语义表达能力强于PCL．新的模型解释使PCL更易于扩展，且使得用PCL理论验证的协议能够利用SPV自动验证．·电子商务领域中的安全电子交易Secure

7、ElectronicTransaction，SET)协议是目前最复杂的工业级协议之一，其原始文档有上千页，简化过程相当困难，相关研究较少，已有的一些简化模型也不够完整．我们在花费大量时间研究SET协议原始文档的基础上，为该协议提出了合理的化简规则，给出了比以往更贴近原协议的简化模型．利用ISL的自动化验证工具SPV实现了对SET协议秘密性、认证性等安全性质的自动化验证，并对协议进行了改进．该工作充分说明了ISL和SPV足以处理复杂的工业级协议．·由于W-eb服务安全(WS—Security)协议与传统网络安全协议的描述

8、方式不同，因此无法直接使用原有的安全协议验证技术对WS—Security协议进行形式化验证．实际上，到目前为止，仍无完整、实用的理论和方法可以证明WS—Security协议的安全性质是否能在协议的任意无穷会话中被满足．我们提出了一个对WS-Security协议的认证性进行自动化验证的方法：我们在一些自动化工具的支持下将WS-Sec