20 AddDs [impOfSubs Fake_parts_insert]; |
20 AddDs [impOfSubs Fake_parts_insert]; |
21 |
21 |
22 |
22 |
23 (*A "possibility property": there are traces that reach the end*) |
23 (*A "possibility property": there are traces that reach the end*) |
24 Goal |
24 Goal |
25 "!!A B. [| A ~= B; A ~= Server; B ~= Server |] \ |
25 "[| A ~= B; A ~= Server; B ~= Server |] \ |
26 \ ==> EX N K. EX evs: ns_shared. \ |
26 \ ==> EX N K. EX evs: ns_shared. \ |
27 \ Says A B (Crypt K {|Nonce N, Nonce N|}) : set evs"; |
27 \ Says A B (Crypt K {|Nonce N, Nonce N|}) : set evs"; |
28 by (REPEAT (resolve_tac [exI,bexI] 1)); |
28 by (REPEAT (resolve_tac [exI,bexI] 1)); |
29 by (rtac (ns_shared.Nil RS ns_shared.NS1 RS ns_shared.NS2 RS |
29 by (rtac (ns_shared.Nil RS ns_shared.NS1 RS ns_shared.NS2 RS |
30 ns_shared.NS3 RS ns_shared.NS4 RS ns_shared.NS5) 2); |
30 ns_shared.NS3 RS ns_shared.NS4 RS ns_shared.NS5) 2); |
31 by possibility_tac; |
31 by possibility_tac; |
32 result(); |
32 result(); |
33 |
33 |
34 Goal |
34 Goal |
35 "!!A B. [| A ~= B; A ~= Server; B ~= Server |] \ |
35 "[| A ~= B; A ~= Server; B ~= Server |] \ |
36 \ ==> EX evs: ns_shared. \ |
36 \ ==> EX evs: ns_shared. \ |
37 \ Says A B (Crypt ?K {|Nonce ?N, Nonce ?N|}) : set evs"; |
37 \ Says A B (Crypt ?K {|Nonce ?N, Nonce ?N|}) : set evs"; |
38 by (REPEAT (resolve_tac [exI,bexI] 1)); |
38 by (REPEAT (resolve_tac [exI,bexI] 1)); |
39 by (rtac (ns_shared.Nil RS ns_shared.NS1 RS ns_shared.NS2 RS |
39 by (rtac (ns_shared.Nil RS ns_shared.NS1 RS ns_shared.NS2 RS |
40 ns_shared.NS3 RS ns_shared.NS4 RS ns_shared.NS5) 2); |
40 ns_shared.NS3 RS ns_shared.NS4 RS ns_shared.NS5) 2); |
41 by possibility_tac; |
41 by possibility_tac; |
42 |
42 |
43 (**** Inductive proofs about ns_shared ****) |
43 (**** Inductive proofs about ns_shared ****) |
44 |
44 |
45 (*Nobody sends themselves messages*) |
45 (*Nobody sends themselves messages*) |
46 Goal "!!evs. evs : ns_shared ==> ALL A X. Says A A X ~: set evs"; |
46 Goal "evs : ns_shared ==> ALL A X. Says A A X ~: set evs"; |
47 by (etac ns_shared.induct 1); |
47 by (etac ns_shared.induct 1); |
48 by Auto_tac; |
48 by Auto_tac; |
49 qed_spec_mp "not_Says_to_self"; |
49 qed_spec_mp "not_Says_to_self"; |
50 Addsimps [not_Says_to_self]; |
50 Addsimps [not_Says_to_self]; |
51 AddSEs [not_Says_to_self RSN (2, rev_notE)]; |
51 AddSEs [not_Says_to_self RSN (2, rev_notE)]; |
52 |
52 |
53 (*For reasoning about the encrypted portion of message NS3*) |
53 (*For reasoning about the encrypted portion of message NS3*) |
54 Goal "!!evs. Says S A (Crypt KA {|N, B, K, X|}) : set evs \ |
54 Goal "Says S A (Crypt KA {|N, B, K, X|}) : set evs \ |
55 \ ==> X : parts (spies evs)"; |
55 \ ==> X : parts (spies evs)"; |
56 by (Blast_tac 1); |
56 by (Blast_tac 1); |
57 qed "NS3_msg_in_parts_spies"; |
57 qed "NS3_msg_in_parts_spies"; |
58 |
58 |
59 Goal |
59 Goal |
60 "!!evs. Says Server A (Crypt (shrK A) {|NA, B, K, X|}) : set evs \ |
60 "Says Server A (Crypt (shrK A) {|NA, B, K, X|}) : set evs \ |
61 \ ==> K : parts (spies evs)"; |
61 \ ==> K : parts (spies evs)"; |
62 by (Blast_tac 1); |
62 by (Blast_tac 1); |
63 qed "Oops_parts_spies"; |
63 qed "Oops_parts_spies"; |
64 |
64 |
65 (*For proving the easier theorems about X ~: parts (spies evs).*) |
65 (*For proving the easier theorems about X ~: parts (spies evs).*) |
74 (** Theorems of the form X ~: parts (spies evs) imply that NOBODY |
74 (** Theorems of the form X ~: parts (spies evs) imply that NOBODY |
75 sends messages containing X! **) |
75 sends messages containing X! **) |
76 |
76 |
77 (*Spy never sees another agent's shared key! (unless it's bad at start)*) |
77 (*Spy never sees another agent's shared key! (unless it's bad at start)*) |
78 Goal |
78 Goal |
79 "!!evs. evs : ns_shared ==> (Key (shrK A) : parts (spies evs)) = (A : bad)"; |
79 "evs : ns_shared ==> (Key (shrK A) : parts (spies evs)) = (A : bad)"; |
80 by (parts_induct_tac 1); |
80 by (parts_induct_tac 1); |
81 by (ALLGOALS Blast_tac); |
81 by (ALLGOALS Blast_tac); |
82 qed "Spy_see_shrK"; |
82 qed "Spy_see_shrK"; |
83 Addsimps [Spy_see_shrK]; |
83 Addsimps [Spy_see_shrK]; |
84 |
84 |
85 Goal |
85 Goal |
86 "!!evs. evs : ns_shared ==> (Key (shrK A) : analz (spies evs)) = (A : bad)"; |
86 "evs : ns_shared ==> (Key (shrK A) : analz (spies evs)) = (A : bad)"; |
87 by Auto_tac; |
87 by Auto_tac; |
88 qed "Spy_analz_shrK"; |
88 qed "Spy_analz_shrK"; |
89 Addsimps [Spy_analz_shrK]; |
89 Addsimps [Spy_analz_shrK]; |
90 |
90 |
91 AddSDs [Spy_see_shrK RSN (2, rev_iffD1), |
91 AddSDs [Spy_see_shrK RSN (2, rev_iffD1), |
92 Spy_analz_shrK RSN (2, rev_iffD1)]; |
92 Spy_analz_shrK RSN (2, rev_iffD1)]; |
93 |
93 |
94 |
94 |
95 (*Nobody can have used non-existent keys!*) |
95 (*Nobody can have used non-existent keys!*) |
96 Goal "!!evs. evs : ns_shared ==> \ |
96 Goal "evs : ns_shared ==> \ |
97 \ Key K ~: used evs --> K ~: keysFor (parts (spies evs))"; |
97 \ Key K ~: used evs --> K ~: keysFor (parts (spies evs))"; |
98 by (parts_induct_tac 1); |
98 by (parts_induct_tac 1); |
99 (*Fake*) |
99 (*Fake*) |
100 by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1); |
100 by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1); |
101 (*NS2, NS4, NS5*) |
101 (*NS2, NS4, NS5*) |
111 |
111 |
112 (** Lemmas concerning the form of items passed in messages **) |
112 (** Lemmas concerning the form of items passed in messages **) |
113 |
113 |
114 (*Describes the form of K, X and K' when the Server sends this message.*) |
114 (*Describes the form of K, X and K' when the Server sends this message.*) |
115 Goal |
115 Goal |
116 "!!evs. [| Says Server A (Crypt K' {|N, Agent B, Key K, X|}) : set evs; \ |
116 "[| Says Server A (Crypt K' {|N, Agent B, Key K, X|}) : set evs; \ |
117 \ evs : ns_shared |] \ |
117 \ evs : ns_shared |] \ |
118 \ ==> K ~: range shrK & \ |
118 \ ==> K ~: range shrK & \ |
119 \ X = (Crypt (shrK B) {|Key K, Agent A|}) & \ |
119 \ X = (Crypt (shrK B) {|Key K, Agent A|}) & \ |
120 \ K' = shrK A"; |
120 \ K' = shrK A"; |
121 by (etac rev_mp 1); |
121 by (etac rev_mp 1); |
124 qed "Says_Server_message_form"; |
124 qed "Says_Server_message_form"; |
125 |
125 |
126 |
126 |
127 (*If the encrypted message appears then it originated with the Server*) |
127 (*If the encrypted message appears then it originated with the Server*) |
128 Goal |
128 Goal |
129 "!!evs. [| Crypt (shrK A) {|NA, Agent B, Key K, X|} : parts (spies evs); \ |
129 "[| Crypt (shrK A) {|NA, Agent B, Key K, X|} : parts (spies evs); \ |
130 \ A ~: bad; evs : ns_shared |] \ |
130 \ A ~: bad; evs : ns_shared |] \ |
131 \ ==> Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|}) \ |
131 \ ==> Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|}) \ |
132 \ : set evs"; |
132 \ : set evs"; |
133 by (etac rev_mp 1); |
133 by (etac rev_mp 1); |
134 by (parts_induct_tac 1); |
134 by (parts_induct_tac 1); |
135 by (Blast_tac 1); |
135 by (Blast_tac 1); |
136 qed "A_trusts_NS2"; |
136 qed "A_trusts_NS2"; |
137 |
137 |
138 |
138 |
139 Goal |
139 Goal |
140 "!!evs. [| Crypt (shrK A) {|NA, Agent B, Key K, X|} : parts (spies evs); \ |
140 "[| Crypt (shrK A) {|NA, Agent B, Key K, X|} : parts (spies evs); \ |
141 \ A ~: bad; evs : ns_shared |] \ |
141 \ A ~: bad; evs : ns_shared |] \ |
142 \ ==> K ~: range shrK & X = (Crypt (shrK B) {|Key K, Agent A|})"; |
142 \ ==> K ~: range shrK & X = (Crypt (shrK B) {|Key K, Agent A|})"; |
143 by (blast_tac (claset() addSDs [A_trusts_NS2, Says_Server_message_form]) 1); |
143 by (blast_tac (claset() addSDs [A_trusts_NS2, Says_Server_message_form]) 1); |
144 qed "cert_A_form"; |
144 qed "cert_A_form"; |
145 |
145 |
146 |
146 |
147 (*EITHER describes the form of X when the following message is sent, |
147 (*EITHER describes the form of X when the following message is sent, |
148 OR reduces it to the Fake case. |
148 OR reduces it to the Fake case. |
149 Use Says_Server_message_form if applicable.*) |
149 Use Says_Server_message_form if applicable.*) |
150 Goal |
150 Goal |
151 "!!evs. [| Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|}) \ |
151 "[| Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|}) \ |
152 \ : set evs; \ |
152 \ : set evs; \ |
153 \ evs : ns_shared |] \ |
153 \ evs : ns_shared |] \ |
154 \ ==> (K ~: range shrK & X = (Crypt (shrK B) {|Key K, Agent A|})) \ |
154 \ ==> (K ~: range shrK & X = (Crypt (shrK B) {|Key K, Agent A|})) \ |
155 \ | X : analz (spies evs)"; |
155 \ | X : analz (spies evs)"; |
156 by (case_tac "A : bad" 1); |
156 by (case_tac "A : bad" 1); |
179 |
179 |
180 (*NOT useful in this form, but it says that session keys are not used |
180 (*NOT useful in this form, but it says that session keys are not used |
181 to encrypt messages containing other keys, in the actual protocol. |
181 to encrypt messages containing other keys, in the actual protocol. |
182 We require that agents should behave like this subsequently also.*) |
182 We require that agents should behave like this subsequently also.*) |
183 Goal |
183 Goal |
184 "!!evs. [| evs : ns_shared; Kab ~: range shrK |] ==> \ |
184 "[| evs : ns_shared; Kab ~: range shrK |] ==> \ |
185 \ (Crypt KAB X) : parts (spies evs) & \ |
185 \ (Crypt KAB X) : parts (spies evs) & \ |
186 \ Key K : parts {X} --> Key K : parts (spies evs)"; |
186 \ Key K : parts {X} --> Key K : parts (spies evs)"; |
187 by (parts_induct_tac 1); |
187 by (parts_induct_tac 1); |
188 (*Fake*) |
188 (*Fake*) |
189 by (blast_tac (claset() addSEs partsEs |
189 by (blast_tac (claset() addSEs partsEs |
195 |
195 |
196 (** Session keys are not used to encrypt other session keys **) |
196 (** Session keys are not used to encrypt other session keys **) |
197 |
197 |
198 (*The equality makes the induction hypothesis easier to apply*) |
198 (*The equality makes the induction hypothesis easier to apply*) |
199 Goal |
199 Goal |
200 "!!evs. evs : ns_shared ==> \ |
200 "evs : ns_shared ==> \ |
201 \ ALL K KK. KK <= Compl (range shrK) --> \ |
201 \ ALL K KK. KK <= Compl (range shrK) --> \ |
202 \ (Key K : analz (Key``KK Un (spies evs))) = \ |
202 \ (Key K : analz (Key``KK Un (spies evs))) = \ |
203 \ (K : KK | Key K : analz (spies evs))"; |
203 \ (K : KK | Key K : analz (spies evs))"; |
204 by (etac ns_shared.induct 1); |
204 by (etac ns_shared.induct 1); |
205 by analz_spies_tac; |
205 by analz_spies_tac; |
211 by (spy_analz_tac 1); |
211 by (spy_analz_tac 1); |
212 qed_spec_mp "analz_image_freshK"; |
212 qed_spec_mp "analz_image_freshK"; |
213 |
213 |
214 |
214 |
215 Goal |
215 Goal |
216 "!!evs. [| evs : ns_shared; KAB ~: range shrK |] ==> \ |
216 "[| evs : ns_shared; KAB ~: range shrK |] ==> \ |
217 \ Key K : analz (insert (Key KAB) (spies evs)) = \ |
217 \ Key K : analz (insert (Key KAB) (spies evs)) = \ |
218 \ (K = KAB | Key K : analz (spies evs))"; |
218 \ (K = KAB | Key K : analz (spies evs))"; |
219 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1); |
219 by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1); |
220 qed "analz_insert_freshK"; |
220 qed "analz_insert_freshK"; |
221 |
221 |
222 |
222 |
223 (** The session key K uniquely identifies the message **) |
223 (** The session key K uniquely identifies the message **) |
224 |
224 |
225 Goal |
225 Goal |
226 "!!evs. evs : ns_shared ==> \ |
226 "evs : ns_shared ==> \ |
227 \ EX A' NA' B' X'. ALL A NA B X. \ |
227 \ EX A' NA' B' X'. ALL A NA B X. \ |
228 \ Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|}) : set evs \ |
228 \ Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|}) : set evs \ |
229 \ --> A=A' & NA=NA' & B=B' & X=X'"; |
229 \ --> A=A' & NA=NA' & B=B' & X=X'"; |
230 by (etac ns_shared.induct 1); |
230 by (etac ns_shared.induct 1); |
231 by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); |
231 by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); |
239 by (Blast_tac 1); |
239 by (Blast_tac 1); |
240 val lemma = result(); |
240 val lemma = result(); |
241 |
241 |
242 (*In messages of this form, the session key uniquely identifies the rest*) |
242 (*In messages of this form, the session key uniquely identifies the rest*) |
243 Goal |
243 Goal |
244 "!!evs. [| Says Server A \ |
244 "[| Says Server A \ |
245 \ (Crypt (shrK A) {|NA, Agent B, Key K, X|}) : set evs; \ |
245 \ (Crypt (shrK A) {|NA, Agent B, Key K, X|}) : set evs; \ |
246 \ Says Server A' \ |
246 \ Says Server A' \ |
247 \ (Crypt (shrK A') {|NA', Agent B', Key K, X'|}) : set evs; \ |
247 \ (Crypt (shrK A') {|NA', Agent B', Key K, X'|}) : set evs; \ |
248 \ evs : ns_shared |] ==> A=A' & NA=NA' & B=B' & X = X'"; |
248 \ evs : ns_shared |] ==> A=A' & NA=NA' & B=B' & X = X'"; |
249 by (prove_unique_tac lemma 1); |
249 by (prove_unique_tac lemma 1); |
251 |
251 |
252 |
252 |
253 (** Crucial secrecy property: Spy does not see the keys sent in msg NS2 **) |
253 (** Crucial secrecy property: Spy does not see the keys sent in msg NS2 **) |
254 |
254 |
255 Goal |
255 Goal |
256 "!!evs. [| A ~: bad; B ~: bad; evs : ns_shared |] \ |
256 "[| A ~: bad; B ~: bad; evs : ns_shared |] \ |
257 \ ==> Says Server A \ |
257 \ ==> Says Server A \ |
258 \ (Crypt (shrK A) {|NA, Agent B, Key K, \ |
258 \ (Crypt (shrK A) {|NA, Agent B, Key K, \ |
259 \ Crypt (shrK B) {|Key K, Agent A|}|}) \ |
259 \ Crypt (shrK B) {|Key K, Agent A|}|}) \ |
260 \ : set evs --> \ |
260 \ : set evs --> \ |
261 \ (ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs) --> \ |
261 \ (ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs) --> \ |
284 val lemma = result() RS mp RS mp RSN(2,rev_notE); |
284 val lemma = result() RS mp RS mp RSN(2,rev_notE); |
285 |
285 |
286 |
286 |
287 (*Final version: Server's message in the most abstract form*) |
287 (*Final version: Server's message in the most abstract form*) |
288 Goal |
288 Goal |
289 "!!evs. [| Says Server A \ |
289 "[| Says Server A \ |
290 \ (Crypt K' {|NA, Agent B, Key K, X|}) : set evs; \ |
290 \ (Crypt K' {|NA, Agent B, Key K, X|}) : set evs; \ |
291 \ ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs; \ |
291 \ ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs; \ |
292 \ A ~: bad; B ~: bad; evs : ns_shared \ |
292 \ A ~: bad; B ~: bad; evs : ns_shared \ |
293 \ |] ==> Key K ~: analz (spies evs)"; |
293 \ |] ==> Key K ~: analz (spies evs)"; |
294 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); |
294 by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); |
301 A_trusts_NS2 RS Spy_not_see_encrypted_key; |
301 A_trusts_NS2 RS Spy_not_see_encrypted_key; |
302 |
302 |
303 |
303 |
304 (*If the encrypted message appears then it originated with the Server*) |
304 (*If the encrypted message appears then it originated with the Server*) |
305 Goal |
305 Goal |
306 "!!evs. [| Crypt (shrK B) {|Key K, Agent A|} : parts (spies evs); \ |
306 "[| Crypt (shrK B) {|Key K, Agent A|} : parts (spies evs); \ |
307 \ B ~: bad; evs : ns_shared |] \ |
307 \ B ~: bad; evs : ns_shared |] \ |
308 \ ==> EX NA. Says Server A \ |
308 \ ==> EX NA. Says Server A \ |
309 \ (Crypt (shrK A) {|NA, Agent B, Key K, \ |
309 \ (Crypt (shrK A) {|NA, Agent B, Key K, \ |
310 \ Crypt (shrK B) {|Key K, Agent A|}|}) \ |
310 \ Crypt (shrK B) {|Key K, Agent A|}|}) \ |
311 \ : set evs"; |
311 \ : set evs"; |
314 by (ALLGOALS Blast_tac); |
314 by (ALLGOALS Blast_tac); |
315 qed "B_trusts_NS3"; |
315 qed "B_trusts_NS3"; |
316 |
316 |
317 |
317 |
318 Goal |
318 Goal |
319 "!!evs. [| Crypt K (Nonce NB) : parts (spies evs); \ |
319 "[| Crypt K (Nonce NB) : parts (spies evs); \ |
320 \ Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|}) \ |
320 \ Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|}) \ |
321 \ : set evs; \ |
321 \ : set evs; \ |
322 \ Key K ~: analz (spies evs); \ |
322 \ Key K ~: analz (spies evs); \ |
323 \ evs : ns_shared |] \ |
323 \ evs : ns_shared |] \ |
324 \ ==> Says B A (Crypt K (Nonce NB)) : set evs"; |
324 \ ==> Says B A (Crypt K (Nonce NB)) : set evs"; |
341 qed "A_trusts_NS4_lemma"; |
341 qed "A_trusts_NS4_lemma"; |
342 |
342 |
343 |
343 |
344 (*This version no longer assumes that K is secure*) |
344 (*This version no longer assumes that K is secure*) |
345 Goal |
345 Goal |
346 "!!evs. [| Crypt K (Nonce NB) : parts (spies evs); \ |
346 "[| Crypt K (Nonce NB) : parts (spies evs); \ |
347 \ Crypt (shrK A) {|NA, Agent B, Key K, X|} : parts (spies evs); \ |
347 \ Crypt (shrK A) {|NA, Agent B, Key K, X|} : parts (spies evs); \ |
348 \ ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs; \ |
348 \ ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs; \ |
349 \ A ~: bad; B ~: bad; evs : ns_shared |] \ |
349 \ A ~: bad; B ~: bad; evs : ns_shared |] \ |
350 \ ==> Says B A (Crypt K (Nonce NB)) : set evs"; |
350 \ ==> Says B A (Crypt K (Nonce NB)) : set evs"; |
351 by (blast_tac (claset() addSIs [A_trusts_NS2, A_trusts_NS4_lemma] |
351 by (blast_tac (claset() addSIs [A_trusts_NS2, A_trusts_NS4_lemma] |
355 |
355 |
356 (*If the session key has been used in NS4 then somebody has forwarded |
356 (*If the session key has been used in NS4 then somebody has forwarded |
357 component X in some instance of NS4. Perhaps an interesting property, |
357 component X in some instance of NS4. Perhaps an interesting property, |
358 but not needed (after all) for the proofs below.*) |
358 but not needed (after all) for the proofs below.*) |
359 Goal |
359 Goal |
360 "!!evs. [| Crypt K (Nonce NB) : parts (spies evs); \ |
360 "[| Crypt K (Nonce NB) : parts (spies evs); \ |
361 \ Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|}) \ |
361 \ Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|}) \ |
362 \ : set evs; \ |
362 \ : set evs; \ |
363 \ Key K ~: analz (spies evs); \ |
363 \ Key K ~: analz (spies evs); \ |
364 \ evs : ns_shared |] \ |
364 \ evs : ns_shared |] \ |
365 \ ==> EX A'. Says A' B X : set evs"; |
365 \ ==> EX A'. Says A' B X : set evs"; |
382 by (blast_tac (claset() addDs [unique_session_keys]) 1); |
382 by (blast_tac (claset() addDs [unique_session_keys]) 1); |
383 qed "NS4_implies_NS3"; |
383 qed "NS4_implies_NS3"; |
384 |
384 |
385 |
385 |
386 Goal |
386 Goal |
387 "!!evs. [| B ~: bad; evs : ns_shared |] \ |
387 "[| B ~: bad; evs : ns_shared |] \ |
388 \ ==> Key K ~: analz (spies evs) --> \ |
388 \ ==> Key K ~: analz (spies evs) --> \ |
389 \ Says Server A \ |
389 \ Says Server A \ |
390 \ (Crypt (shrK A) {|NA, Agent B, Key K, \ |
390 \ (Crypt (shrK A) {|NA, Agent B, Key K, \ |
391 \ Crypt (shrK B) {|Key K, Agent A|}|}) \ |
391 \ Crypt (shrK B) {|Key K, Agent A|}|}) \ |
392 \ : set evs --> \ |
392 \ : set evs --> \ |
410 qed_spec_mp "B_trusts_NS5_lemma"; |
410 qed_spec_mp "B_trusts_NS5_lemma"; |
411 |
411 |
412 |
412 |
413 (*Very strong Oops condition reveals protocol's weakness*) |
413 (*Very strong Oops condition reveals protocol's weakness*) |
414 Goal |
414 Goal |
415 "!!evs. [| Crypt K {|Nonce NB, Nonce NB|} : parts (spies evs); \ |
415 "[| Crypt K {|Nonce NB, Nonce NB|} : parts (spies evs); \ |
416 \ Says B A (Crypt K (Nonce NB)) : set evs; \ |
416 \ Says B A (Crypt K (Nonce NB)) : set evs; \ |
417 \ Crypt (shrK B) {|Key K, Agent A|} : parts (spies evs); \ |
417 \ Crypt (shrK B) {|Key K, Agent A|} : parts (spies evs); \ |
418 \ ALL NA NB. Notes Spy {|NA, NB, Key K|} ~: set evs; \ |
418 \ ALL NA NB. Notes Spy {|NA, NB, Key K|} ~: set evs; \ |
419 \ A ~: bad; B ~: bad; evs : ns_shared |] \ |
419 \ A ~: bad; B ~: bad; evs : ns_shared |] \ |
420 \ ==> Says A B (Crypt K {|Nonce NB, Nonce NB|}) : set evs"; |
420 \ ==> Says A B (Crypt K {|Nonce NB, Nonce NB|}) : set evs"; |