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
