PCL protocol composition logic

PCL 协议组合逻辑

一 主体（principal）和线程（thread）的区分

1.主体：指 **协议的参与者，用X^来表示。**每个主体可以扮演一个或多个角色，如 InitCR和RespCR ；

2.线程：主体在某个具体的协议会话中的执行过程，用X和Y表示。

总之，主体代表协议参与者的抽象概念，而线程代表了主体在特定会话中的具体实例化。主体可以在多个不同的会话中出现，并且可以以不同的方式扮演不同的角色。线程则代表了主体在某个具体的会话中的行为。

二.Protocol Programming Language

1. Terms

   1.terms 通常由 常量c和变量x，通过构造器p进行构建，构造器有 **元组化操作、公钥加密 ENCK{|t|} 和签名 SIGK{|t|} **。可以完全评估的闭合项（closed terms）是协议中交换的信息的内容，注：闭合项是完全具体化的项，其所有的变量都被替换为具体的值或常量。

   2.关于项的evaluation（评估），是指 对项进行计算或求值的过程，用于模拟计算过程，将项替换为它们的值或结果。

   3.包含自由变量（如 pointers and references ）的项是无法直接发送的，完全评估意味着 term中的变量全部被实例化！所以可以发送。

   4.基本项（basic terms）u ：它是不直接包含密码操作的项，因为它可以包含变量，而这个变量的取代值可能是一个加密结果，但是没有直接使用密码学原语。 所以，基本术语是不涉及具体的密码算法的项；

   项（terms）t：可以包含密码学原语的项，如对称或非对称加密、数字签名等密码学原语。