论文部分内容阅读
近几十年来，运用形式化方法对安全协议进行分析验证一直是信息安全领域研究的热点，而模型检测方法成为近年来安全协议形式化研究的主流，并产生了一系列有效的验证方法和验证工具，如：Petri网模型、模型检测工具SPIN等。
针对安全协议抗拒绝服务攻击缺少形式化分析方法的研究现状，基于Meadows框架，结合Petri网强大的建模能力，本文提出了CPN Cost-based安全协议模型；本文还利用模型检测工具SPIN对BAN-Yahalom协议进行了形式化分析验证。
本文的主要研究成果和工作如下：
1.针对入侵者攻击目标的不同，将获取私密信息的安全攻击和消耗服务器资源的拒绝服务攻击分类，对不同的攻击者分别建模分析。
2.基于Meadows Cost-based框架，扩展CPN安全协议形式化模型，提出了CPN Cost-based形式化模型，利用该扩展模型验证了SSL协议容易受到拒绝服务攻击，JFK协议具有良好的抵御拒绝服务攻击性，从而为安全协议抵御拒绝服务攻击性提出了一种形式化分析方法。
3.利用模型检测工具SPIN对BAN-Yahalom协议进行形式化验证，并讨论了Promela语言的攻击者模型，以及利用线性时序逻辑公式描述协议的安全性质，从而验证了这种基于线性时序逻辑的模型检测工具能够有效的运用于安全协议的形式化分析中。
4.利用CPN仿真工具CPN-tools，提出了利用CPN-ML语言查询语言描述安全协议的安全性质的方法，并将该方法与线性时序逻辑的描述方法做比较。
本文的解决方案的可用性和有效性都通过具体的实例来证明。其中，扩展的CPN模型作为分析安全协议抗拒绝服务攻击的形式化模型，具有一定的通用性。而提出的CPN-ML查询函数描述协议安全性质也是有效的。模型检测工具SPIN成功应用到BAN-Yahalom协议的形式化验证中，发现了其协议存在的几个安全漏洞，具有一定的意义。