1.4 章节安排 5

1.5 本章小结 5

2 AVISPA工具的介绍 6

2.1 AVISPA的基本结构 6

2.2 AVISPA的安装和使用 8

2.2.1 命令方式 8

2.2.2 SPAN方式 9

2.3 本章小结 11

3 高级协议描述语言HLPSL 13

3.1 HLPSL基础 13

3.1.1 基础角色 14

3.1.2 转换过程 14

3.1.3 混合角色 15

3.1.4 高层角色 16

3.1.5 实例化 16

3.2 HLPSL注意事项 17

3.3 HLPSL对协议攻击的检测 20

3.4 本章小结 21

4 协议安全攻击仿真的实现 22

4.1 LTE网络中HeNB和eNB之间的切换认证的仿真 22

4.1.1 方案介绍 22

4.1.2 安全仿真实现 24

4.1.3 安全仿真结果分析 26

4.2 IEEE 802.16M中基于票据的快速切换认证的仿真 29

4.2.1 方案介绍 30

4.2.2 安全仿真实现 31

4.2.3 安全仿真结果分析 34

4.3 本章小结 36

结束语 37

致 谢 38

参考文献 39

研究成果 41

附录1 HLPSL符号和关键字的说明 42

附录2 LTE网络中HENB和ENB之间的切换认证方案的IF说明 44

附录3 IEEE 802.16M中基于票据的快速切换认方案的IF说明 49

1 绪论

1.1 安全协议概述

1.1.1 安全协议的基本概念

协议[1]指参与各方要遵守的规范和约定，两个或者两个以上的参与者为完成某项特定的任务而采取的一系列动作的集合。协议还具有如下特点：（1）协议中每个实体都必须了解协议，并预先知道所要完成的所有步骤；（2）协议中的每个可信实体都必须同意并遵循它；（3）协议不能模糊，每一步都必须明确定义且不会引起误解；（4）协议必须是完整的，对每种可能情况必须规定具体的动作。

而安全协议[2]也称作密码协议，是以密码学为基础的消息交换协议，其目的是在网络环境中提供各种安全服务。需满足认证性、私密性、完整性、不可否认性。常见分类有密钥交换协议、认证协议、认证和密钥交换协议、电子商务协议。

1.1.2 安全协议的常见攻击

一般对协议自身的攻击可以分为主动攻击和被动攻击[3]。

主动攻击包含攻击者访问他所需信息的故意行为，包含对数据流的某些修改，或者生成一个假的数据流，包括拒绝服务攻击、分布式拒绝服务、信息篡改、资源使用、欺骗、伪装、重放等攻击方法。