67 (Hash[Key(shrK A)] |
67 (Hash[Key(shrK A)] |
68 {|Agent A, Agent B, Nonce NA, Agent Server|}) |
68 {|Agent A, Agent B, Nonce NA, Agent Server|}) |
69 # evs1 : recur" |
69 # evs1 : recur" |
70 |
70 |
71 (*Bob's response to Alice's message. C might be the Server. |
71 (*Bob's response to Alice's message. C might be the Server. |
72 XA should be the Hash of the remaining components with KA, but |
72 We omit PA = {|XA, Agent A, Agent B, Nonce NA, P|} because |
73 Bob cannot check that. |
73 it complicates proofs, so B may respond to any message at all!*) |
74 P is the previous recur message from Alice's caller. |
|
75 NOTE: existing proofs don't need PA and are complicated by its |
|
76 presence! See parts_Fake_tac.*) |
|
77 RA2 "[| evs2: recur; B ~= C; B ~= Server; Nonce NB ~: used evs2; |
74 RA2 "[| evs2: recur; B ~= C; B ~= Server; Nonce NB ~: used evs2; |
78 Says A' B PA : set evs2; |
75 Says A' B PA : set evs2 |] |
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|}) |
76 ==> Says B C (Hash[Key(shrK B)] {|Agent B, Agent C, Nonce NB, PA|}) |
81 # evs2 : recur" |
77 # evs2 : recur" |
82 |
78 |
83 (*The Server receives Bob's message and prepares a response.*) |
79 (*The Server receives Bob's message and prepares a response.*) |
84 RA3 "[| evs3: recur; B ~= Server; |
80 RA3 "[| evs3: recur; B ~= Server; |