Protocol Representation

A protocol defines a sequence of actions of the participating parties. The actions include sending and receiving messages. Messages are defined by the following grammar. The grammar can be easily extended if needed.

Each message can be represented as a tree with the atomic messages as leaves and operations as intermediate nodes. Figure 3 shows an example for the message: $A,B,\{A,B\}$K_B. We define the depth of a message as the depth of the tree representing that message. For example, in Figure 3 the depth of the message tree is 4.

 
Figure 3: Example of a message tree for the message: $A,B,\{A,B\}$K_B