In cryptographic protocol design, we always assume the presence of an intruder that has a complete control over the communication network. Accordingly, the intruder is able to intercept, modify, store, retrieve and send any circulating message in the network. Moreover, we assume that the intruder has the usual encryption and decryption abilities. In this work, we consider another valuable source of information available to the intruder: the protocol itself. Actually, the protocol may be viewed by the intruder as a computation engine which may be used to synthesize and deliver some particular information that makes possible a fatal attack.
In our approach, we capture all these intruder abilities by a deductive proof system. We associate to each protocol step an inference rule. Each inference rule captures one possible instrumentation of the protocol. The general form of an inference rule is:
where are messages and c is a boolean
formula. This inference rule should be read as follows: the
intruder could supply the protocol with the messages
and get the message m from the protocol
provided that the side condition c holds
. In fact, the side
condition refers to those freshness conditions dictated by the
protocol. Furthermore, we will endow each inference rule with
a sequence of protocol steps (a scenario) showing how
the intruder could instrument the protocol with the
information
so as to get the message m .
Now, let us see how this applies to the Woo and Lam protocol of Table 1. For the sake of clarity, we present here the inference rules together with the associated scenarios without explaining how they are generated. Such explanations will be given further in the sequel.
The first step in the Woo and Lam protocol of Table 1 is:
The inference rule associated with this protocol step is:
meaning that the intruder could get from the protocol the identity of any principal wishing to initiate a protocol session. Here is the scenario that makes this possible:
This sequence stipulates that the intruder could get the identity of a principal A by intercepting the message sent by this principal when wishing to initiate a new protocol session. In doing so, the intruder I performs a masquerade on the role of a principal B, which is written I(B) . Later in this section, we will present inference rules that capture sophisticated computations.
The second step in the Woo and Lam protocol of Table 1 is:
The inference rule associated with this protocol step is:
meaning that the intruder could get a fresh nonce
(generated by B ) from the protocol just by supplying it with
an agent identity. The side condition stipulates
the freshness
of the
information
. Here is the scenario that illustrates such
a situation:
This sequence stipulates that the intruder does a masquerade
on the role A . First, the intruder sends to B the
principal identifier A . According to the protocol, the
principal B will react by generating a fresh nonce and
sending it on the network to A , hence to I(A) .
The third step in the Woo and Lam protocol of Table 1 is:
The inference rule associated with this protocol step is:
meaning that the intruder could supply the protocol
with any information X and get it encrypted under the secret
key shared between the server S and a principal A . At this
level, we would like to pinpoint one important feature in our
verification algorithm. The reader should notice that we used
X in the inference rule instead of . The rationale
underlying this choice is that the principal A , at the third
step of the protocol, replies with the message received at the
second step (i.e.
) encrypted by
. Notice that
is a nonce generated and uttered by B and sent to
A . Now, let us mention the following facts:
Owing to these three facts, A can verify neither the value,
the freshness nor the type of the message received at the
second step of the protocol. Consequently, A will accept any
message at that step and will reply by sending the encrypted
version of this message under the key . This explains
the rationale underlying the use of a variable message X
instead of
. We will show further how fatal attacks
could stem from this second protocol step.
Here is the scenario that exhibits how the intruder could
instrument the protocol so as to get the message provided that he supplies the protocol with X :
This sequence stipulates that the intruder will do a masquerade
on the role B . First, the intruder will wait for A to
initiate a protocol session i.e. to send the message A which
will be intercepted by I(B) . Next, the intruder I(B) will
send a message X to the principal A . The latter will react
innocently by sending the message .
From now on, it is clear that the intruder has the ability to
encrypt any known message X with the secret key shared by the server and a principal A . Indeed, this ability
follows from the three-steps sequence above. This highlights a
weakness in the design of the Woo and Lam protocol. More
dramatically, the intruder could encrypt any known message X
by any shared key
where p stands for any
principal identifier. The reader should notice that in the
protocol specification the principal identifier A is
implicitly universally quantified over all principals.
Now, let us give some general comments regarding the inference rules and the associated scenarios. First, the agent identifiers as well as the introduced variables are implicitly universally quantified. Second, the generated scenarios constitute proofs of the correction of the inference rules. Actually, the scenarios are propagated during the deduction process.
The fourth step in the Woo and Lam protocol of Table 1 is:
The inference rule associated with this protocol step is:
meaning that the intruder could supply the protocol
with a principal identifier, say A , and a known message X
so as to get an encrypted version of the composition of these
two messages under the key . Here is the scenario that
illustrates such a situation:
This sequence stipulates that the intruder will do a
masquerade on the role A . First, the intruder sends to B
the principal identifier A . According to the protocol, the
principal B reacts by generating a fresh nonce and
sending it on the network to A , hence to I(A) . The next
step is very sensible from the security standpoint. In fact,
at the third step, the principal B is waiting for a message
(
) encrypted under a key (
) that is locally
unknown (from B standpoint). Nevertheless, the principal B
has no means to check neither that the received message at the
third step is effectively encrypted under
(
is unknown to B ), nor that its content is
. Hence, the
principal B can accept any message, say X , at this third
step. Finally, the principal B reacts confidently with the
message
. This pinpoints a second
weakness in the design of the Woo and Lam protocol.
The fifth step in the Woo and Lam protocol of Table 1 is:
The inference rule associated with this protocol step is:
meaning that the intruder could supply the protocol
with a message of the form so as to get the message
. Here is the scenario that illustrates such a
situation:
This sequence stipulates that the intruder will do a
masquerade on the role B . First, the intruder sends to the
server the message . According
to the protocol, the server decrypts such a message twice
(using
then
) and sends the sub-message X
encrypted under the key
. Notice that the server, at
the fourth step, is normally expecting a message of the form
. However, the server can
check neither the value, the freshness nor the type of
. Accordingly, the server accepts any other information
instead of
. This explains the rationale underlying the
use of X instead of
in the previous inference rule.
From now on, it is clear that the intruder has extra
decrypting abilities. In addition to the usual ones, the
intruder can instrument the protocol to decrypt messages
encrypted under keys that are unknown to him. For instance,
assume that the intruder is wishing to decrypt a message of
the form . Recall also that the intruder may
be a legal principal that shares a symmetric key
with
the server. The intruder can merely supply the server with the
message
to get finally the
message
which he can decrypt to extract
X . Here, the intruder has used the server as an oracle to
decrypt messages. Notice that this example illustrates only
one possible application (among many) of the previous
inference rule. This pinpoints a third weakness in the design
of the Woo and Lam protocol.
We sum up in Table 3 the whole proof system that has been generated from the Woo and Lam protocol of Table 1. The inference rules and the associated scenarios have been automatically generated from the protocol specification. The generation method will be explained further in the sequel.
Table 3:
The Deductive Proof System Associated with the Woo and
Lam Protocol