In order to see whether the Analyzer could find attacks like this, we modeled a protocol along the line of Bellovin's scenario. In order to make the analysis tractable, we assumed packets were only four blocks long. We modeled two types of headers. One was two blocks long, and one was only one block. This meant that message bodies were always at least two blocks long, which meant that we were able to illustrate the self-healing properties of cipher block chaining; even if the first block was garbled, the second would be correct. We also assumed that hosts would only continue decrypting a packet if the header parsed; this allowed us to discard cases in which header was garbled, and hence a message could neither be passed to the intruder or regarded as a legitimate message for an honest user. This allowed us to ignore a number of useless states that would not have aided us in the analysis but would have increased the size of the search space. We also assumed that SPIs were simplex, so that host A encrypting a message for host B always used spi(A,B) when encrypting a message, and spi(B,A) when decrypting it.
We made a severely simplifying assumption about headers. We assumed that the only thing distinguishing one header from another was its type (short or long) and who the senders and receivers of the message were. This was probably oversimplification, and may have prevented us from finding some subtle attacks in which different sessions between the same parties were confused. However, we believed that it was enough for our goal of determining whether sessions between different parties could be confused. We also assumed that the intruder knows all headers.
Our specification of cipher-block chaining is recursive. When encrypting, the host stores the last encrypted block it produced in a local state variable. It then applies the cipher-block chaining algorithm to the last encrypted block and the next plaintext block. It then replaces the last encrypted block in the state variable with the new encrypted block, which it will use to produce the next encrypted block. Plaintext blocks are either produced by the host (the case when the producer of the message is an honest user) or supplied by the intruder (the case when the producer of the message is a dishonest user). Our reason for having the host produce the messages for honest users is that we assume that communication between the honest user and the host is secure, and that the honest user and host obey the same policy. Thus we may identify the honest user with the host. Likewise, since we assume that all dishonest users are in cooperation with the intruder, we may assume that all messages from dishonest users are produced by the intruder.
Our specification of decryption is similar. The main difference is that all ciphertext messages are assumed to be received from the intruder, since they are passed along an insecure network. The host stores the last ciphertext block received and applies the cipher block chaining decryption algorithm to the next block received. Once it has produced the decrypted block, it replaces the last ciphertext block with the one it just received, and awaits the next ciphertext block.
Our recursive definition of cipher block chaining led to a certain amount of explosion in the state space, since the Analyzer attempted to interleave encryption and decryption transitions. Although the Analyzer has some facilities for recognizing and avoiding multiple interleavings of events, this did not prevent them all. However, even with the state explosion we were able to find Bellovin's attacks. However, our use of a recursive specification style made the specification much easier to read and write. It also made it possible to model a host's refusal to proceed with decryption if it could not read the header, which in itself was a significant help in reducing the search space. However, in order to analyze larger protocols, we will probably need better ways of cutting down on the state explosion.
Our specification also contained an inaccuracy that could lead to the discovery of spurious attacks. In order to simplify the recursive specification, we assumed that blocks were sent out to the network as soon as they were encrypted or decrypted. This of course is not the case; blocks are not sent until the entire packet is encrypted or decrypted. Our ``simplifying'' assumption meant we discovered ``attacks'' in which the intruder used information about one block to influence the production of the next block. We will discuss this in more detail in the next section.
Our specification contained twelve rules:
A copy of the specification is included in the Appendix.