1 引言
1998年，Thayer,Herzog 以及Guttman提出的串空间模型[1]（Strand Space Model）,串空间模型是一种结合定理和协议迹的混合方法。串是参与协议的主体可以执行的事件序列。对于诚实的主体，该事件序列是根据协议定义，由发送事件和接收事件组合而成的。此外，该模型还定义了攻击串，描述攻击者的行为。串空间模型的核心结构是它的丛结构。丛是一个良构（well-defined）集合，表示一个完整的协议交换串空间的子集。丛可以表示为有限无环图，其中的边表示结点间的因果依赖关系，根据串空间的基本模型，容易对其不同方向的扩展、增强和优化。
在传统的串空间基础上，我们引入一种带变量的串空间，即变量出现在消息项及其演算中，允许变量在一定范围内变化并对变量作置换运算。发送和接收操作不再用 符号＋和符号－表示，而是分别用符号＜＞和符号（）表示，例如 表示接收一个值并存在变量 中；而 表示发送一个项 。类似于文献[2]中思想，串与串中的动作元素能相互反应，并产生一个新的项。例如如果 和 同步发生，则发送的项 被变量 接收，其作用结果是产生一个置换项 。
我们引入的逻辑则能保证诚实主体在执行一系列动作后，一些断言如秘密性、可鉴别性仍然能够保持。逻辑中的模态词源于进程代数[3]中的一系列表示动作的模态操作。主要方法是对角色行为附加断言，并采用Floyd-Hoare逻辑[4]方式，通过一系列角色行为的组合，绑定相应的逻辑公式，最后应用这些公式给出一个协议正确性证明。与以前的类BAN逻辑[5]及Paulson的归纳方法[6]不一样，其主要思想是肯定包含某个行为的断言是成立的，这样就可以推理协议的性质，而无须对攻击者的行为进行推理。逻辑的语义是基于协议运行的具体的迹，而不象以前逻辑那样其语义仅是一种抽象的概念。
将带变量的串空间模型的行为语义和逻辑推断相结合主要包含以下二个方面：
(1)串空间中的项一般是带变量的，我们称为模式项。主体通过接收对方传来的值或自己产生新鲜数将模式项实例化，即变成不再含变量的项。只有当实例化后的模式项与协议规定的信息格式相匹配时，主体才进行下一个动作。
(2) 当主体A做出协议规定的行为 后，我们给出相应的逻辑推断。例如 表示主体A完成动作后，公式成立。
...........................................
5 结论
在传统的串空间基础上提出了一种带变量的串空间模型，以及基于主体行为语义的逻辑推理系统。串空间中的变量可以是参加协议的主体、密钥、产生的新鲜数以及接收和发送的消息，只有当协议接收方通过解密发现与解密模式匹配时才用实际值置换项变量，这种模型更接近于实际协议执行过程中的开放环境以及体现执行环境的不确定性和复杂性。提出的逻辑包含了主要公理及推理规则，其中的模态公式把诚实主体发生的行为与谓词公式绑定在一起，这样只要诚实主体有关的行为一旦发生，与其绑定的逻辑公式也就为真，这样只需推理诚实主体完成的各种步骤，而无须具体推断攻击者的各种可能攻击。最后我们以Helsinki协议作为实例分析说明了这种方法的有效性。
参考文献：
[1] F.J.T. Fábrega, J.C. Herzog and J.D. Guttman, Strand spaces: Why is a security protocol correct? in:Proceedings of the 1998 IEEE Symposium on Security and Privacy, Oakland, CA, IEEE Computer Society Press, 1998, pp. 160–171.
[2] G. Berry and G. Boudol, www.51lunwen.org/jsjaq/ The chemical abstract machine, Theoretical Computer Science 96 (1992),217–248.
[3] M. Abadi and A. Gordon, A calculus for cryptographic protocols: the spi calculus, Information and Computation 148(1) (1999), 1–70. Expanded version available as SRC Research Report 149(January 1998).
[4] R.W. Floyd, Assigning meaning to programs, in: Mathematical aspects of computer science: Proc. American Mathematics Soc. Symposia, J.T. Schwartz, ed., Volume 19, Providence RI, American Mathematical Society, 1967, pp. 19–31.
[5] M. Burrows, M. Abadi and R. Needham, A logic of authentication, in: Proceedings of the Royal Society, Series A 426(1871) (1989), 233–271. Also appeared as SRC Research Report 39 and, in a shortened form, in ACM。
[6] L. Paulson, Proving properties of security protocols by induction, in: 10th IEEE Computer Security Foundations Workshop, 1997, pp. 70–83.
[7] ISO/IEC. 2nd DIS 11770-3, Information technologySecurity techniques-key management; part 3; Mechanisms using asymmetric techniques. 1997.
[8] N.Durgin, J.Mitchell and D.Pavlovic, A compositional logic for proving security properties of protocols, in: Journal of Computer Security 11(2003) 677-721.
