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进程，如图1所示。

Initiator a的CSP进程描述如下：

响应者b与服务器s也有着相似的描述。

攻击者进程被描述为：

2 数据独立技术

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

2.1 一般的数据独立分析

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

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

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

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

2.2 Roscoe的数据独立技术