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

D.X. Liu and Y.C. Bai


Security protocols, protocol representation, cross-tree, cross-forest, formal methods


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.

Important Links:

Go Back