网络安全认证协议自动分析系统

摘要

网络协议的安全性分析和验证是当今计算机安全领域中研究的重大课题。协议安全性分析包括非形式化和形式化两种方法，形式化方法是安全协议分析和验证的主要方法。我们以大量的协议形式化建模研究为基础，以网络安全认证协议为研究对象，采用模型检测技术，开发了网络安全认证协议自动分析系统。该系统功能主要是用来对认证协议进行自动建模与验证。本系统分为用户界面模块、自动分析建模模块以及自动验证模块。用户界面模块为用户提供了直观的GUI界面，以可见即可得的方式对网络认证协议进行录入，用这种方式形成系统所接收的原语言——PDL(Protocol Description Language)；自动建模分析子模块设计了认证协议的形式化分析算法，对认证协议进行建模与性质规约；自动验证子模块内嵌SPIN，对建模过程进行自动验证并返回验证结果。 本系统完成了对双方公钥类型和三方对称密钥类型协议的自动建模与验证，并成功地发现了N-S、Helsinki、TMN等协议的攻击漏洞。针对状态爆炸问题，本系统采用了atomic和steps、顺序重定向、缩减随机数变量的取值范围以及偏序规约等多项优化策略，实验结果表明系统采用优化策略具有有效性。此外，系统的创新点还体现在它的抽象性、效率性、自动化程度高、可扩展性以及友好的用户界面等方面。本系统具有较高的应用价值，可作为以网络认证协议为核心的网络通信系统安全性的有效分析、评测工具。

目录

文摘

英文文摘

声明

第一章引言

1.1研究背景

1.2研究思路

1.3论文组织

第二章安全协议及其分析方法

2.1安全协议

2.1.1安全协议的概念

2.1.2安全协议的历史

2.1.3安全协议的分类

2.2安全协议的分析方法

2.2.1安全协议的非形式化分析

2.2.2安全协议形式化分析

第三章模型检测及相关技术

3.1模型检测

3.2几个重要的术语

3.3模型检测工具SPIN

3.4模型检测工具对网络认证协议的安全性分析

3.4.1 Promela对认证协议的建模

3.4.2时态逻辑

3.4.3验证

3.5利用SPIN对N-S协议进行形式化的分析

3.5.1套用Promela对认证协议建模的五个步骤。

3.5.2利用LTL对N-S协议性质的描述

3.5.3利用SPIN对N-S协议进行验证

第四章网络安全认证协议自动分析系统的设计

4.1网络安全认证协议自动分析系统概述

4.1.1系统简介

4.1.2系统功能

4.2系统实现

4.2.1整体设计

4.2.2模块设计

第五章系统特点及其优化策略

5.1系统描述语言PDL

5.2效率性

5.3自动化设计

5.4功能可扩展性

5.5用户界面设计

5.6解决状态爆炸问题之策略

5.6.1 atomic和steps

5.6.2 顺序重定向

5.6.3缩减随机数变量的取值范围

5.6.4偏序规约技术

第六章其它相关工作

6.1认证逻辑

6.2 FDR

6.3 MURΦ

6.4 NRL

6.5 ATHENA

6.6ISBELL

第七章结论与展望

7.1结论

7.2进一步工作方向

致谢

参考文献

攻读学位期间的研究成果