88 |
88 |
89 (*Bob receives the returned message and compares the Nonces with |
89 (*Bob receives the returned message and compares the Nonces with |
90 those in the message he previously sent the Server.*) |
90 those in the message he previously sent the Server.*) |
91 RA4 "[| evs: recur lost; A ~= B; |
91 RA4 "[| evs: recur lost; A ~= B; |
92 Says B C {|XH, Agent B, Agent C, Nonce NB, |
92 Says B C {|XH, Agent B, Agent C, Nonce NB, |
93 XA, Agent A, Agent B, Nonce NA, P|} |
93 XA, Agent A, Agent B, Nonce NA, P|} : set evs; |
94 : set evs; |
|
95 Says C' B {|Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|}, |
94 Says C' B {|Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|}, |
96 Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, |
95 Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, |
97 RA|} |
96 RA|} : set evs |] |
98 : set evs |] |
|
99 ==> Says B A RA # evs : recur lost" |
97 ==> Says B A RA # evs : recur lost" |
100 |
98 |
101 (**No "oops" message can readily be expressed, since each session key is |
99 (**No "oops" message can easily be expressed. Each session key is |
102 associated--in two separate messages--with two nonces. |
100 associated--in two separate messages--with two nonces. |
103 ***) |
101 ***) |
104 end |
102 end |