next up previous
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 tex2html_wrap_inline1387 S: A,B,N tex2html_wrap_inline1045
  2. S tex2html_wrap_inline1387 A: {N tex2html_wrap_inline1045 ,B,K tex2html_wrap_inline1171 ,{K tex2html_wrap_inline1171 ,A} tex2html_wrap_inline1677 } tex2html_wrap_inline1679
  3. A tex2html_wrap_inline1387 B: {K tex2html_wrap_inline1171 ,A} tex2html_wrap_inline1677
  4. B tex2html_wrap_inline1387 A: {N tex2html_wrap_inline1175 } tex2html_wrap_inline1691
  5. A tex2html_wrap_inline1387 B: {N tex2html_wrap_inline1175 -1} tex2html_wrap_inline1691

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

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

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

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

   table412
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:

It's now been proven that A believes (A tex2html_wrap_inline1169 B) and that A believes (fresh(K tex2html_wrap_inline1171 )). However, steps 5 and 4 are not entirely correct. In step 8 ``S says K tex2html_wrap_inline1171 '' is treated as ``S says A tex2html_wrap_inline1169 B''. Either ``A believes (S says K tex2html_wrap_inline1839 S says A tex2html_wrap_inline1169 B)'' should be a premise or ``K tex2html_wrap_inline1171 '' should be idealized as ``A tex2html_wrap_inline1169 B'' in S's message to A. Similarly in step 9 ``A believes (S says tex2html_wrap_inline1847 )'' is used where ``A believes (S says (fresh(K tex2html_wrap_inline1171 )))'' is necessary. Again the two solutions are a premise saying ``A believes (S says K tex2html_wrap_inline1839 S says fresh(K tex2html_wrap_inline1171 )'' 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
tex2html_wrap_inline1387 B: {K tex2html_wrap_inline1171 ,A} tex2html_wrap_inline1677
NS-B2
B: decrypt{K tex2html_wrap_inline1171 ,A} tex2html_wrap_inline1677
NS-B3
B proves (A tex2html_wrap_inline1169 B)
NS-B4
B proves fresh (K tex2html_wrap_inline1171 )
NS-B5
B: F(N tex2html_wrap_inline1175 ,K tex2html_wrap_inline1171 ) = {N tex2html_wrap_inline1175 } tex2html_wrap_inline1691
NS-B6
B tex2html_wrap_inline1387 {N tex2html_wrap_inline1175 } tex2html_wrap_inline1691
NS-B7
tex2html_wrap_inline1387 B: {N tex2html_wrap_inline1175 -1} tex2html_wrap_inline1691
NS-B8
B: decrypt {N tex2html_wrap_inline1175 -1} tex2html_wrap_inline1691

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

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 tex2html_wrap_inline1175 is fresh. One difficulty in this proof comes from conditions of the form tex2html_wrap_inline1903 B sent {K tex2html_wrap_inline1171 ,A} tex2html_wrap_inline1677 . The truth of this negated conditions comes from making sure that B sent {K tex2html_wrap_inline1171 ,A} tex2html_wrap_inline1677 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.

   table516
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:

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

S says fresh (K tex2html_wrap_inline1171 ) tex2html_wrap_inline1053 S controls fresh (K tex2html_wrap_inline1171 ) tex2html_wrap_inline1651 fresh (K tex2html_wrap_inline1171 )

doesn't work. Instead a premise such as:

S said fresh (K tex2html_wrap_inline1171 ) tex2html_wrap_inline1651 fresh (K tex2html_wrap_inline1171 )

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 tex2html_wrap_inline1827 and K tex2html_wrap_inline1171 even if the key K tex2html_wrap_inline1997 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 up previous
Next: Discussion Up: Proofs of Exemplary Protocols Previous: Station-to-Station Protocol

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