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

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

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

       数据独立技术使模型检测器的证明更加完整，因为它的应用使大协议的建模成为可能。

3．1 协议模型的扩展
 　　
　　为了解决验证的局限性，需要系统代理能够在实际类型保持有限的情况下，调用无限的不同的新鲜值。沿用Roscoe的方法，引入Manager进程扩展CSP协议模型。与以前的协议模型相比，该模型引入了Manager进程。此进程与Intruder进程相互配合以实现新鲜值的循环利用，因此可视为新鲜值的循环机制。可以说，该模型是对Roscoe文献的一个扩展和细化，可以证明其满足PosConjEqT′c条件：
   
　　(1)进程中的数据类型随机数Na、Nb和密钥Kdo均为数据独立类型。
   
　　(2)可信代理进程为标准类型进程，满足PosConjEqT′c条件。
  
　　(3)攻击者进程在明确推理系统中建立，并且其初始知识集不包含对类型T成员(除了常数C)的非等价测试，满足P0sConjEqT′c条件。

　　因此该系统中转换前全部行为可以用经过映射的、相应的有限系统描述。也正基于此，可以在无限新鲜值的产生过程中应用非单映射转换，从而将其简化为相应的有限过程，以形成完整的形式化描述。

3．2 协议各对象的描述
　　
　　对于每一个新鲜值引入对应的Manager进程，取消可信代理分发新鲜值的能力，只在单次运行期间存储新鲜值，并要求其在完成协议一次运行时“遗忘”所有存储的新鲜值。当新鲜值v不再被可信参与者所知(存储)时，称v被“遗忘”。攻击者能够存储在网络中所见的所有新信息。为了能够产生无限的新鲜值，可以对攻击者存储的新鲜值应用collasphag函数，从而启动所提出的新鲜值循环机制。即当新鲜值v在网络中被“遗忘”时可以被循环再利用。一旦该值被循环利用，相应的Manager进程可以在网络中再次将其作为新鲜值使用。

(1)可信进程
　　
　　在扩展的CSP协议模型中，进程描述如下：

　　扩展后的描述主要有三处变动：第一，进程被定义为递归进程，表示Initiator可以执行无限数量的序列运行；而在之前的模型描述中，进程在SKIP终止。第二，新鲜Nonce NA不再是参数，而是来自集合NonceF(通过定义，进程可以接收该集合中的任意值)；之后将会介绍Manager进程如何终止这些值的产生。第三，添加了close事件表示进程重新开始执行初始状态。该事件标志着进程一次运行的结束，在新鲜值的循环机制中发挥重要作用。

(2)Manager进程
   
　　Manger进程负责利用有限资源向网络提供无限的新鲜值。需要为每一种数据独立类型分别定义一个Manager进程，在上述的Yahalom协议中需要定义一个管理Nonce类型值的Manager进程——Nonce Manager和一个管理SESSionKey类型值的Manager进程——SessionKeyManager。本节研究Manager进程的CSP设计和实现。

　　将协议中的每一种数据独立类型T所拥有的值分为两类集合。第一类集合称为Foreground值，这些值被阿络视为新鲜值。第二类集合由Background值组成，表示类型r旧的或静态的值。当循环利用Intruder存储的新鲜值时，将使用这一集合进行映射。

　　可以说Manager进程是建模过程中的人造产物，并不代表实际对象而只代表了对于新鲜值的某种操作，主要完成触发“遗忘”值的循环和分发新鲜值的功能。

　　为了对Manager进程进行形式化描述，此处定义两个新的事件：
  
　　①ifclose．(v)：表示最后一个存储v的进程是否已经“遗忘”了v，如果“遗忘”为true，否则为false。
   
　　②replace．(v,b)：表示对intruder存储中含有v的所有信息进行操作，将v的所有实例替换为Background值b，即完成Collapse函数的非单映射。在相对意义上，v又会被视为新鲜，即实现了有限值产生无限新鲜值。

　　同时，使用下述策略确定循环值映射为哪个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脚本输入工具，完成验证。

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

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