安全协议操作语义模型研究及应用-计算机软件与理论专业论文

摘

摘 要

桂林电子科技大学学位论文

桂林电子科技大学学位论文

摘要

安全协议的操作语义模型是一种分析安全协议的新模型，它结合了以往多种协议 分析模型的优点，能分析多个协议及多个主体并行运行的协议系统的安全性，具有严 谨、简洁、高效等特点。

本文对安全协议的操作语义模型进行了深入的研究，并基于该语义模型对目前安 全协议形式化分析领域中两个热点问题 "组合协议"和"多方协议"的安全性进行研 究。取得的主要成果如下

(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协议提出了一个用于多个主体间相互认证的多 方认证协议。

关键词: 操作语义模型:组合协议:多方协议:形式化方法.

万方数据

I –

–

– PAGE IV –

万方数据

Abstract

The operational semantics model of security protocol is a new approach for an- alyzing and verifying the security of protocol .Having fully absorbed many merits of different models，it becomes a strict，concise ，high effective method and can straight- forwardly analyze the parallel execution of multi protocols system and multi agents system.

The aim of this task is to analyze the operational semantics model of security protocol and to verify the security of multi protocols system and multi agents system by the operational semantics model. The main results obtained are as follows:

The operational semantics model of security protocol is studied and a new frame based on this model is constructed, in which the formal definition of agent

model，communication model，cryptographic primitives and security requirements are

studied.Finally，as an example ，the operational semantics model of NS protocol is constructed.

Scyther ，which is an automatic analyzer of security protocol based on the oper