基于串空间模型安全协议形式化方法的分析与扩展

摘要

网络技术是一把双刃剑，它给人们提供快捷通信的同时，也给信息的安全造成了严重的威胁。信息的安全性在早期主要是依赖好的加解密算法来实现的，但是，伴随着网络开放性的增加和应用多样性的加强，还需要其他方式才能解决好这个问题。安全协议借助于密码算法和协议逻辑，达到在网络环境中提供各种安全服务的目的，已经成为构建网络安全的基石。安全协议形式化分析是指采用各种形式化的语言或者模型，为安全协议的实体和环境建立模型，按照规定的假设和分析、验证方法证明协议的安全性。安全协议的形式化分析已经发展了近三十年，但这个领域仍然远未成熟。串空间理论的出现将安全协议形式化分析推向了一个新的高度。串空间中引入了反映因果关系的偏序结构概念，有效避免了模型检测方法普遍存在的状态空间爆炸问题，同时协议的执行过程用图示法表示，可以借助图的理论和算法对安全协议进行分析。
　　 串空间最初被设计用于分析静态的、参与主体较少的协议，例如认证协议。对于动态的、参与主体相对较多的协议，如ad hoc路由协议、匿名协议等等，基本串空间模型还不能对其进行有效分析，因而需要对它进行进一步研究。本文在深入研究串空间模型理论基础上，对其进行扩展，取得一些新的研究成果。
　　 本文的主要工作在以下几个方面：
　　 (1)匿名性基于串空间的形式化分析是匿名性分析领域的一个重要组成部分，然而这方面的研究才刚刚起步。本文基于丛消息解析等价技术，将观察视角和匿名性结合起来，给出不同观察视角下各种匿名性的定义，并比较它们之间的匿名程度，形成了一个比较完善的基于串空间的匿名形式化框架。以一个基于区域的k匿名路由协议为例，验证形式化框架能有效指出匿名程度偏低的协议中匿名机制不足之处，以指导研究人员进行改进。
　　 (2)对串空间进行扩展并应用于分析比较复杂的协议-ad hoc安全路由协议。本文首先完善了串空间下ad hoc路由协议的一致性和任意中继者可信条件的定义。然后以SRP协议中一个返回不存在路由的攻击实例为例，验证任意中继者可信条件的正确性。
　　 (3)串空间主要用于协议正确性的证明，研究人员较难直接应用它来发现协议漏洞，并进一步获取漏洞原因以及如何改进。分析安全路由协议时，串空间仅仅对各节点消息序列进行形式化，而忽略各节点的消息验证过程。本文研究中继节点中可能存在的敌手节点的各种攻击方式，结合逆向思维，设计出一种基于串空间攻击分析模型，能够比较全面的分析导致协议返回不存在路由的攻击。