1.3 课题研究的主要内容

随着因特网和基于网络服务的发展，如今新的安全协议的数量和规模已经超出了人们的能力来对其进行严格地分析和验证，这对像IETF（Internet Engineering Task Force）、ITU（International Telecommunication Union）、W3C（World Wide Web Consortium）这样的标准化组织以及产品或服务是基于这些协议的公司而言是一个日益严重的问题。对使用基于安全基础设施的技术的用户而言，也是一个问题。

从之前的研究中，我们能看到大量安全协议的形式化分析的新技术，许多自动化或半自动化的安全协议分析工具被提出，但都只能分析小型或中型的协议。因而，发展至分析大规模、工业化的安全协议是一个科学上和技术上的挑战。AVISPA以一种系统化地方式实现了这种挑战。

AVISPA是一套基于模型检测原理，建立和分析安全协议模型的工具，具有完全自动化、稳定、富有表现力、易于使用等特点，可用于验证各种安全相关网络协议。利用 AVISPA 强大的自动化检测功能可以快速的对协议安全性进行验证，加快协议的开发和标准化的过程。

首先通过学习AVISPA工具的安装使用和HLPSL建模语言，熟悉AVISPA工具中的攻击思想和方法，掌握AVISPA仿真流程；然后利用AVISPA工具对两个安全协议实例建模分析，进行安全攻击仿真，验证其安全性；最后通过仿真数据对协议的安全性能进行分析。

1.4 章节安排

本次课题是通过基于AVISPA安全攻击仿真的研究，总结分析出安全协议的相关概念、基于AVISPA安全攻击仿真实现的方法。并通过对LTE（Long Term Evolution）网络中HeNB（Home eNodeB）和eNB（eNodeB）之间的切换认证和IEEE 802.16m中基于票据的快速切换的仿真，实现对不同协议的安全分析，同时达到熟练掌握基于AVISPA仿真的目的。根据本人所做工作，论文分五章，具体内容安排如下：

第一章：绪论。首先对安全协议的背景知识进行了概述，然后对安全协议形式化分析中的模型检测方法的发展和原理做了简要介绍，最后对本文的组织内容进行了说明；

第二章：AVISPA工具的介绍。首先介绍了AVISPA工具集的基本结构，对其四个模块分别作了简要的说明。然后针对两种不同的方式：命令行和SPAN，分别介绍了AVISPA的安装和使用方法；

第三章：高级协议描述语言HLPSL。先介绍了HLPSL语言的基础，通过一个简单的例子说明如何用HLPSL语言对协议进行建模分析，然后对HLPSL运用过程中需注意的问题做出总结归纳，最后分析了HLPSL是如何实现对安全协议攻击的检测；来.自/优尔论|文-网www.youerw.com/

第四章：协议安全攻击仿真的实现。利用AVISPA实现了对LTE网络中HeNB和eNB之间的切换认证和IEEE 802.16m中基于票据的快速切换认证两个方案的仿真，并对仿真结果做出相应的分析；

1.5 本章小结

本章介绍了安全协议的基本概念、安全协议的常见攻击方法]及设计规范等相关背景知识。并对安全协议形式化分析中的模型检测方法的发展做了一个说明，分析了模型检测方法的基本原理。最后，对本文的章节安排进行了介绍。