60 X: synth (analz (sees Spy evs)) |] |
60 X: synth (analz (sees Spy evs)) |] |
61 ==> Says Spy B X # evs : recur" |
61 ==> Says Spy B X # evs : recur" |
62 |
62 |
63 (*Alice initiates a protocol run. |
63 (*Alice initiates a protocol run. |
64 "Agent Server" is just a placeholder, to terminate the nesting.*) |
64 "Agent Server" is just a placeholder, to terminate the nesting.*) |
65 RA1 "[| evs: recur; A ~= B; A ~= Server; Nonce NA ~: used evs |] |
65 RA1 "[| evs1: recur; A ~= B; A ~= Server; Nonce NA ~: used evs1 |] |
66 ==> Says A B |
66 ==> Says A B |
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 # evs : 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 XA should be the Hash of the remaining components with KA, but |
73 Bob cannot check that. |
73 Bob cannot check that. |
74 P is the previous recur message from Alice's caller. |
74 P is the previous recur message from Alice's caller. |
75 NOTE: existing proofs don't need PA and are complicated by its |
75 NOTE: existing proofs don't need PA and are complicated by its |
76 presence! See parts_Fake_tac.*) |
76 presence! See parts_Fake_tac.*) |
77 RA2 "[| evs: recur; B ~= C; B ~= Server; Nonce NB ~: used evs; |
77 RA2 "[| evs2: recur; B ~= C; B ~= Server; Nonce NB ~: used evs2; |
78 Says A' B PA : set evs; |
78 Says A' B PA : set evs2; |
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" |
81 # evs2 : recur" |
82 |
82 |
83 (*The Server receives Bob's message and prepares a response.*) |
83 (*The Server receives Bob's message and prepares a response.*) |
84 RA3 "[| evs: recur; B ~= Server; |
84 RA3 "[| evs3: recur; B ~= Server; |
85 Says B' Server PB : set evs; |
85 Says B' Server PB : set evs3; |
86 (PB,RB,K) : respond evs |] |
86 (PB,RB,K) : respond evs3 |] |
87 ==> Says Server B RB # evs : recur" |
87 ==> Says Server B RB # evs3 : recur" |
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; A ~= B; |
91 RA4 "[| evs4: recur; 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|} : set evs; |
93 XA, Agent A, Agent B, Nonce NA, P|} : set evs4; |
94 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|}, |
95 Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, |
95 Crypt (shrK B) {|Key KAB, Agent A, Nonce NB|}, |
96 RA|} : set evs |] |
96 RA|} : set evs4 |] |
97 ==> Says B A RA # evs : recur" |
97 ==> Says B A RA # evs4 : recur" |
98 |
98 |
99 (**No "oops" message can easily be expressed. Each session key is |
99 (**No "oops" message can easily be expressed. Each session key is |
100 associated--in two separate messages--with two nonces. |
100 associated--in two separate messages--with two nonces. |
101 ***) |
101 ***) |
102 end |
102 end |