基于公钥的密码协议的形式化分析方法

1 密码协议分析的形式化方法概述

长期以来, 密码学专家一直依赖经验性的指导原则来设计密码协议, 但事实表明非形式化的设计方法很容易忽略掉一些微妙的、直觉难以发现的漏洞。形式化方法是采用各种形式化的语言或模型, 按照规定的假设、分析和验证方法, 来对密码协议的安全性进行验证, 形式化方法主要用于研究协议的性质, 这在很大程度上独立于协议所包含的密码算法的性质[1]。 (1) 基于代数分析的方法[2]。在1983年, Dolve与Yao首次提出将协议作为代数系统来研究。它们为密码协议建模的代数系统被称作Dolve-Yao模型, 对这一模型稍加修改, 就是目前大多数形式化方法仍在使用的模型。其中包括软件工具Interrogator、NRL协议分析器与Longley-Riboy工具。 (2) 基于逻辑推理的方法[3]。这种方法中最具影响力的一类就是BAN逻辑, 它由Burrows, Abadi和Needham于1989年提出。BAN逻辑的设计者希望给出每个消息的精确含义, 此外, BAN逻辑还给出一套逻辑推理规则。利用BAN逻辑, 其设计者曾经成功地发现了存在于CCITTX.509标准推荐草案。 (3) 借助图论的Strandspaee方法。1998年, Thayer, Herzog和Guttman提出了一种分析密码协议安全性的新方法。它利用图论方法来建立协议中因果关系的模型, 但本质上仍是基于代数的分析方法。各Strand通过消息的发送与接收相钩连, 钩连的整体称作Bundie, 它是一个用于描述Strand间通信的图结构。该方法根据主体所具有数据组成的模板来判断协议是否正确。并且该方法提出的理想的概念有助于状态可达性的归纳证明。

2 基于协议原型的协议设计方法

2.1 基于协议原型的协议设计方法

设计步骤如下: (1) 做好开发前的应用需求分析, 对所设计的协议将应用于什么系统, 以及使用的背景做详细的分析; (2) 依据系统的具体情况决定我们设计的协议使用基于对称密码体制还是非对称密码体制; (3) 看系统要求协议作双向认证还是单向认证, 然后再分别具体考虑协议中的实体使用的是哪种方式的认证:源认证 (OA) 、目标认证 (DA) 、暗认证 (IA) ; (4) 确定了单个实体的认证类型后, 再分别考虑实体的验证类型:被迫验证 (F) 、自我证明 (S) 、无验证 (O) ; (5) 接着根据 (3) 、 (4) 分别确定各实体使用的是哪种原型:IAφ、IAF、OAφ、OAS、OAF、DAφ、DAF', 然后将其组合得到协议的原型; (6) 根据上一步得到的原型, 得到协议的一般形式, 然后根据系统的具体要求向各个信息中添加加密因素, 在本步骤中要区分单一的认证协议和带有密钥建立的协议, 另外在设计协议时, 一定要注意原型可能存在的攻击及安全漏洞;对设计得协议进行检查, 减少协议中的冗余信息。

2.2 基于协议原型的协议设计方法的一个简单应用

我们不难发现只要得到了所要求设计的协议的认证原型, 从表中查出该原型所对应的最常用的密码协议, 再看对其相关的攻击和修改我们可以得到一个安全的协议。例如假设要设计的协议的认证原型是DAF, Ack-DAF, Ack, 那么分析可以很容易就得到了一个安全的协议。但是在有些原型在现有的密码协议中很少使用, 甚至至今都没有出现过, 那么自然在就查不到很多该原型相关信息, 这样就增加了协议设计的难度, 下面我们给出一个这样的例子。

Step I:首先我们假设本协议的应用需求分析工作已经作好, 具体如下。

(1) 协议中有两个通信实体, 一个是服务器B, 令一个就是用户A, 协议由用户发起。

(2) 本系统中实体都拥有自己的公钥和私钥, 双方没有预共享密钥。

(3) 服务器和用户均需要验证对方的身份, 并建立新的会话密钥。

(4) 服务器和用户间有一个预共享的密钥生成算法, 假设为:KAB=f (r A, r B) 。

Step II:由应用需求我们己经知道了, 本协议使用的是非对称密码体制。

Step III:由于用户是协议的发起人, 所以用户对服务器提出目标认证 (DA) , 而服务器应对用户做源认证 (OA) 。

Step IV:由于协议是要求做双向认证, 所以双方都必须得做被迫验证 (F) , 而且用户对服务器做的目标认证 (DA) 是必须要求服务器回答的。

S t e p V:根据上面的分析得到用户的原型是:ADF, Ack, 服务器的原型就是:OAF, 这样得到了协议的认证原型就是:

Step VI:得到原型ADF, Ack-OAF的一般形式。

(1) A→B:BPubkey{A, r A};

(2) A←B:r A, rB;

(3) A→B:APrikey{B, r B};。

Step VII:检查上面的协议中是否有冗余信息, 由于KAB的生成与Ar有关, 所以显然第三条信息中的rA是多余的应将其删除, 从而得到协议如下。

(1) A→B:BPubkey{A, r A};

(3) A→B:APrikey{B, r B, {A}KAB};。

3 结语

各种改进的逻辑方法虽然能够更准确地分析协议的安全性, 但它们本身并没有提出有关设计准则的建议, 因此不能直接有效地防止错误的产生。本文首先介绍了密码协议设计的一般性准则, 这些准则是在协议分析的过程中总结出来的, 以这些准则为基础给出了一种基于协议原型的设计方法。

摘要：目前, 基于密码技术的密码协议对于保证计算机网络安全起着十分重要的作用。这些密码协议的安全性直接影响着网络系统的安全性。形式化方法是一种当前较流行的用于分析密码协议安全性的方法。本文在形式化方法分析密码协议的基础上, 对基于公钥的密码协议进行原型抽象和分类, 给出了基于协议原型的协议设计方法, 并通过实例方法说明此种协议设计方法。

关键词：密码协议,形式化方法,公钥密码协议,保密性

参考文献

[1] 王全来, 王亚弟, 韩继红.密码协议形式化分析的计算合理性[J].计算机工程与应用, 2007, 21.

[2] 钱勇.认证协议设计与分析方法的研究[D].上海:上海交通大学, 2001.

[3] Paul Syverson and Paul C.van Oorshot.On Unifying some Authentication Pro-tocol Logics.IEEE Computer Society Symposium on Research in Security and Privacy, IEEE Computer Society, May1994:14～28.