Next: The Model Up: A Model Checker for Previous: The Specification

# Messages

Typically, the messages exchanged during the run of a protocol are built up using pairing and encryption from smaller submessages. The smallest such submessages (i.e. they contain no submessages themselves) are called atomic messages. There are four types of atomic messages.

• Keys are used to encrypt messages. We make the perfect encryption'' assumption, which states that the only way to obtain the plaintext from an encrypted message is by using the appropriate decryption key. Keys have the property that every key k has an inverse such that for all messages m , . (Note that for symmetric cryptography the decryption key is the same as the encryption key, so .)
• Principal names are used to refer to the participants in a protocol.
• Nonces are randomly generated numbers. The intuition is that since they are randomly generated, any message containing a nonce can be assumed to have been generated after the nonce was generated. (It is not an old'' message.)
• Data which plays no role in how the protocol works but which is intended to be communicated between principals.

Let denote the space of atomic messages. The set of all messages over some set of atomic messages is defined inductively as follows:

• If then . (Any atomic message is a message.)
• If and then . (Two messages can be paired together to form a new message.)
• If and key then . (A message M can be encrypted with key k to form a new message.)

Because keys have inverses, we take this space modulo the equivalence . It is also important to note that we make the following perfect encryption assumption. The only way to generate is from m and k . In other words, there do not exist messages and and key k such that , and implies m = m' and k = k' .

Let be a subset of messages. The closure of B (denoted ), representing the set of everything that can be derived from B , is defined by the following rules:

1.
If then .
2.
If and then . (pairing)

3.
If then and . (projection)

4.
If and key then . (encryption)

5.
If and key then . (decryption)

Next: The Model Up: A Model Checker for Previous: The Specification