Next: Discussion Up: Proofs of Exemplary Protocols Previous: Station-to-Station Protocol

## Needham-Schroeder key distribution protocol

This section presentes the use of the weakest precondition calculus to prove the Needham-Schroeder protocol for key distribution (not for public keys). The original protocol is:

1. A S: A,B,N
2. S A: {N ,B,K ,{K ,A} }
3. A B: {K ,A}
4. B A: {N }
5. A B: {N -1}

The expanded protocol from A's point of view is:

NS-A1
A : A,B,N {A sends a message}
NS-A2
A: {N ,B,K ,{K ,A} } {A receives the message}
NS-A3
A: decrypt{X {A decrypts the message}
NS-A4
A proves (A B)
NS-A5
A proves (fresh(K )
NS-A6
A {K ,A}
NS-A7
A: {N }
NS-A8
A: decrypt{N }
NS-A9
A: F(N ,1) = N -1
NS-A10
A: F(N -1,K ) = {N -1}
NS-A11
A {N -1}

Steps NS-A1 through NS-A5 are used in testing A's postconditions. The postconditions for A should be:

• A believes (A sees K ) Discharged in step NS-A2
• A believes (A B) Discharged in step NS-A4
• A believes (fresh(K )) Discharged in step NS-A5

Note that we do not include a post-condition that A sent any message to initiate the protocol. We strongly believe that such a post condition is important, and that specific ordering between protocol steps should be maintained. This is discussed further in [AF97].

Table 14: Proof of A's postconditions for NS protocol.

The proof of A's postconditions (steps 1 through 9 of the protocol) are presented in Table 14, generating the following preconditions for A:

• A believes fresh(N )
• A believes (S controls A B)
• A believes (S controls fresh(K )
• A believes (A S)
• A sees ``A'', ``B'', N , and K
• A believes (A sees K )

It's now been proven that A believes (A B) and that A believes (fresh(K )). However, steps 5 and 4 are not entirely correct. In step 8 ``S says K '' is treated as ``S says A B''. Either ``A believes (S says K S says A B)'' should be a premise or ``K '' should be idealized as ``A B'' in S's message to A. Similarly in step 9 ``A believes (S says )'' is used where ``A believes (S says (fresh(K )))'' is necessary. Again the two solutions are a premise saying ``A believes (S says K S says fresh(K )'' or an idealization. For both of these problems Syverson and van Oorschot [Syv96] use the premise approach, we have opted for protocol idealization.

The expanded protocol from B's point of view is:

NS-B1
B: {K ,A}
NS-B2
B: decrypt{K ,A}
NS-B3
B proves (A B)
NS-B4
B proves fresh (K )
NS-B5
B: F(N ,K ) = {N }
NS-B6
B {N }
NS-B7
B: {N -1}
NS-B8
B: decrypt {N -1}

Steps NS-A1 through NS-A5 are used in testing A's postconditions. The postconditions for B should be:

• B believes (B sees K ) Discharged in step NS-B2
• B believes (A B) Discharged in step NS-B3
• B believes (fresh(K )) Discharged in step NS-B4
• B believes (B received N ) Discharged in step 8

The first three postconditions are symmetric to those of A. The last is used to help prove currency, and requires an additional premise that N is fresh. One difficulty in this proof comes from conditions of the form B sent {K ,A} . The truth of this negated conditions comes from making sure that B sent {K ,A} isn't in any of the preconditions. This may raise complications that aren't there for the other conditions which can be proven in a single step.

Table 15: Proof of B's postconditions for NS protocol.

The proof of B's postconditions is shown in Table 15 and generates the following preconditions for B:

• B believes fresh(N )
• B believes (S controls A B)
• B believes (S controls fresh(K )
• B believes (B S)
• B sees K ,N
• B believes (B sees K )

The problems arise in steps 2, 3, and 4. First, just as for participant A, the server S only mentions the key K and does not explicitly mention its freshness or validity. Unlike in A's proof an idealization (e.g. K idealized as fresh (K )) won't work for B. Because of the nonce N participant A could believe ``S says K '', but at best B can only prove ``S said K '' (step 12). Thus, the proof:

S says fresh (K ) S controls fresh (K ) fresh (K )

doesn't work. Instead a premise such as:

S said fresh (K ) fresh (K )

is necessary. Of course, using said in the place of says is quite risky as B can be subjected to a replay attack using old, broken keys for K and K even if the key K remains valid. Again, we have assumed a protocol idalization to remove this problem. Further work is definitely needed to resolve this problem in the verification of this protocol.

Next: Discussion Up: Proofs of Exemplary Protocols Previous: Station-to-Station Protocol

Jim Alves-Foss
Fri Aug 1 16:00:31 PDT 1997