基于UML的形式化框架及其在安全协议验证中的应用

摘要

随着信息技术的飞速发展，计算机软件系统已广泛应用到社会的各个领域。软件规模和复杂性在不断增加，软件出现错误的可能性也随之增加。为了保证软件的质量、提高软件的可靠性，将主流的软件开发方法与形式化方法相结合是一种可行的方法。
　　本文结合UML方法与形式化方法的优点，提出了基于扩展UML的轻量级形式化框架。通过领域分析，选取并扩展合适的UML模型，形成领域轮廓以支持特定领域建模，进而提供UML模型向形式化模型转换的可行性方案。该框架避免了复杂建模过程，降低了形式化方法的使用门槛，扩大了形式化方法在实际软件开发中的应用。基于该框架，本文还提出了安全协议形式化验证方法，并从工程的角度给出了一套完整的安全协议形式化验证工程方法。该方法制定了适用于安全协议建模的UM L类图和时序图扩展机制，用工程化的协议表达方式形式化安全协议，完成协议安全性验证。通过匹配及转换规则，本文实现了从扩展UML模型向ProVerif规格的Pi演算模型的转化，以验证安全协议的私密性和认证性。此外，该方法基于正则表达式分析并图形化验证结果，能帮助软件开发人员较快发现协议存在的漏洞并精化模型。
　　最后，本文实现了基于扩展UML的安全协议形式化验证平台，并以Hankshake协议、NS公钥协议及买卖水印协议为例，验证了相关的安全性质，证明了本文方法的有效性和实用性。

目录

封面

声明

中文摘要

英文摘要

目录

第一章 绪论

1.1研究背景

1.2研究内容

1.3论文结构

第二章 文献综述

2.1统一建模语言UML

2.2形式化方法

2.3 UML与形式化方法

第三章 基于UML的轻量级形式化框架

3.1问题定位

3.2框架流程

3.3框架公共组件

第四章 基于扩展UML的安全协议形式化验证方法

4.1方法流程

4.2协议UML建模局限性及其扩展

4.3应用Pi演算模型的转化

4.4应用Pi演算模型验证及反例图形化

第五章 安全协议验证平台的设计实现及实例分析

5.1安全协议验证平台的设计与实现

5.2协议实例分析

第六章 总结与展望

6.1总结

6.2展望

参考文献

发表论文和参加科研情况说明

致谢