The NRL Protocol Analyzer is a formal methods tool for analyzing security properties of cryptographic protocols. Protocols are specified as communicating state machines, one of which is a hostile intruder who can read all traffic, modify or delete traffic, perform cryptographic operations, and may be in cooperation with some legitimate users of the system. The intruder also is assumed to have knowledge about relationships between data. That is, if it sees the result of encrypting a piece of plaintext with a key, it will know that it is the result of encrypting the plaintext with that key, although it may not know plaintext or key. This model has the effect of simplifying our search for known pairs, since it means that if the intruder sees a plaintext-ciphertext pair, it also knows that it is such.
The user of the Analyzer attempts to determine whether or not a protocol is secure by specifying an insecure state. The Analyzer works backwards from that state until it either reaches an initial state, in which case it has found an attack, or until it has shown that all paths begin in an unreachable state.
The Analyzer makes no assumptions about the limits on the number of protocol executions, the number of principals performing the different executions, the number of interleaved executions, or the number of times cryptographic functions are applied. This results in a search space that is originally infinite. However, the Analyzer provides means for specifying and proving inductive lemmas about the unreachability of infinite classes of states. This allows the user to narrow down the search space so that in many cases an exhaustive search is possible.
An Analyzer specification consists of four parts. The first part describes the operations and terms used in the specification. The second part describes the rewrite rules used. These capture the necessary algebraic properties of cryptosystems, such as the fact that encryption and decryption cancel each other out. The third part specifies the words known initially by the intruder. The last and main part consists of transition rules describing the actions taken by legitimate participants. The inputs to these transition rules are messages received (which may have been passed on by the intruder) and values of local state variables. The outputs are messages sent (which will be available to the intruder) and new values of the local state variables. The intruder actions are not specified directly, but are generated automatically from the specification.
The Analyzer generates the input state to an existing state defined as a set of local state variables values and words known to the intruder as follows. It takes each transition rule output in turn and uses a narrowing algorithm to find a complete description of all substitutions that make any portion of the output reducible to a subset of the state. The input to the rule and the unmatched portion of the state then become the input state. This allows the Analyzer to discover unexpected consequences of the use of cryptographic functions.
The Analyzer has been applied to a number of different cryptographic protocols, and has found flaws in several. In some cases the flaws had not been discovered before. Examples of protocols the Analyzer has been used to examine are the Simmons Selective Broadcast Protocol [5], the Burns-Mitchell Ticket Granting Protocol [4], the Needham Schroeder public key protocol [7]. A description of the Analyzer is given in [6].
Most of the protocols to which the Analyzer has been applied are specified at a higher degree of abstraction than the protocols we will be looking at in this paper. Methods for using block ciphers to encrypt messages more than one block long are not modeled, and the integrity of an encrypted message is assumed. Thus, using the Protocol Analyzer to explore the consequences of cipher block chaining was a new departure.