模型检测在安全协议形式化验证中的应用

摘要

信息对当代社会具有重要作用，信息安全依赖于安全协议的应用。对安全协议的分析是一项极有价值的工作。目前的安全协议验证工作主要采用各种形式化方法，如模态逻辑证明、定理证明理论以及模型检测方法。模态逻辑技术采用各种公式进行论述，验证是否能实现预期要求，操作流程比较简便，其中著名的方法有BAN逻辑、SVO逻辑、Kialar逻辑等；定理证明理论通过对各实体进行定义，利用命题证明检验缺陷的有无，其中应用较多的技术有Isabelle技术、串空间等。随着各种检测手段的发展，入侵技术也在不断更新，原有检测手段的不足逐渐显露出来。模态逻辑方式虽然易懂易用，可有时不能提供精确的表达，分析能力有限；定理证明方法较模态逻辑有了较大改进，验证过程更加严谨，但是检测内容主要集中在协议正确性方面，验证能力比较有限，证明过程不是很好理解，而且难以实现自动化。即便如此，这两种分析方法还是在协议验证中作出了重要贡献，检测能力比早期的人为判断有很大进步。模型检测方法的使用较晚，但应用已经比较广泛了。该方法最早被用于硬件验证，随着上世纪末被引入安全协议领域后，经历了一个飞速发展的阶段。模型检测技术根据系统模型和验证属性进行状态空间搜索，其优势在于自动化程度高，用模型检测工具进行自动分析，大大减少了人工干预，当验证属性不满足时能够提供相应的反例。
　　本文首先介绍了密码学和安全协议的理论基础，重点介绍了形式化方法的理论和技术。接着介绍了模型检测技术的工作原理，对模型检测工具SMV的工作过程进行实例说明。之后，采用基于理论证明的串空间技术对 Otway-Rees协议、NSPK协议进行分析。最后，利用模型检测工具SMV对Otway-Rees协议、NSPK协议以及两种协议的修改版本进行了验证，检测协议中是否存在缺陷。经过检测，验证了先前理论对两种协议的分析，以及模型检测方法的有效性。

目录

封面

声明

中文摘要

英文摘要

目录

第一章 绪论

1.1 问题研究背景

1.2 形式化技术的研究现状

1.3 本文工作介绍

1.4 本章小结

第二章 安全协议简介

2.1 密码学简介

2.2 安全协议简介

2.3 本章小结

第三章 形式化验证的基础

3.1 形式化验证技术的主要方法

3.2 模型检测的工作过程

3.3 模型检测工具SMV

3.4 本章小结

第四章 利用串空间方法进行协议分析

4.1 NSPK协议的串空间分析

4.2 Otway-Rees协议的串空间分析

4.3 本章小结

第五章 使用模型检测技术对协议进行验证

5.1 利用SMV对Otway-Rees协议实施验证

5.2 用符号化模型检测工具SMV分析NSPK协议

5.3本章小结

第六章 结束语

6.1 本文工作总结

6.2 后续工作展望

致谢

参考文献