**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.