垣曲做网站,金华网站制作案例,网站动态加速,wordpress文章固定字段安全协议操作语义模型研究及应用-计算机软件与理论专业论文摘摘 要桂林电子科技大学学位论文桂林电子科技大学学位论文摘要安全协议的操作语义模型是一种分析安全协议的新模型#xff0c;它结合了以往多种协议 分析模型的优点#xff0c;能分析多个协议及多个主体并行运行的协…安全协议操作语义模型研究及应用-计算机软件与理论专业论文摘摘 要桂林电子科技大学学位论文桂林电子科技大学学位论文摘要安全协议的操作语义模型是一种分析安全协议的新模型它结合了以往多种协议 分析模型的优点能分析多个协议及多个主体并行运行的协议系统的安全性具有严 谨、简洁、高效等特点。本文对安全协议的操作语义模型进行了深入的研究并基于该语义模型对目前安 全协议形式化分析领域中两个热点问题 组合协议和多方协议的安全性进行研 究。取得的主要成果如下(1)对安全协议的操作语义模型进行研究建立了基于此语义模型的协议分析杠 架。在该杠架中分析了协议参与主体通信模型威胁模型密码学原语以及安全属性 等协议组成要素并以NS为例说明利用操作语义模型分析协议的建模过程。(2)对基于操作语义模型自动化验证工具Scyther进行研究。分析了Scyther的内 部运行机制给出了利用Scyther分析安全协议一般步骤并以移动通信系统的密钥分 配协议(TMN)为例利用Scyther对其安全性进行验证结果表明该协议存在机密性与 认证性缺陷给出了针对该缺陷的攻击路径并分析了其产生原因。最后以NS协议为 例从时间和空间两个方面比较了Scyther和传统的模型检验器SMV的性能结果表 明Scyther具有更优越的时空性能。(3)利用安全协议的操作语义模型对组合协议的安全性进行研究。给出了组合协 议系统及组合协议攻击的形式化的描述介绍了利用操作语义模型分析组合协议的安 全性的一般步骤。基于此分别对含Yahalom和Denning-Sacco两个协议以及含Yahaloo- BANYahalom-Lowe和Denning-Sacco 个协议的组合协议系统的安全性进行分析结 果表明这两个组合协议系统均存在组合协议攻击给出了攻击路径并分析了其产生的 原因。(4)利用安全协议的操作语义模型对多方协议的安全性进行研究。对 方认证协 议BNV的安全性进行分析结果表明该协议存在认证性缺陷。针对该缺陷提出了在 协议的消息中添加标识协议主体的消息项的改进分析结果表明改进的协议不存在原 协议的缺陷。最后基于改进后的BNV协议提出了一个用于多个主体间相互认证的多 方认证协议。关键词: 操作语义模型:组合协议:多方协议:形式化方法.万方数据I ––– PAGE IV –万方数据AbstractThe 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 modelsit becomes a strictconcise 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 agentmodelcommunication modelcryptographic primitives and security requirements arestudied.Finallyas an example the operational semantics model of NS protocol is constructed.Scyther which is an automatic analyzer of security protocol based on the oper