安全协议形式化描述语言的设计与解析

论文摘要

安全协议的重要性随着网络技术的飞速发展与日俱增，安全协议的形式化分析已成为网络安全领域的研究热点。形式化描述是形式化分析的前提。本文首先对安全协议的形式化描述技术进行了概述。在此基础上，对安全协议形式化描述语言的设计以及解析器的设计与实现进行了较为深入的研究，主要内容包括：首先，研究了安全协议的多重集重写模型MSR（multiset rewriting），针对它在协议自动化分析方面存在的不足，通过在消息谓词中引入安全属性谓词对MSR模型进行了扩展。根据扩展的MSR模型设计了安全协议的低级描述语言IL（interpretation language），并给出了IL完整的定义。理论与实践表明，IL能精确刻画协议的运行及其安全属性，且易于转换为末端分析程序的初始化输入。其次，针对IL可读性较差、普通用户不易用其对安全协议进行刻画的问题，研究了动作时序逻辑TLA（temporal logic of actions）的描述语言TLA+，借鉴其模块化的描述方式和TLA的语义设计了安全协议的高级描述语言PSL（protocol specification language），并给出了PSL完整的定义。PSL基于角色的、类似于消息交互的协议描述方式较好满足了用户的需求。通过与其它描述语言的对比，PSL描述能力较强。而且，PSL与IL存在一种对应关系，保证了协议的PSL描述能唯一的转换为IL描述。随后，针对安全协议自动化分析的需求，需将协议的PSL描述转换为IL描述。由于协议的IL描述不能直接被末端分析程序识别，还需将其转换为分析程序的初始化输入。为此，借助现有词法分析工具Flex和语法分析工具Bison设计并实现了PSL解析器和IL解析器，为协议描述语言之间的自动转换和末端分析程序的初始化打下了基础。此外，为了检验设计并实现的安全协议形式化描述和解析系统的正确性，同时也为了检测末端分析程序的有效性，构造了一个由安全协议的PSL描述组成的测试集，选取该测试集中三种不同类型的协议对安全协议自动化分析系统进行了正确性测试，测试结果表明系统顺利检测出了协议已知的攻击。此外，从错误发现和解析时间两方面对解析器的性能进行了测试，测试结果表明其较好地满足了系统的需求。最后，对本文工作进行了总结，并对下一步的研究工作做了展望。

论文目录

• 表目录
• 图目录
• 摘要
• ABSTRACT
• 第一章 绪论
• 1.1 课题的提出
• 1.2 安全协议形式化描述的必要性
• 1.2.1 安全协议非形式化描述的缺点
• 1.2.2 安全协议形式化描述的优点
• 1.3 安全协议形式化描述技术的发展与现状
• 1.4 本文的主要工作及结构安排
• 第二章 基于MSR的安全协议低级描述语言设计
• 2.1 低级描述语言的设计思路
• 2.2 MSR模型
• 2.2.1 基本概念
• 2.2.2 多重集重写理论
• 2.2.3 协议执行
• 2.2.4 攻击者理论
• 2.2.5 MSR的描述实例
• 2.3 低级描述语言IL的设计
• 2.3.1 对MSR模型的扩展
• 2.3.2 IL的定义
• 2.3.3 IL的结构、标识符、类型、常量和变量
• 2.3.4 IL表达式与语句
• 2.3.5 IL的描述实例
• 2.3.6 对IL的评价
• 2.4 小结
• 第三章 基于TLA+的安全协议高级描述语言设计
• 3.1 高级描述语言的设计思路
• 3.2 TLA+概念
• 3.2.1 TLA简介
• 3.2.2 TLA基本概念
• 3.2.3 用TLA描述和验证系统
• 3.3 高级描述语言PSL的设计
• 3.3.1 TLA+在PSL中的应用
• 3.3.2 高级描述语言的定义
• 3.3.3 PSL结构、标识符、常量和变量
• 3.3.4 PSL表达式和语句
• 3.3.5 PSL控制结构
• 3.3.6 PSL的描述实例
• 3.4 高级描述语言之间的比较
• 3.5 小结
• 第四章 解析器的设计与实现
• 4.1 PSL到IL的解析
• 4.1.1 PSL解析器功能结构设计
• 4.1.2 PSL解析器主函数
• 4.1.3 PSL词法分析模块
• 4.1.4 PSL语法分析模块
• 4.1.5 PSL语义分析和目标代码生成模块
• 4.2 IL到末端分析程序的解析
• 4.2.1 IL解析器功能结构设计
• 4.2.2 IL解析器主函数
• 4.2.3 IL词法分析模块
• 4.2.4 IL语法分析模块
• 4.2.5 IL语义分析模块
• 4.3 小结
• 第五章 系统测试与结果分析
• 5.1 测试对象
• 5.2 测试方法与环境
• 5.3 测试结果与分析
• 5.3.1 系统正确性测试
• 5.3.2 解析器性能测试
• 5.4 小结
• 结束语
• 参考文献
• 附录A NSPK的MSR描述
• 附录B NSPK的IL描述
• 附录C NSPK的PSL描述
• 作者简历 作者攻读硕士学位期间完成的主要工作
• 致谢