论文导读：与符号化方法相比较，我们使用形式化方法对协议进行描述不仅是为了简化描述过程，而是为了进一步利用形式化方法对协议进行验证：证明协议是正确的，即实现了为其制定的各种安全性目标。于是，证明一个协议的安全性问题就转化为证明上述项重写系统中不会产生这样的特定句子。另一种用于分析密码协议的形式化方法是建立在逻辑方法的基础之上。
关键词：形式化，密码协议，安全性
长期以来，密码学专家一直凭着丰富的经验来指导和设计密码协议，但事实表明这种设计方法很容易忽略掉一些微妙的、直觉难以发现的漏洞[1,2,3]。因此，将形式化方法应用到密码协议中是必然的结果。
1、形式化方法
形式化方法是一种用于描述系统性质的数学方法，它主要用于发现一个系统
中的歧义性、不一致性，与不完备性那么这个系统可以大到某个企业级的软件、硬件系统，也可以小到我们讨论范围内的某个协议。与符号化方法相比较，我们使用形式化方法对协议进行描述不仅是为了简化描述过程，而是为了进一步利用形式化方法对协议进行验证：证明协议是正确的，即实现了为其制定的各种安全性目标；或者分析出协议存在的缺陷。因此，形式化方法在给出描述协议的符号集合基础上，还会在该集合上定义各种关系与运算，以进一步揭示隐藏在协议内部的各种性质。
那么如何运用形式化方法证明协议的正确性呢？证明过程通常可以分为三个部分：第一、确定证明的目标，即协议需要实现何种安全目标；第二、建立协议的形式化模型，即给出协议的形式化描述；第三、证明。
虽然形式化方法为协议的验证工作提供了强大的证明手段，但是形式化方法并不能为协议的正确性提供百分之百的保证。这是因为：首先，协议正确性的证明总是在证明它的形式化方法所采用的特定假设下进行的，如果违背了这些假设，那么原先的证明结果也就失去了意义。
2、密码协议的形式化分析方法
目前形式化方法主要用于研究协议的性质，这在很大程度上独立于协议所包含的密码算法的性质，因此下文中我们总是假设协议所使用的密码算法是不可破解的。
(1) 基于代数分析的方法
在1983年，Dolve与Yao首次提出将协议作为代数系统来研究。它们为密码协议建模的代数系统被称作Dolve-Yao模型，对这一模型稍加修改，就是目前大多数形式化方法仍在使用的模型[4]。
在Dolve-Yao模型中，协议的交互过程采用代数方法表示：消息的接收与发送分别对应一组代数表达式以及相应的变换规则;网络被认为是处于入侵者的控制之下：入侵者可以读取所有的信息流，并具有创建、修改与破坏消息的能力；此外，即入侵者还可以执行任何系统合法用户能够执行的操作。但同时假设：在初始阶段，入侵者不知道任何关于系统合法用户的秘密信息。这样，入侵者就可以将协议交互过程看作产生句子(消息)的机器，并且这些句子满足特定的重写(rewrite)规则，例如：句子中具有相同密钥的加密与解密操作符可以互相抵消。因此，入侵者的目标就是找到一个揭示秘密的特定句子。于是，证明一个协议的安全性问题就转化为证明上述项重写系统中不会产生这样的特定句子。
但是Dolve-Yao模型只针对某种特定形式的协议，即，级联协议与名称戳协议。并且后来Even与Goldreich发现，如果对上述协议稍微放宽条件，那么协议的安全性问题就成为数学上不可判定的问题。因此，这方面的理论工作没有进一步拓展。
然而稍后，用于分析协议安全性的工具开发得到了人们的重视，并且这些工作大都基于Dolve-Yao模型。这其中包括软件工具Interrogator， N RL协议分析器fill与Longley-Rigby工具。在这些工作的早期阶段，研究人员所开发的工具成功地发现了一些人I分析难以发现的协议漏洞。例如，研究人员利用NRL协议分析器发现了Simmons选择性广播协议中的一个漏洞；利用Longley-Rigby工具发现了一个银行协议中的漏洞。而近年来研究人员主要致力于在Dolve-Yao模型之上实现模型检测技术与定理证明技术。这方面的工作开端于Lowe利用一个具有普遍意义的模型检测器，即FDR，发现了针对Needham-Schroeder公钥协议的中间人攻击。自此，利用模型检测器与定理证明器来分析协议安全性问题的工作得到了人们的普遍重视。
(2)基于逻辑推理的方法
另一种用于分析密码协议的形式化方法是建立在逻辑方法的基础之上。这种方法中最具影响力的一类就是BAN逻辑，它由Burrows, Abadi和Needham于1989年提出。与上述Dolve-Yao模型不同的是，虽然BAN逻辑考虑到入侵者存在的可能性，但是它不检查未授权情况下的秘密泄漏，而主要研究可信主体(principal)在协议执行过程中所持信念(belief)的演化。
BAN逻辑的设计者希望给出每个消息的精确含义，因此它们将一个消息转换为一个逻辑表达式，这个逻辑表达式是原有消息的一个理想化模式。此外，BAN逻辑还给出一套逻辑推理规则。在利用BAN逻辑对协议进行分析之前，首先需要对协议进行理想化处理，然后还需要给出协议主体具有的初始信念假设。在协议执行过程中，协议主体通过接收消息能够增加较为直观的知识，然后根据上述初始假设的信念与协议执行过程中得到的知识，利用BAN逻辑给出的推理规则就可以得到此协议步骤下直观上难以得到的深层次的知识与信念。如果在协议执行结束后，通过上述推理所得到的信念能够满足鉴别协议的安全需求，例如共享会话密钥，那么就证明该协议是正确的。如果不能满足，则说明这个协议可能存在漏洞。利用BAN逻辑，其设计者曾经成功地发现了存在于CCITT X.509标准推荐草案中的一个以前未被发现的漏洞。
但是BAN逻辑也存在一些问题，例如：语义模糊、理想化过程局限、初始假设不尽合理、以及推理规则不够完善，使得利用BAN逻辑己证明为安全的协议，后来却被发现存在漏洞。这样一来，人们只能相信BAN逻辑证明协议的不安全性，而不能相信其证明的协议安全性。
1/2 1 2 下一页 尾页 |
