[转载]安全协议浅谈
信息来源： 新临天下--网络技术论坛1.安全协议的基本概念
首先需要指出，本文所指的安全协议特指使用密码学技术的密码协议（cryptographic protocol）。所谓协议，就是两个或者两个以上的参与者为完成某项特定的任务而采取的一系列步骤。这个定义包含三层含义：
1) 协议自始至终是有序的过程，每一个步骤必须执行，在前一步没有执行完之前，后面的步骤不可能执行；
2) 协议至少需要两个参与者；
3) 通过协议必须能够完成某项任务。
密码协议是使用密码学技术的协议，协议的参与者可能是可以信任的人，也可能是攻击者和完全不信任的人。密码协议包含某种密码算法。在网络通信中最常用的、基本的密码协议按照其完成的功能可以分成以下三类：
1) 密钥交换协议
一般情况下是在参与协议的两个或者多个实体之间建立共享的秘密，通常用于建立在一次通信中所使用的会话密钥。协议可以采用对称密码体制，也可以采用非对称密码体制，例如Diffie-Hellman密钥交换协议。
2) 认证协议
认证协议中包括实体认证（身份认证）协议、消息认证协议、数据源认证和数据目的认证协议等，用来防止假冒、篡改、否认等攻击。
3) 认证和密钥交换协议
这类协议将认证和密钥交换协议结合在一起，是网络通信中最普遍应用的安全协议。常见的有Needham-Schroeder协议、分布认证安全服务（DASS）协议、ITU-T X.509认证协议等等。
2.安全协议的安全性
安全协议是许多分布式系统安全的基础，确保这些协议的安全运行是极为重要的。大多数安全协议只有为数不多的几个消息传递，其中每一个消息都是经过巧妙设计的，消息之间存在着复杂的相互作用和制约；同时，安全协议中使用了多种不同的密码体制，安全协议的这种复杂的情况导致目前的许多安全协议存在安全缺陷。造成协议存在安全缺陷的原因主要有两个：一是协议设计者误解或者采用了不恰当的技术；二是协议设计者对环境要求的安全需求研究不足。因此，对协议的安全性进行分析和研究是一个重要的课题。
由于实际应用的安全协议产生缺陷的原因是多种多样的，所以很难有一种通用的分类方法将安全协议的安全缺陷进行分类。S. Gritzalis和D. Spinellis根据安全缺陷产生的原因和相应的攻击方法对安全缺陷进行了分类：
基本协议缺陷
是指在安全协议的设计中没有或者很少防范攻击者的攻击。
口令/密钥猜测缺陷
这类缺陷产生的原因是用户往往从一些常用的词中选择其口令，从而导致攻击者能够进行口令猜测攻击；或者选取了不安全的伪随机数生成算法构造密钥，使攻击者能够恢复该密钥。
陈旧（stale）消息缺陷
主要是指协议设计中对消息的新鲜性没有充分考虑，从而使攻击者能够进行消息重放攻击，包括消息源的攻击、消息目的的攻击等等。
并行会话缺陷
协议对并行会话攻击缺乏防范，从而导致攻击者通过交换适当的协议消息能够获得所需要的信息。包括并行会话单角色缺陷、并行会话多角色缺陷等等。
内部协议缺陷
协议的可达性存在问题，协议的参与者中至少有一方不能够完成所有必须的动作而导致的缺陷。
密码系统缺陷
协议中使用的密码算法和密码协议导致协议不能完全满足所要求的机密性、认证等需求而产生的缺陷。
安全协议的安全性是一个很难解决的问题，许多广泛应用的安全协议后来都被发现存在安全缺陷。因此，从安全协议的分析和设计角度来看，我们都不能够存在轻信和盲从心理，而应当对协议的安全性作出认真的分析。
3.安全协议的分析
目前，对安全协议进行分析的方法主要有两大类：一类是攻击检验方法；一类是形式化的分析方法。
所谓攻击检验方法就是搜集使用目前的对协议的有效攻击方法，逐一对安全协议进行攻击，检验安全协议是否具有抵抗这些攻击的能力。在分析的过程中主要使用自然语言和示意图，对安全协议所交换的消息进行剖析。这种分析方法往往是非常有效的，关键在于攻击方法的选择。
形式化的分析方法是采用各种形式化的语言或者模型，为安全协议建立模型，并按照规定的假设和分析、验证方法证明协议的安全性。目前，形式化的分析方法是研究的热点，但是就其实用性来说，还没有什么突破性的进展。
近几年来，密码学家提出了许多关于安全协议的形式化分析方法，以检验协议中是否存在安全缺陷。总的来说，协议的形式化分析技术可以概括为四大类：
<类型1> 使用通用的、不是为分析安全协议专门设计的形式化描述语言和协议校验工具建立安全协议的模型并进行校验。
其主要思想是将安全协议看作一般的协议，并试图证明协议的正确性。采用的工具和模型与验证一般协议的类似，例如使用有限状态图、Petri网模型、LOTOS语言等等。这种方法的一个主要缺点是仅证明协议的正确性而不是安全性。
<类型2> 安全协议的设计者设计专门的专家系统来制定协议的校验方案并进行协议检验，从而对协议的安全性作出结论。
其主要思想是根据协议的设计开发专用的专家系统，使用专家系统发现协议是否能够达到不合理的状态（比如密钥的泄露等等）。这种技术能够很好的识别缺陷但是不能证明协议的安全性，也不可能发现未知的缺陷。
<类型3> 使用基于知识和信念的逻辑来建立所分析的协议的安全需求模型。
这种方法是目前为止使用最广泛的一种方法，最著名的是BAN逻辑。BAN逻辑是一个形式逻辑模型，进行基于知识和信任的分析。BAN逻辑假设认证是完整性和新鲜度的函数，使用逻辑规则来对协议的属性进行跟踪和分析。一般来说，BAN逻辑只能推出认证的结果，而不能对一般的安全性进行证明。
使用BAN逻辑分析安全协议的步骤如下：
（1） 协议的理想化转化
（2） 假设所有的协议初始状态
（3） 使用逻辑规则对系统的状态作出断言
（4） 运用逻辑原理得到关于信任的断言
<类型4> 基于密码学系统的代数特性开发协议的形式化模型
这种方法是将安全协议系统当作一个代数系统模型，表示出协议的参与者的各种状态，然后分析某种状态的可达性。Michael Merritt已经证明了代数模型可以用来分析安全协议。美国海军研究实验室（Navy Research Lab.）开发的协议分析器是这种方法中最成功的一个应用，可以用来在各种协议中寻找新的和已知的缺陷。
安全协议的形式化分析方法本身是研究的热点，但是其应用并不是非常广泛，主要原因是安全协议的安全性的形式化过程比较困难。
需要指出的是，由于安全协议本身的复杂性，目前并没有一种方法能够给出安全协议安全性的充分而且必要的理论证明。上述每一类方法都有不同的侧重点，或者说或多或少地存在不足之处，我们在使用上述方法分析安全协议的时候，应当仔细分析协议的特点、应用环境和需求，综合使用这些分析方法，以得到一个比较合理的结果。
页:
[1]