密钥协商的目的是在不安全的通讯环境下实现参与者的安全会话。在这种环境中,存在着各种各样的攻击方式,它们可以是数学上的,也可以是物理方式上的;可以应用通讯技术的缺陷,也可以应用协议自身的漏洞。 攻击者不只允许截获、修正和删除协议规则的通讯信息,也允许控制一个或多个参与者, 甚至参加任何可能的信息,把协议的消息转向其它接受者等。这些攻击方法多样,也决定了分析密钥协商协议安全的复杂性。
目前,分析密钥协商协议安全性的方法有两种,一种是启示式的手段,一种是公理化的方法。所谓启示式手段,是指剖析者依据本人的经历和相关知识,利用本人掌握的攻击方法调查或验证协议的安全性,从协议的交互进程中寻觅安全破绽。应用启示式论证手段设计协议复杂而适用:只需依据既定的安全目的,提出一种协议,并地下承受剖析者的安全性剖析即可。但这种做法的弊端也不容无视:
(1)新的分析技术层出不穷, 在任何时候都有可能提出新的分析技术;(2)这种做法使我们很难相信协议真正的安全性。一旦协议被新的攻击方法攻破,该协议或者需要修改,或者被彻底摒弃,即使修改后可以达到安全要求, 但这种反复的修补也增加了人们对安全的担心。因此,学者们试图设计出可以准确刻画参与者和敌手特征的形式化安全模型,并在该模型下讨论协议的安全性,这就是公理化手段。
公理化手段用数学方法构造安全证明进程,以阐明待论证的协议到达了安全目的。爲了构造这一证明进程,剖析者首先需求建立一个安全模型,经过该模型定义协议的参与者以及参与者之间的互信关系、协议的安全参数和协议的通讯环境等。另外,模型还应定义敌手环境并爲协议设定契合实践状况的详细的安全目的。公理化手段分爲三种:基于信息论、基于计算复杂性以及基于符号:
(1)基于信息论的手段。假定敌手有有限的计算才能和计算资源。因而,信息论安全的协议也往往被称爲是无条件安全的。
(2)基于计算复杂性的手段。与基于信息论的手段相比,基于计算复杂性的手段对敌手的计算才能和计算资源有所限制。现实上,这更契合实践状况:假如不计代价地攻击某协议,耗费的代价比取得的机密信息的价值还高的话是没有意义的。这种论证办法通常将协议S的安全性归约到另一个成绩P的难解性上,使得,假如S的安全性被攻破,那麼就可以有方法处理P;假如P的难解性被公以为是成立的,那麼就可以保证S的安全性没有成绩。人们通常也把这种办法称爲可证明安全的手段。该办法也是目前大少数人以为的最牢靠的安全性论证手段。
(3)基于符号的手段。这种方法利用一些特定的语法规则定义安全模型。比如著名的BAN 逻辑和串空间理论都是这一方法的典型代表。
可证明安全性理论的应用价值是显而易见的: 研究者可以避开“极微本原”的难解性问题研究而把精力集中在如何将协议的安全性归约到该“极微本原”上。换句话说,只要相信“极微本原”的安全性,不必进一步分析协议即可相信其安全性。
尽管可证明安全性理论有如此优势,但也并非“完美”: 在安全模型的规划过程中,需要明确该模型会涵盖哪些攻击,而模型的设计者很难在一个模型中涵盖针对协议的所有攻击,这是因为,一方面设计者的知识和经验都有一定的局限性,不可能将所有的攻击都考虑到;另一方面,针对协议的攻击手段复杂晦涩,且随着网络和应用环境的改变, 新的攻击也会层出不穷。因此,针对安全模型本身的分析与改进也是信息安全领域一个重要的研究分支。每次安全模型的改进都有力地推动着协议安全性理论的发展。
