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

同时，使用下述策略确定循环值映射为哪个Background值：对于每一种数据独立类型T，定义两个不同的Background值TPk和TBu。将所有intruder所知的Foreground值映射为TBk，不知的映射为TBk。

通过上述定义和策略研究，描述Manager进程如下：

　　其中，T表示数据类型，TF代表该数据类型的Foreground集合，TBk和TBa分别代表不同的Background值TBk和TBu。

为了编译阶段的效率，将其分解为并行结构。因为对每一个新鲜值的控制都是独立的。在Yahalom协议中，假设定义新鲜Nonce集为{N1，N2}，新鲜SessionKey集为{K1}，则可建模为下面的并行结构：

其中，T表示数据类型，TF代表该数据类型的Foreground集合，TBk和TBa分别代表不同的Background值TBk和TBu。

为了编译阶段的效率，将其分解为并行结构。因为对每一个新鲜值的控制都是独立的。在Yahalom协议中，假设定义新鲜Nonce集为{N1，N2}，新鲜SessionKey集为{K1}，则可建模为下面的并行结构：

(3)Intmdez进程

扩展Intruder进程，使其与Manager进程一起形成(数据独立类型)新鲜值循环机制。当启动新鲜值v的循环机制时，对存储中含有v的所有信息进行操作，将v的所有实例替换为Background值b。

沿用在Manager进程中的定义和研究，Intruder进程描述如下：

4 数据独立技术在CSP协议模型中的实现
　　
　　CSPM是CSP的机器可读语言，适用于FDR、ProBE等各种工具。一般的程序语言以可执行的形式描述算法。CSPM也包含功能程序语言，但是其主要目标不同：此处它以自动操作的形式支持并行系统的描述。因此，CSPM脚本通常被定义为一组进程而不是程序。作为基础层，CSPM脚本还支持表达式和函数。为了能够将扩展后的协议模型输入验证工具ProBE并完成验证，需要将扩展CSP描述编写成CSPM脚本(因为ProBE编译接口无法扩展)。因此在编写CSPM脚本过程中定义了相应的新事件、新进程以实现扩展，最终将手工完成的CSPM脚本输入工具，完成验证。

本文的研究确保了协议中每个代理都可以执行无限数量的序列运行，解决了有限检测问题。但是，并行运行的代理实体数量的无限问题没有得到解决；如果在模型中没有发现攻击。不能够证明在更高的并行度不存在攻击。这也是今后的一个研究方向。

数据独立技术可以在一定的协议范围内使用，不可以直接运用在包含时戳的协议中。因为执行的典型操作超出了数据独立范围，如使用对比算子xy决定时戳y是否比时戳x旧。扩展研究处理时戳可以作为未来的研究方向。