数据独立技术在CSP协议模型中的设计

1996年，Lowe首先使用通信顺序进程CSP和模型检测技术分析NSPK(Needham-Schroeder Public Key)协议，并成功发现了协议中的一个中间人攻击行为。随后，Roscoe对CSP和FDR(Fallures-Divergence Refinenent)的组合做了进一步研究，认为CSP方法是形式分析安全协议的一条新途径。事实证明，CSP方法对于安全协议分析及发现安全协议攻击非常有效。但是类似FDR的模型检测通常受NONce、Key等新鲜值大小的限制，而在实际执行中所需的数据值比这大得多。使用数据独立技术使结点能够调用无限的新鲜值以保证实例无限序列的运行。本文将研究Roscoe这些理论，对CSP协议模型进行设计与实现，从而解决有限检测的问题。

1 CSP协议模型
　　
　　在CSP模型中，协议参与者被表示为CSP的进程(process)，消息被表示为事件(event)，进而协议被表示为一个通信顺序进程的集合。

CSP协议模型由一些可信的参与者进程和入侵者进程组成，进程并行运行且通过信道交互。以NSPK协议为例。该协议的CSP模型包括两个代理(初始者a，响应者b)和一个能执行密钥产生、传送或认证服务的服务器s，它们之间通过不可信的媒介(入侵者)通信，所以存在四个CSP进程．

　 Initiator a的CSP进程描述如下：

响应者b与服务器s也有着相似的描述。
　　
　　攻击者进程被描述为：

　　2 数据独立技术

　　数据独立技术是本论文的关键技术．它起源于Lazic的数据独立研究。

2．1 一般的数据独立分析

　　如果一个进程P对于类型T没有任何限制，则P对于T类型是数据独立的。此时，T可以被视为P的参数。

通常，数据独立分析是为以类型T为参数的验证问题发现有限阈值。如果对于T的阈值，可以验证系统成立，则对于所有较大的T值也可以验证系统成立。这点对于很多问题都是成立的。

安全协议模型中的许多特征都可以被视为数据独立实体。常见的key、nonce可以作为模型中进程的参数。

对依赖nonce和密钥(和依赖协议的其他简单数据对象)惟一性的安全协议进行的阀值计算，主要是发现进程存储量的阈值，并不能直接解决验证的局限性，也就不能直接应用于安全协议模型。

2．2 Roscoe的数据独立技术
　　
　　上节证明了一般目标的数据独立结果不适用于安全协议分析。所以Roscoe对这些结果进行推论。发展了数据独立技术。本节将介绍几条对课题研究具有重要理论意义的推论。

(1)基本原则

　　对一般数据独立分析结果进行推论所基于的基本原则也是证明数据独立理论最重要的方法。即对进程P的参数类型T应用Conapsint函数φ建立映射关系，证明映射前P(T)的行为经过函数转换，是P(φ(T))行为的子集。
　　
　　对于安全协议主要研究进程的迹。可以很直观地发现如果Collapsing函数φ是单映射的(T的所有成员被映射为不同值)，并应用于进程P的参数类型T上(P对于T数据独立)，则因为T的所有成员被映射为不同值，所以映射前的行为等价于映射后的行为，如式(1)所示：

　如果使用的Collapsing函数φ为非单映射函数，则有可能改变等价测试结果，产生不等式(2)：

该不等式只适用于变量，对于程序中的常量，情况有所不同。因此提出下面两个条件：
　　PosConjEqT(Positive Conjunetions of Equality teSTs)条件由Lazic提出，该条件可以使变量使用

非单映射函数的进程再度满足等式(1)。
　　对于常量虽然不能重新满足等式(1)，但可满足不等式(3)：

协议的某些方面可能并不满足PosConjEqT条件，如代理进程可能需要执行拥有常量(例如名字)的不等式测试。因此，针对常量集C定义PosConjEqT′c条件如下：
　　
　　如果进程P对于常量集C满足下列条件，则称进程P满足PosConjEqT′c条件。该条件满足PosConjEqT条件，但与PosConjEqT条件的不同之处是：对于至少包含常量集C一个成员的等价测试，P可能拥有non-STOP结果。(2)明确推理系统

　　协议模型中的代理进程是标准类型进程且易于进行满足PosConjEqT′c条件的特性检测。但Intruder进程可以依靠推理系统指定产生或破坏信息的规则，这一特性决定了其更为复杂。
　　
　　如果推理系统满足这样的条件，即对于类型间的任意函数φ：T1→T2，只要(X,f)是系统产生的适用于类型T1推论，则(φ(X)，φ(f))就是适用于T2的推论，进而称该推理系统与这些类型参数T明确相关。其中要求推理的产生在T上对称(也就是平等对待T的所有成员)并且对出现在推理左边的T成员不再具有不等的要求。

从上述定义可以确定这样的性质：如果在明确推理系统中建立攻击者，并且攻击者的初始知识集不包含对于类型T成员(除了常数C)的非等价测试，那么