交叉树:一种用于安全协议分析的数据结构

Cross-Tree:A Date Structure for Analysis of Security Protocols

提出用一种特殊的数据结构交叉树来描述安全协议中的消息。交叉树有一些交叉结点,拥有交叉结点的几棵交叉树形成交叉森林。一棵交叉树唯一对应于一个消息,一个交叉森林表示那些在协议执行过程中采用相同机制发送或接收的消息。一个或几个消息中相同的原子消息在交叉树或交叉森林中用交叉结点来表示,这样易于保证原子消息的一致性,以及公钥和它所有者之间的一致性。另外,交叉树还可用于为消息模板建立可接受消息,这对于建立在模型检验基础上的安全协议分析是非常必要的。

This article proposes a data structrre called cross-tree which is a special tree with some nodes crossed to represent messages in security protocols, Several cross-trees can constitute a cross-forest when they have crossed modes. A cross-tree corresponds uniquely with a message,and a cross-forest represents those messages that are sent or received by the same principal in a protocol execution. The same atomic messages in one message or several messages are represented sa the crossed nodes in a cross-tree or a cross-forest;hence it is easy to guarantee the consistency of the atomic messages and the consistency of the public keys and its owners, iIn addition,a cross-tree can be used to construct acceptable messages for a message template,which is mecessary for the analysis of security protocols based on model checking.