论文部分内容阅读
安全协议的操作语义模型是一种分析安全协议的新模型,它结合了以往多种协议分析模型的优点,能分析多个协议及多个主体并行运行的协议系统的安全性,具有严谨、简洁、高效等特点。 本文对安全协议的操作语义模型进行了深入的研究,并基于该语义模型对目前安全协议形式化分析领域中两个热点问题:“组合协议”和“多方协议”的安全性进行研究。取得的主要成果如下: (1)对安全协议的操作语义模型进行研究,建立了基于此语义模型的协议分析框架。在该框架中分析了协议参与主体,通信模型,威胁模型,密码学原语以及安全属性等协议组成要素,并以NS为例说明利用操作语义模型分析协议的建模过程。 (2)对基于操作语义模型自动化验证工具Scyther进行研究。分析了Scyther的内部运行机制,给出了利用Scyther分析安全协议一般步骤,并以移动通信系统的密钥分配协议(TMN)为例,利用Scyther对其安全性进行验证,结果表明该协议存在机密性与认证性缺陷,给出了针对该缺陷的攻击路径并分析了其产生原因。最后,以NS协议为例,从时间和空间两个方面比较了Scyther和传统的模型检验器SMV的性能,结果表明Scyther具有更优越的时空性能。 (3)利用安全协议的操作语义模型对组合协议的安全性进行研究。给出了组合协议系统及组合协议攻击的形式化的描述,介绍了利用操作语义模型分析组合协议的安全性的一般步骤。基于此,分别对含Yahalom和Denning-Sacco两个协议以及含Yahaloo-BAN,Yahalom-Lowe和Denning-Sacco三个协议的组合协议系统的安全性进行分析,结果表明这两个组合协议系统均存在组合协议攻击,给出了攻击路径并分析了其产生的原因。 (4)利用安全协议的操作语义模型对多方协议的安全性进行研究。对三方认证协议BNV的安全性进行分析,结果表明该协议存在认证性缺陷。针对该缺陷,提出了在协议的消息中添加标识协议主体的消息项的改进,分析结果表明改进的协议不存在原协议的缺陷。最后,基于改进后的BNV协议提出了一个用于多个主体间相互认证的多方认证协议。