25 Cons "[| (PA, RA, KAB) : respond evs; |
25 Cons "[| (PA, RA, KAB) : respond evs; |
26 Key KBC ~: used evs; Key KBC ~: parts {RA}; |
26 Key KBC ~: used evs; Key KBC ~: parts {RA}; |
27 PA = Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, P|}; |
27 PA = Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, P|}; |
28 B ~= Server |] |
28 B ~= Server |] |
29 ==> (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|}, |
29 ==> (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|}, |
30 {|Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, |
30 {|Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|}, |
31 Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|}, |
31 Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, |
32 RA|}, |
32 RA|}, |
33 KBC) |
33 KBC) |
34 : respond evs" |
34 : respond evs" |
35 |
35 |
36 |
36 |
78 Says A' B PA : set_of_list evs; |
78 Says A' B PA : set_of_list evs; |
79 PA = {|XA, Agent A, Agent B, Nonce NA, P|} |] |
79 PA = {|XA, Agent A, Agent B, Nonce NA, P|} |] |
80 ==> Says B C (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|}) |
80 ==> Says B C (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|}) |
81 # evs : recur lost" |
81 # evs : recur lost" |
82 |
82 |
83 (*The Server receives and decodes Bob's message. Then he generates |
83 (*The Server receives Bob's message and prepares a response.*) |
84 a new session key and a response.*) |
|
85 RA3 "[| evs: recur lost; B ~= Server; |
84 RA3 "[| evs: recur lost; B ~= Server; |
86 Says B' Server PB : set_of_list evs; |
85 Says B' Server PB : set_of_list evs; |
87 (PB,RB,K) : respond evs |] |
86 (PB,RB,K) : respond evs |] |
88 ==> Says Server B RB # evs : recur lost" |
87 ==> Says Server B RB # evs : recur lost" |
89 |
88 |
90 (*Bob receives the returned message and compares the Nonces with |
89 (*Bob receives the returned message and compares the Nonces with |
91 those in the message he previously sent the Server.*) |
90 those in the message he previously sent the Server.*) |
92 RA4 "[| evs: recur lost; A ~= B; |
91 RA4 "[| evs: recur lost; A ~= B; |
93 Says C' B {|Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, |
|
94 Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|}, RA|} |
|
95 : set_of_list evs; |
|
96 Says B C {|XH, Agent B, Agent C, Nonce NB, |
92 Says B C {|XH, Agent B, Agent C, Nonce NB, |
97 XA, Agent A, Agent B, Nonce NA, P|} |
93 XA, Agent A, Agent B, Nonce NA, P|} |
|
94 : set_of_list evs; |
|
95 Says C' B {|Crypt (shrK B) {|Key KBC, Agent C, Nonce NB|}, |
|
96 Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, |
|
97 RA|} |
98 : set_of_list evs |] |
98 : set_of_list evs |] |
99 ==> Says B A RA # evs : recur lost" |
99 ==> Says B A RA # evs : recur lost" |
100 |
100 |
101 (**No "oops" message can readily be expressed, since each session key is |
101 (**No "oops" message can readily be expressed, since each session key is |
102 associated--in two separate messages--with two nonces. |
102 associated--in two separate messages--with two nonces. |