安全协议进化生成与模态逻辑验证研究

摘要

本文探讨了形式化的、自动化的安全协议分析和设计方法。从模型、方法和应用等多个方面对安全协议自动生成与验证进行了研究。 本论文的主要研究工作有：给出了安全协议自动生成与验证模型，用于指导具体的安全协议自动生成与验证方法研究。提出了认证协议的自动生成和验证方法。该方法采用基于进化策略的生成方法和基于BAN逻辑的验证方法。深入地研究了基于进化算法的安全协议生成方法。提出了基于协同进化的安全协议生成算法。针对电子商务这一热门的安全协议应用领域，提出了电子商务协议的演化生成方法。深入地研究了基于模态逻辑的安全协议形式化验证方法。提出了用模态逻辑来分析安全协议猜测攻击的方法。

目录

文摘

英文文摘

第1章绪论

1.1安全协议及相关技术简介

1.1.1密码学基础

1.1.2安全协议的定义和内涵

1.1.3安全协议的分类

1.1.4安全协议的缺陷和攻击

1.2安全协议分析和设计研究现状

1.2.1安全协议形式化分析研究现状

1.2.2安全协议设计研究现状

1.3本论文的研究目的、内容和创新之处

1.4本论文内容的组织安排

1.5本章小结

第2章安全协议自动生成与验证模型

2.1模型及其特点

2.2针对模型的讨论

2.2.1基本问题

2.2.2生成方法

2.2.3验证方法

2.2.4具体应用

2.3用于安全协议生成的进化算法

2.3.1进化算法概述

2.3.2进化策略

2.3.3协同进化

2.4用于安全协议验证的模态逻辑方法

2.4.1 BAN逻辑

2.4.2 SVO逻辑

2.4.3 CKT5逻辑

2.5本章小结

第3章认证协议的自动生成与验证

3.1认证协议自动生成与验证模型

3.2认证协议的描述和验证

3.3认证协议自动生成与验证算法

3.3.1算法流程

3.3.2染色体编码方案

3.3.3适应度函数

3.3.4操作算子

3.4实验和分析

3.5本章小结

第4章安全协议的进化生成方法研究

4.1安全协议的协同进化生成算法

4.1.1目的和动机

4.1.2安全协议的协同进化生成算法

4.1.3实验和分析

4.1.4算法小结

4.2电子商务协议的演化生成方法

4.2.1电子商务协议的性质

4.2.2电子商务协议的描述和验证

4.2.3电子商务协议生成算法

4.2.4实验和分析

4.2.5相关工作和比较

4.3本章小结

第5章安全协议的模态逻辑验证方法研究

5.1问题的提出

5.2分析安全协议密码系统相关缺陷的模态逻辑方法

5.2.1安全协议密码系统相关缺陷及其形式化分析

5.2.2 CKT5逻辑扩展

5.2.3实例分析

5.2.4讨论

5.3分析安全协议猜测攻击的模态逻辑方法

5.3.1安全协议猜测攻击及其形式化分析

5.3.2 CKT5逻辑扩展

5.3.3实例分析

5.3.4讨论

5.4本章小结

第6章总结与展望

参考文献

致谢

读博期间完成的论文

读博期间参加的科研项目