CROSS-TREE: A DATA STRUCTURE FOR ANALYSIS OF SECURITY PROTOCOLS

摘要

This article proposes a data structure 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 nodes. 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 as 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. In addition. a cross-tree can be used to construct acceptable messages for a message template, which is necessary for the analysis of security protocols based on model checking.