基于ProVerif的安全攻击仿真+源代码(2)
3.1 协议建模 12
3.1.1 声明部分 12
3.1.2 宏过程 14
3.1.3 进程 14
3.2 安全属性 16
3.2.1 可达性与保密性 16
3.2.2 对应的断言 16
3.3 握手协议分析 17
3.4 本章小结 18
4 SE-AKA协议安全攻击仿真的实现 19
4.1 LTE网络中SE-AKA协议 20
4.1.1 LTE网络架构 20
4.1.2 椭圆曲线Diffie-Hellman 21
4.1.3 SE-AKA协议 21
4.2 形式化验证 25
4.2.1 保密性 27
4.2.2 认证性 28
4.2.3 匿名性 32
4.3 本章小结 34
结 论 35
致 谢 36
参考文献37
附录1 握手协议 39
附录2 握手协议的完整代码 40
附录3 改进后的握手协议的完整代码 42
1 绪论
1.1 安全协议
1.1.1 安全协议的基本概念
协议[1,2] ，指参与实体要遵守的规则和标准，即参与实体为完成某项特定任务而采取的一系列动作的集合。
协议具有的特点[3]如下：（1）协议的每个参与者都必须知道所要完成的所有协议步骤，并认可且遵循它；（2）协议本身定义必须是明确完善的；（3）协议必须存在一个具体目标，即协议最终需达到的目的。
而安全协议也称密码协议[3,4]，是基于密码学的协议，它使用密码算法来达到密钥分配[4]、密钥交换[4]、身份认证[4] 、访问控制等目标。为方便描述，本文只采用了“安全协议”这一概念。
1.1.2 安全协议的常见攻击
对协议本身的攻击可以分为被动攻击[5]和主动攻击[5]。
被动攻击，通常不改变系统中的数据，只是读取数据，从中获利。被动攻击包括嗅探、信息收集等攻击方法。由于没有篡改信息，所以留下可供审计的痕迹很少或根本没有，基本上很难被发现。
主动攻击，通常要比被动威胁严重得多，因为主动威胁通常要有意地改动数据或生成伪造数据。主动攻击主要包括中断、篡改、伪造。
我们知道，在实际应用中，协议遭受到的攻击是多种多样的，常见的攻击方法[4]有：重放攻击[5] 、类型缺陷攻击[5]、并行会话攻击[5] 。
1.1. 安全协议的分类
作为保障网络信息安全的关键手段，在网络通信各个领域，安全协议简直无所不在。它具有应用广泛、种类繁多、安全目标多样化的特点，目前没有统一明确的标准对其进行分类。目前，主要根据协议的加密体制、协议有无可信第三方、处于ISO 网络参考模型的层次和协议的功能这四个方面对协议进行分类。通常，我们采用按照协议的功能来对协议进行划分，为以下四类[6,7,8,10]：
（1）密钥交换协议[2,9]。这类协议用于在协议的两个或多个主体之间协商出一个用于对话的秘密密钥。安全协议就是通过该秘密密钥和相应的密码算法来确保通信中信息的机密性。协议中的密码算法可采用公开密钥密码体制或对称密钥密码体制。大多数密钥交换协议的设计原型是Diffie-Hellman[2,9]协议。
（2）认证协议[2,9]。在网络通信中，认证协议是最常用的协议类型。认证协议包括身份认证协议、消息认证协议、数据源认证协议和数据目的认证协议等，它主要用来认证参与者的身份，保证消息的完整性，认证消息的来源和目的地，并且能够用来应对篡改攻击、假冒攻击[9,11]和DoS攻击[7,9,11]等。通常，根据认证的方式划分为单向认证协议和双向认证协议。