Claim 1
If a search for the intruder knowing ecbc(K,C,P), C and P has a solution, then there exists known pairs under the key, K .
This follows immediately from our assumption that the intruder always knows relations between words if they exist, and from the fact that, if the intruder knows C and P, then the intruder can compute exclusive-or of C and P. The converse of this statement is of course not true; it may be possible that the intruder can learn the exclusive-or of C and P without knowing C and P. However, if we are able to rule out knowledge of C and P, we will have been able to rule out one important way of finding known pairs.
The next two claims describe the intruder's ability to produce chosen plaintext and ciphertext. We make use of a function called notsent. The term notsent(X) can be computed by the intruder if and only if it already knows X. We guarantee the ``if'' part of the above claim by specifying notsent(X) as a function computable by the intruder, and the ``only if'' part by having all messages generated by an honest principal (in this case, a host) contain as subterms either constants, timestamps, function symbols other than notsent, or subterms of earlier messages received. We can verify that these restrictions guarantee that notsent(X) is achievable only if the intruder knows X by giving the Analyzer as a goal the state in which the intruder knows notsent(X) but has not computed notsent(X) from X. We then prove that this goal state is unreachable.
The reason for choosing this definition of notsent is that we
want to be able to model an arbitrary function that the intruder
can use to produce chosen plaintext when CBC mode is used.
The idea is as follows. Suppose that the intruder can produce
ecbc(K,IV,notsent(IV)). Then the intruder can choose
notsent(IV) to be the exclusive-or of IV and a chosen plaintext
P. Applying the cipher block chaining algorithm to IV
and notsent(IV) would result in 
which would give
us the chosen plaintext we would need. A similar argument would
produce chosen ciphertext.
Given this motivation, our claims are as follows:
Claim 2
If a search for the intruder knowing ecbc(K,notsent(P),P), or ecbc(K,IV,notsent(IV)) has a solution, then there exist chosen-plaintext pairs under the key, K .
Claim 3
If a search for the intruder knowing dcbc(K,notsent(C),C), or dcbc(K,IV,notsent(IV)) has a solution, then there exist chosen-ciphertext pairs under the key, K .
We note again that we have no guarantee that the converse of these statements is true. Knowing that intruder can't produce ecbc(K,notsent(P),P) or ecbc(K,IV,notsent(IV)) does not eliminate the possibility that the intruder may be able to force the choice of X and Y so that their exclusive-or is a chosen P, without being able to choose X or Y directly. However, we do know that if we can rule out the intruder's finding ecbc(K,notsent(P),P) and ecbc(K,IV,notsent(IV)), we can rule out one of the most likely ways the intruder has of finding chosen plaintext.
Our claims in this section replaces a previous set of claims which relied upon the intruder's use of a constant notsent instead of the function notsent(P). While this was sufficient to capture known and chosen pairs for Electronic Code Book Mode, it was not sufficient to capture the fact that the intruder needed knowledge of one of the arguments of ecbc or dcbc before he computed the other. The incorrect use of notsent as a constant led to the discover of spurious ``attacks'' on protocols. In the next section, we will describe show how our analysis of the IP Encapsulating Security Protocol led to a discovery of such a spurious attack. We will also show how the discovery of these spurious attacks helped us to identify an error both in our specification and in our requirements.