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 $k^{-1}$ such that for all messages m , $\{ \{ m \}_{k} \}_{k^{-1}} = m$. (Note that for symmetric cryptography the decryption key is the same as the encryption key, so $k = k^{-1}$.)
• 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 ${\cal A}$ denote the space of atomic messages. The set of all messages ${\cal M}$ over some set of atomic messages ${\cal A}$ is defined inductively as follows:

• If $a \in {\cal A}$ then $a \in {\cal M}$. (Any atomic message is a message.)
• If $m_{1} \in {\cal M}$ and $m_{2} \in {\cal M}$ then $m_{1} \cdot m_{2} \in {\cal M}$. (Two messages can be paired together to form a new message.)
• If $m \in {\cal M}$ and key $k \in {\cal A}$ then $\{m\}_{k} \in {\cal M}$. (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 $\{ \{ m \}_{k} \}_{k^{-1}} = m$. It is also important to note that we make the following perfect encryption assumption. The only way to generate $\{ m \}_{k}$ is from m and k . In other words, there do not exist messages $m, m_{1},$ and $m_{2}$ and key k such that $\{ m \}_{k} = m_{1} \cdot m_{2}$, and $\{ m \}_{k} = \{ m' \}_{k'}$ implies m = m' and k = k' .

Let $B \subseteq {\cal M}$ be a subset of messages. The closure of B (denoted $\overline{B}$), representing the set of everything that can be derived from B , is defined by the following rules:

1.

If $m \in B$ then $m \in \overline{B}$.

2.

If $m_{1} \in \overline{B}$ and $m_{2} \in \overline{B}$ then $m_{1} \cdot m_{2} \in \overline{B}$. (pairing)

3.

If $m_{1} \cdot m_{2} \in \overline{B}$ then $m_{1} \in \overline{B}$ and $m_{2} \in \overline{B}$. (projection)

4.

If $m \in \overline{B}$ and key $k \in \overline{B}$ then $\{m\}_{k} \in \overline{B}$. (encryption)

5.

If $\{m\}_{k} \in \overline{B}$ and key $k^{-1} \in \overline{B}$ then $m \in \overline{B}$. (decryption)