Notation

We use the following notation to describe steps in a protocol.

1. 

Here, the step number of the message is given (this is the first message in the protocol), the message is sent from X to Y, the text of the message is messagetext, and the step is named label.

We use the notation to indicate the message is signed with public key p, and to indicate that a field is encrypted with symmetric key k.