1996年，Lowe首先使用通信顺序进程CSP和模型检测技术分析NSPK(Needham-Schroeder Public Key)协议，并成功发现了协议中的一个中间人行为。随后，Roscoe对CSP和FDR(Fallures-Divergence Refinenent)的组合做了进一步研究，认为CSP方法是形式分析安全协议的一条新途径。事明，CSP方法对于安全协议分析及发现安全协议非常有效。但是类似FDR的模型检测通常受NONce、Key等新鲜值大小的，而在实际执行中所需的数据值比这大得多。使用数据技术使结点能够调用无限的新鲜值以保例无限序列的运行。本文将研究Roscoe这些理论，对CSP协议模型进行设计与实现，从而解决有限检测的问题。1996年，Lowe首先使用通信顺序进程CSP和模型检测技术分析NSPK(Needham-Schroeder Public Key)协议，并成功发现了协议中的一个中间人行为。随后，Roscoe对CSP和FDR(Fallures-Divergence Refinenent)的组合做了进一步研究，认为CSP方法是形式分析安全协议的一条新途径。事明，CSP方法对于安全协议分析及发现安全协议非常有效。但是类似FDR的模型检测通常受NONce、Key等新鲜值大小的，而在实际执行中所需的数据值比这大得多。使用数据技术使结点能够调用无限的新鲜值以保例无限序列的运行。本文将研究Roscoe这些理论，对CSP协议模型进行设计与实现，从而解决有限检测的问题。
在CSP模型中，协议参与者被表示为CSP的进程(process)，消息被表示为事件(event)，进而协议被表示为一个通信顺序进程的集合。
CSP协议模型由一些可信的参与者进程和入侵者进程组成，进程并行运行且通过信道交互。以NSPK协议为例。该协议的CSP模型包括两个代理(初始者a，响应者b)和一个能执行密钥产生、传送或认证服务的服务器s，它们之间通过不可信的媒介(入侵者)通信，所以存在四个CSP进程，如图1所示。
如果一个进程P对于类型T没有任何，则P对于T类型是数据的。此时，T可以被视为P的参数。
通常，数据分析是为以类型T为参数的验证问题发现有限阈值。如果对于T的阈值，可以验证系统成立，则对于所有较大的T值也可以验证系统成立。这点对于很多问题都是成立的。
安全协议模型中的许多特征都可以被视为数据实体。常见的key、nonce可以作为模型中进程的参数。
对依赖nonce和密钥(和依赖协议的其他简单数据对象)惟一性的安全协议进行的阀值计算，主要是发现进程存储量的阈值，并不能直接解决验证的局限性，也就不能直接应用于安全协议模型。
上节证明了一般目标的数据结果不适用于安全协议分析。所以Roscoe对这些结果进行推论。发展了数据技术。本节将介绍几条对课题研究具有重要理论意义的推论。
对一般数据分析结果进行推论所基于的基本原则也是证明数据理论最重要的方法。即对进程P的参数类型T应用Conapsint函数建立映射关系，证明映射前P(T)的行为经过函数转换，是P((T))行为的子集。
对于安全协议主要研究进程的迹。可以很直观地发现如果Collapsing函数是单映射的(T的所有被映射为不同值)，并应用于进程P的参数类型T上(P对于T数据)，则因为T的所有被映射为不同值，所以映射前的行为等价于映射后的行为，如式(1)所示：
如果使用的Collapsing函数为非单映射函数，则有可能改变等价测试结果，产生不等式(2)：
PosConjEqT条件：如果进程P中的每一次等价测试失败都会引发STOP进程，则称进程P满足PosConjEqT条件。
协议的某些方面可能并不满足PosConjEqT条件，如代理进程可能需要执行拥有常量(例如名字)的不等式测试。因此，针对常量集C定义PosConjEqTc条件如下：
如果进程P对于常量集C满足下列条件，则称进程P满足PosConjEqTc条件。该条件满足PosConjEqT条件，但与PosConjEqT条件的不同之处是：对于至少包含常量集C一个的等价测试，P可能拥有non-STOP结果。
协议模型中的代理进程是标准类型进程且易于进行满足PosConjEqTc条件的特性检测。但Intruder进程可以依靠推理系统指定产生或信息的规则，这一特性决定了其更为复杂。
如果推理系统满足这样的条件，即对于类型间的任意函数：T1T2，只要(X,f)是系统产生的适用于类型T1推论，则((X)，(f))就是适用于T2的推论，进而称该推理系统与这些类型参数T明确相关。其中要求推理的产生在T上对称(也就是平等对待T的所有)并且对出现在推理左边的T不再具有不等的要求。
从上述定义可以确定这样的性质：如果在明确推理系统中建立者，并且者的初始知识集不包含对于类型T(除了C)的非等价测试，那么该进程满足PosConjEqTc条件(并且因此，整个协议模型满足网络其他部分的条件)。
可以看出系统成分是否满足上述性质对研究至关重要。只有满足这些条件才能够在协议分析的CSP模型中构造更为复杂的事件。
Roscoe在文献中引入了NM进程，负责产生系统所需的无眼新鲜值。那么在以前运行中，一个进程要在每一次输出通信时产生一个新鲜值v；而现在就会将这次通信变为向该进程输入v，并且要求其与相应的NM进程同步。
为了满足新鲜值的惟一性和新鲜性，引入的NM进程需进行下列操作：存储所有发送的新鲜值，相同的新鲜值只发送一次，不发送属于者的新鲜值。显然这些操作并不满足PosConjEqT条件。
Roscoe没有单独使用NM进程进行无限新鲜值的分发，而是应用数据技术，在NM进程中执行Collapse转换，通过转换从有限集生成无限新鲜值。
Roscoe的数据技术提供了这样的理论基础：若系统的所有成分满足PosConjEqTc条件，则大协议系统中转换前的全部行为(就系统迹而言)可以用经过映射的相应的有限系统描述。这一技术了可以在大协议中应用非单映射转换，将问题简化为相应的有限系统。
为了解决验证的局限性，需要系统代理能够在实际类型保持有限的情况下，调用无限的不同的新鲜值。沿用Roscoe的方法，引入Manager进程扩展CSP协议模型。以Yahalom协议为例，扩展后模型如图2所示。
与以前的协议模型相比，该模型引入了Manager进程。此进程与Intruder进程相互配合以实现新鲜值的循环利用，因此可视为新鲜值的循环机制。可以说，该模型是对Roscoe文献的一个扩展和细化，可以证明其满足PosConjEqTc条件：
(3)者进程在明确推理系统中建立，并且其初始知识集不包含对类型T(除了C)的非等价测试，满足P0sConjEqTc条件。
因此该系统中转换前全部行为可以用经过映射的、相应的有限系统描述。也正基于此，可以在无限新鲜值的产生过程中应用非单映射转换，从而将其简化为相应的有限过程，以形成完整的形式化描述。
对于每一个新鲜值引入对应的Manager进程，取消可信代理分发新鲜值的能力，只在单次运行期间存储新鲜值，并要求其在完成协议一次运行时“遗忘”所有存储的新鲜值。当新鲜值v不再被可信参与者所知(存储)时，称v被“遗忘”。者能够存储在网络中所见的所有新信息。为了能够产生无限的新鲜值，可以对者存储的新鲜值应用collasphag函数，从而启动所提出的新鲜值循环机制。即当新鲜值v在网络中被“遗忘”时可以被循环再利用。一旦该值被循环利用，相应的Manager进程可以在网络中再次将其作为新鲜值使用。
扩展后的描述主要有三处变动：第一，进程被定义为递归进程，表示Initiator可以执行无限数量的序列运行；而在之前的模型描述中，进程在SKIP终止。第二，新鲜Nonce NA不再是参数，而是来自集合NonceF(通过定义，进程可以接收该集合中的任意值)；之后将会介绍Manager进程如何终止这些值的产生。第三，添加了close事件表示进程重新开始执行初始状态。该事件标志着进程一次运行的结束，在新鲜值的循环机制中发挥重要作用。
将协议中的每一种数据类型T所拥有的值分为两类集合。第一类集合称为Foreground值，这些值被阿络视为新鲜值。第二类集合由Background值组成，表示类型r旧的或静态的值。当循环利用Intruder存储的新鲜值时，将使用这一集合进行映射。
可以说Manager进程是建模过程中的人造产物，并不代表实际对象而只代表了对于新鲜值的某种操作，主要完成触发“遗忘”值的循环和分发新鲜值的功能。
①ifclose.(v)：表示最后一个存储v的进程是否已经“遗忘”了v，如果“遗忘”为true，否则为lse。
②replace.(v,b)：表示对intruder存储中含有v的所有信息进行操作，将v的所有实例替换为Background值b，即完成Collapse函数的非单映射。在相对意义上，v又会被视为新鲜，即实现了有限值产生无限新鲜值。
同时，使用下述策略确定循环值映射为哪个Background值：对于每一种数据类型T，定义两个不同的Background值TPk和TBu。将所有intruder所知的Foreground值映射为TBk，不知的映射为TBk。
为了编译阶段的效率，将其分解为并行结构。因为对每一个新鲜值的控制都是的。在Yahalom协议中，假设定义新鲜Nonce集为{N1，N2}，新鲜SessionKey集为{K1}，则可建模为下面的并行结构：
扩展Intruder进程，使其与Manager进程一起形成(数据类型)新鲜值循环机制。当启动新鲜值v的循环机制时，对存储中含有v的所有信息进行操作，将v的所有实例替换为Background值b。
CSPM是CSP的机器可读语言，适用于FDR、ProBE等各种工具。一般的程序语言以可执行的形式描述算法。CSPM也包含功能程序语言，但是其主要目标不同：此处它以自动操作的形式支持并行系统的描述。因此，CSPM脚本通常被定义为一组进程而不是程序。作为基础层，CSPM脚本还支持表达式和函数。为了能够将扩展后的协议模型输入验证工具ProBE并完成验证，需要将扩展CSP描述编写成CSPM脚本(因为ProBE编译接口无法扩展)。因此在编写CSPM脚本过程中定义了相应的新事件、新进程以实现扩展，最终将手工完成的CSPM脚本输入工具，完成验证。
本文的研究确保了协议中每个代理都可以执行无限数量的序列运行，解决了有限检测问题。但是，并行运行的代理实体数量的无限问题没有得到解决；如果在模型中没有发现。不能够证明在更高的并行度不存在。这也是今后的一个研究方向。
数据技术可以在一定的协议范围内使用，不可以直接运用在包含时戳的协议中。因为执行的典型操作超出了数据范围，如使用对比算子xy决定时戳y是否比时戳x旧。扩展研究处理时戳可以作为未来的研究方向。数据技术可以在一定的协议范围内使用，不可以直接运用在包含时戳的协议中。因为执行的典型操作超出了数据范围，如使用对比算子xy决定时戳y是否比时戳x旧。扩展研究处理时戳可以作为未来的研究方向。
免责声明：本文仅代表作者个人观点，与C114中国通信网无关。其原创性以及文中陈述文字和内容未经本站，对本文以及其中全部或者部分内容、文字的真实性、完整性、及时性本站不作任何或承诺，请读者仅作参考，并请自行核实相关内容。
·MWC 英特尔加速5G产业协作与标准化进程(3-2)·从CSP转型DSP：运营商需要什么？(2-20)·中兴通讯发布5G全系列预商用基站 引领5G商用进程(2-16)·光纤预埋入户：提升FTTH部署进程新策略(2-16)·TBR：运营商加速ITO管理服务进程，华为市场影响力不断增强(2-16)·京东3C再签三大商家 80亿大单加速平台化进程(2-7)·深圳联通携手中兴揭牌NB-IoT联合创新实验室 加速物联网应用商用进程(1-22)·互联网化进程加速中的酷派能否抓住智能互联的风口(1-16)·印度：爱立信、诺基亚和华为4G扩程的一大亮点(12-30)·华为扮演NB-IoT关键角色：引领发展进程 加速生态成熟(12-22)
·英国宣布已确定部署5G的三个初始频段2/21·菲律宾PLDT宣布与华为进行5G合作 计划2020年推出5G网络2/16·爱立信电信SK电讯宣布完成全球首个洲际5G网络测试2/16·诺基亚今年底要推出的4.9G技术是什么？2/15·诺基亚称今年年底提供4.9G技术：下载速率高达3Gbps2/15·谷歌携手诺基亚高通积极推进3.5GHz无线·华为将为西班牙电信在13个国家部署vEPC网络2/7·这波野心有点大！SK电讯的Lora网络已经建到了泰国2/7·中移动2017年将在巴基斯坦投资2亿美元扩大3G/4G网络覆盖2/7·尼泊尔电信15天发展4万4G用户 2月4日将推预付费服务1/24·新加坡M1携手华为进行5G毫米波试验 速度达到35Gbps1/20·诺基亚CTO：2017年5G将走出“原型”进入现场试验1/20
推荐：