15 AddDs [Says_imp_knows_Spy RS parts.Inj, parts.Body]; |
15 AddDs [Says_imp_knows_Spy RS parts.Inj, parts.Body]; |
16 AddDs [impOfSubs analz_subset_parts, impOfSubs Fake_parts_insert]; |
16 AddDs [impOfSubs analz_subset_parts, impOfSubs Fake_parts_insert]; |
17 |
17 |
18 |
18 |
19 (*A "possibility property": there are traces that reach the end*) |
19 (*A "possibility property": there are traces that reach the end*) |
20 Goal "[| B ~= Server |] \ |
20 Goal "B ~= Server \ |
21 \ ==> EX NA K. EX evs: otway. \ |
21 \ ==> \\<exists>NA K. \\<exists>evs \\<in> otway. \ |
22 \ Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \ |
22 \ Says B A {|Nonce NA, Crypt (shrK A) {|Nonce NA, Key K|}|} \ |
23 \ : set evs"; |
23 \ : set evs"; |
24 by (REPEAT (resolve_tac [exI,bexI] 1)); |
24 by (REPEAT (resolve_tac [exI,bexI] 1)); |
25 by (rtac (otway.Nil RS |
25 by (rtac (otway.Nil RS |
26 otway.OR1 RS otway.Reception RS |
26 otway.OR1 RS otway.Reception RS |
27 otway.OR2 RS otway.Reception RS |
27 otway.OR2 RS otway.Reception RS |
28 otway.OR3 RS otway.Reception RS otway.OR4) 2); |
28 otway.OR3 RS otway.Reception RS otway.OR4) 2); |
29 by possibility_tac; |
29 by possibility_tac; |
30 result(); |
30 result(); |
31 |
31 |
32 Goal "[| Gets B X : set evs; evs : otway |] ==> EX A. Says A B X : set evs"; |
32 Goal "[| Gets B X : set evs; evs : otway |] ==> \\<exists>A. Says A B X : set evs"; |
33 by (etac rev_mp 1); |
33 by (etac rev_mp 1); |
34 by (etac otway.induct 1); |
34 by (etac otway.induct 1); |
35 by Auto_tac; |
35 by Auto_tac; |
36 qed"Gets_imp_Says"; |
36 qed"Gets_imp_Says"; |
37 |
37 |
64 bind_thm ("OR2_parts_knows_Spy", |
64 bind_thm ("OR2_parts_knows_Spy", |
65 OR2_analz_knows_Spy RS (impOfSubs analz_subset_parts)); |
65 OR2_analz_knows_Spy RS (impOfSubs analz_subset_parts)); |
66 bind_thm ("OR4_parts_knows_Spy", |
66 bind_thm ("OR4_parts_knows_Spy", |
67 OR4_analz_knows_Spy RS (impOfSubs analz_subset_parts)); |
67 OR4_analz_knows_Spy RS (impOfSubs analz_subset_parts)); |
68 |
68 |
69 (*For proving the easier theorems about X ~: parts (knows Spy evs).*) |
69 (*For proving the easier theorems about X \\<notin> parts (knows Spy evs).*) |
70 fun parts_induct_tac i = |
70 fun parts_induct_tac i = |
71 etac otway.induct i THEN |
71 etac otway.induct i THEN |
72 ftac Oops_parts_knows_Spy (i+7) THEN |
72 ftac Oops_parts_knows_Spy (i+7) THEN |
73 ftac OR4_parts_knows_Spy (i+6) THEN |
73 ftac OR4_parts_knows_Spy (i+6) THEN |
74 ftac OR2_parts_knows_Spy (i+4) THEN |
74 ftac OR2_parts_knows_Spy (i+4) THEN |
75 prove_simple_subgoals_tac i; |
75 prove_simple_subgoals_tac i; |
76 |
76 |
77 |
77 |
78 (** Theorems of the form X ~: parts (knows Spy evs) imply that NOBODY |
78 (** Theorems of the form X \\<notin> parts (knows Spy evs) imply that NOBODY |
79 sends messages containing X! **) |
79 sends messages containing X! **) |
80 |
80 |
81 (*Spy never sees a good agent's shared key!*) |
81 (*Spy never sees a good agent's shared key!*) |
82 Goal "evs : otway ==> (Key (shrK A) : parts (knows Spy evs)) = (A : bad)"; |
82 Goal "evs : otway ==> (Key (shrK A) : parts (knows Spy evs)) = (A : bad)"; |
83 by (parts_induct_tac 1); |
83 by (parts_induct_tac 1); |
92 |
92 |
93 AddSDs [Spy_see_shrK RSN (2, rev_iffD1), |
93 AddSDs [Spy_see_shrK RSN (2, rev_iffD1), |
94 Spy_analz_shrK RSN (2, rev_iffD1)]; |
94 Spy_analz_shrK RSN (2, rev_iffD1)]; |
95 |
95 |
96 |
96 |
97 (*Nobody can have used non-existent keys!*) |
|
98 Goal "evs: otway ==> Key K ~: used evs --> K ~: keysFor(parts(knows Spy evs))"; |
|
99 by (parts_induct_tac 1); |
|
100 (*Fake*) |
|
101 by (blast_tac (claset() addSDs [keysFor_parts_insert]) 1); |
|
102 (*OR2, OR3*) |
|
103 by (ALLGOALS Blast_tac); |
|
104 qed_spec_mp "new_keys_not_used"; |
|
105 Addsimps [new_keys_not_used]; |
|
106 |
|
107 |
|
108 |
|
109 (*** Proofs involving analz ***) |
97 (*** Proofs involving analz ***) |
110 |
98 |
111 (*Describes the form of K and NA when the Server sends this message. Also |
99 (*Describes the form of K and NA when the Server sends this message. Also |
112 for Oops case.*) |
100 for Oops case.*) |
113 Goal "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \ |
101 Goal "[| Says Server B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \ |
114 \ evs : otway |] \ |
102 \ evs : otway |] \ |
115 \ ==> K ~: range shrK & (EX i. NA = Nonce i) & (EX j. NB = Nonce j)"; |
103 \ ==> K \\<notin> range shrK & (\\<exists>i. NA = Nonce i) & (\\<exists>j. NB = Nonce j)"; |
116 by (etac rev_mp 1); |
104 by (etac rev_mp 1); |
117 by (etac otway.induct 1); |
105 by (etac otway.induct 1); |
118 by (ALLGOALS Simp_tac); |
106 by (ALLGOALS Simp_tac); |
119 by (ALLGOALS Blast_tac); |
107 by (ALLGOALS Blast_tac); |
120 qed "Says_Server_message_form"; |
108 qed "Says_Server_message_form"; |
176 |
164 |
177 |
165 |
178 (**** Authenticity properties relating to NA ****) |
166 (**** Authenticity properties relating to NA ****) |
179 |
167 |
180 (*Only OR1 can have caused such a part of a message to appear.*) |
168 (*Only OR1 can have caused such a part of a message to appear.*) |
181 Goal "[| A ~: bad; evs : otway |] \ |
169 Goal "[| A \\<notin> bad; evs : otway |] \ |
182 \ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (knows Spy evs) --> \ |
170 \ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (knows Spy evs) --> \ |
183 \ Says A B {|NA, Agent A, Agent B, \ |
171 \ Says A B {|NA, Agent A, Agent B, \ |
184 \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \ |
172 \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \ |
185 \ : set evs"; |
173 \ : set evs"; |
186 by (parts_induct_tac 1); |
174 by (parts_induct_tac 1); |
187 by (Blast_tac 1); |
175 by (Blast_tac 1); |
188 qed_spec_mp "Crypt_imp_OR1"; |
176 qed_spec_mp "Crypt_imp_OR1"; |
189 |
177 |
190 Goal "[| Gets B {|NA, Agent A, Agent B, \ |
178 Goal "[| Gets B {|NA, Agent A, Agent B, \ |
191 \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \ |
179 \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \ |
192 \ A ~: bad; evs : otway |] \ |
180 \ A \\<notin> bad; evs : otway |] \ |
193 \ ==> Says A B {|NA, Agent A, Agent B, \ |
181 \ ==> Says A B {|NA, Agent A, Agent B, \ |
194 \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \ |
182 \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} \ |
195 \ : set evs"; |
183 \ : set evs"; |
196 by (blast_tac (claset() addDs [Crypt_imp_OR1]) 1); |
184 by (blast_tac (claset() addDs [Crypt_imp_OR1]) 1); |
197 qed"Crypt_imp_OR1_Gets"; |
185 qed"Crypt_imp_OR1_Gets"; |
212 |
200 |
213 |
201 |
214 (*It is impossible to re-use a nonce in both OR1 and OR2. This holds because |
202 (*It is impossible to re-use a nonce in both OR1 and OR2. This holds because |
215 OR2 encrypts Nonce NB. It prevents the attack that can occur in the |
203 OR2 encrypts Nonce NB. It prevents the attack that can occur in the |
216 over-simplified version of this protocol: see OtwayRees_Bad.*) |
204 over-simplified version of this protocol: see OtwayRees_Bad.*) |
217 Goal "[| A ~: bad; evs : otway |] \ |
205 Goal "[| A \\<notin> bad; evs : otway |] \ |
218 \ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (knows Spy evs) --> \ |
206 \ ==> Crypt (shrK A) {|NA, Agent A, Agent B|} : parts (knows Spy evs) --> \ |
219 \ Crypt (shrK A) {|NA', NA, Agent A', Agent A|} \ |
207 \ Crypt (shrK A) {|NA', NA, Agent A', Agent A|} \ |
220 \ ~: parts (knows Spy evs)"; |
208 \ \\<notin> parts (knows Spy evs)"; |
221 by (parts_induct_tac 1); |
209 by (parts_induct_tac 1); |
222 by Auto_tac; |
210 by Auto_tac; |
223 qed_spec_mp "no_nonce_OR1_OR2"; |
211 qed_spec_mp "no_nonce_OR1_OR2"; |
224 |
212 |
225 val nonce_OR1_OR2_E = no_nonce_OR1_OR2 RSN (2, rev_notE); |
213 val nonce_OR1_OR2_E = no_nonce_OR1_OR2 RSN (2, rev_notE); |
226 |
214 |
227 (*Crucial property: If the encrypted message appears, and A has used NA |
215 (*Crucial property: If the encrypted message appears, and A has used NA |
228 to start a run, then it originated with the Server!*) |
216 to start a run, then it originated with the Server!*) |
229 Goal "[| A ~: bad; evs : otway |] \ |
217 Goal "[| A \\<notin> bad; evs : otway |] \ |
230 \ ==> Says A B {|NA, Agent A, Agent B, \ |
218 \ ==> Says A B {|NA, Agent A, Agent B, \ |
231 \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs --> \ |
219 \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs --> \ |
232 \ Crypt (shrK A) {|NA, Key K|} : parts (knows Spy evs) \ |
220 \ Crypt (shrK A) {|NA, Key K|} : parts (knows Spy evs) \ |
233 \ --> (EX NB. Says Server B \ |
221 \ --> (\\<exists>NB. Says Server B \ |
234 \ {|NA, \ |
222 \ {|NA, \ |
235 \ Crypt (shrK A) {|NA, Key K|}, \ |
223 \ Crypt (shrK A) {|NA, Key K|}, \ |
236 \ Crypt (shrK B) {|NB, Key K|}|} : set evs)"; |
224 \ Crypt (shrK B) {|NB, Key K|}|} : set evs)"; |
237 by (parts_induct_tac 1); |
225 by (parts_induct_tac 1); |
238 by (Blast_tac 1); |
226 by (Blast_tac 1); |
250 bad form of this protocol, even though we can prove |
238 bad form of this protocol, even though we can prove |
251 Spy_not_see_encrypted_key*) |
239 Spy_not_see_encrypted_key*) |
252 Goal "[| Says A B {|NA, Agent A, Agent B, \ |
240 Goal "[| Says A B {|NA, Agent A, Agent B, \ |
253 \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \ |
241 \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \ |
254 \ Gets A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \ |
242 \ Gets A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \ |
255 \ A ~: bad; evs : otway |] \ |
243 \ A \\<notin> bad; evs : otway |] \ |
256 \ ==> EX NB. Says Server B \ |
244 \ ==> \\<exists>NB. Says Server B \ |
257 \ {|NA, \ |
245 \ {|NA, \ |
258 \ Crypt (shrK A) {|NA, Key K|}, \ |
246 \ Crypt (shrK A) {|NA, Key K|}, \ |
259 \ Crypt (shrK B) {|NB, Key K|}|} \ |
247 \ Crypt (shrK B) {|NB, Key K|}|} \ |
260 \ : set evs"; |
248 \ : set evs"; |
261 by (blast_tac (claset() addSIs [NA_Crypt_imp_Server_msg]) 1); |
249 by (blast_tac (claset() addSIs [NA_Crypt_imp_Server_msg]) 1); |
264 |
252 |
265 (** Crucial secrecy property: Spy does not see the keys sent in msg OR3 |
253 (** Crucial secrecy property: Spy does not see the keys sent in msg OR3 |
266 Does not in itself guarantee security: an attack could violate |
254 Does not in itself guarantee security: an attack could violate |
267 the premises, e.g. by having A=Spy **) |
255 the premises, e.g. by having A=Spy **) |
268 |
256 |
269 Goal "[| A ~: bad; B ~: bad; evs : otway |] \ |
257 Goal "[| A \\<notin> bad; B \\<notin> bad; evs : otway |] \ |
270 \ ==> Says Server B \ |
258 \ ==> Says Server B \ |
271 \ {|NA, Crypt (shrK A) {|NA, Key K|}, \ |
259 \ {|NA, Crypt (shrK A) {|NA, Key K|}, \ |
272 \ Crypt (shrK B) {|NB, Key K|}|} : set evs --> \ |
260 \ Crypt (shrK B) {|NB, Key K|}|} : set evs --> \ |
273 \ Notes Spy {|NA, NB, Key K|} ~: set evs --> \ |
261 \ Notes Spy {|NA, NB, Key K|} \\<notin> set evs --> \ |
274 \ Key K ~: analz (knows Spy evs)"; |
262 \ Key K \\<notin> analz (knows Spy evs)"; |
275 by (etac otway.induct 1); |
263 by (etac otway.induct 1); |
276 by analz_knows_Spy_tac; |
264 by analz_knows_Spy_tac; |
277 by (ALLGOALS |
265 by (ALLGOALS |
278 (asm_simp_tac (simpset() addcongs [conj_cong] |
266 (asm_simp_tac (simpset() addcongs [conj_cong] |
279 addsimps [analz_insert_eq, analz_insert_freshK] |
267 addsimps [analz_insert_eq, analz_insert_freshK] |
289 val lemma = result() RS mp RS mp RSN(2,rev_notE); |
277 val lemma = result() RS mp RS mp RSN(2,rev_notE); |
290 |
278 |
291 Goal "[| Says Server B \ |
279 Goal "[| Says Server B \ |
292 \ {|NA, Crypt (shrK A) {|NA, Key K|}, \ |
280 \ {|NA, Crypt (shrK A) {|NA, Key K|}, \ |
293 \ Crypt (shrK B) {|NB, Key K|}|} : set evs; \ |
281 \ Crypt (shrK B) {|NB, Key K|}|} : set evs; \ |
294 \ Notes Spy {|NA, NB, Key K|} ~: set evs; \ |
282 \ Notes Spy {|NA, NB, Key K|} \\<notin> set evs; \ |
295 \ A ~: bad; B ~: bad; evs : otway |] \ |
283 \ A \\<notin> bad; B \\<notin> bad; evs : otway |] \ |
296 \ ==> Key K ~: analz (knows Spy evs)"; |
284 \ ==> Key K \\<notin> analz (knows Spy evs)"; |
297 by (blast_tac (claset() addDs [Says_Server_message_form] addSEs [lemma]) 1); |
285 by (blast_tac (claset() addDs [Says_Server_message_form] addSEs [lemma]) 1); |
298 qed "Spy_not_see_encrypted_key"; |
286 qed "Spy_not_see_encrypted_key"; |
299 |
287 |
300 |
288 |
301 (*A's guarantee. The Oops premise quantifies over NB because A cannot know |
289 (*A's guarantee. The Oops premise quantifies over NB because A cannot know |
302 what it is.*) |
290 what it is.*) |
303 Goal "[| Says A B {|NA, Agent A, Agent B, \ |
291 Goal "[| Says A B {|NA, Agent A, Agent B, \ |
304 \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \ |
292 \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \ |
305 \ Gets A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \ |
293 \ Gets A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \ |
306 \ ALL NB. Notes Spy {|NA, NB, Key K|} ~: set evs; \ |
294 \ ALL NB. Notes Spy {|NA, NB, Key K|} \\<notin> set evs; \ |
307 \ A ~: bad; B ~: bad; evs : otway |] \ |
295 \ A \\<notin> bad; B \\<notin> bad; evs : otway |] \ |
308 \ ==> Key K ~: analz (knows Spy evs)"; |
296 \ ==> Key K \\<notin> analz (knows Spy evs)"; |
309 by (blast_tac (claset() addSDs [A_trusts_OR4, Spy_not_see_encrypted_key]) 1); |
297 by (blast_tac (claset() addSDs [A_trusts_OR4, Spy_not_see_encrypted_key]) 1); |
310 qed "A_gets_good_key"; |
298 qed "A_gets_good_key"; |
311 |
299 |
312 |
300 |
313 (**** Authenticity properties relating to NB ****) |
301 (**** Authenticity properties relating to NB ****) |
314 |
302 |
315 (*Only OR2 can have caused such a part of a message to appear. We do not |
303 (*Only OR2 can have caused such a part of a message to appear. We do not |
316 know anything about X: it does NOT have to have the right form.*) |
304 know anything about X: it does NOT have to have the right form.*) |
317 Goal "[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \ |
305 Goal "[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} \ |
318 \ : parts (knows Spy evs); \ |
306 \ : parts (knows Spy evs); \ |
319 \ B ~: bad; evs : otway |] \ |
307 \ B \\<notin> bad; evs : otway |] \ |
320 \ ==> EX X. Says B Server \ |
308 \ ==> \\<exists>X. Says B Server \ |
321 \ {|NA, Agent A, Agent B, X, \ |
309 \ {|NA, Agent A, Agent B, X, \ |
322 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|} \ |
310 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|} \ |
323 \ : set evs"; |
311 \ : set evs"; |
324 by (etac rev_mp 1); |
312 by (etac rev_mp 1); |
325 by (parts_induct_tac 1); |
313 by (parts_induct_tac 1); |
329 |
317 |
330 (** The Nonce NB uniquely identifies B's message. **) |
318 (** The Nonce NB uniquely identifies B's message. **) |
331 |
319 |
332 Goal "[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(knows Spy evs); \ |
320 Goal "[| Crypt (shrK B) {|NA, NB, Agent A, Agent B|} : parts(knows Spy evs); \ |
333 \ Crypt (shrK B) {|NC, NB, Agent C, Agent B|} : parts(knows Spy evs); \ |
321 \ Crypt (shrK B) {|NC, NB, Agent C, Agent B|} : parts(knows Spy evs); \ |
334 \ evs : otway; B ~: bad |] \ |
322 \ evs : otway; B \\<notin> bad |] \ |
335 \ ==> NC = NA & C = A"; |
323 \ ==> NC = NA & C = A"; |
336 by (etac rev_mp 1); |
324 by (etac rev_mp 1); |
337 by (etac rev_mp 1); |
325 by (etac rev_mp 1); |
338 by (parts_induct_tac 1); |
326 by (parts_induct_tac 1); |
339 (*Fake, OR2*) |
327 (*Fake, OR2*) |
340 by (REPEAT (Blast_tac 1)); |
328 by (REPEAT (Blast_tac 1)); |
341 qed "unique_NB"; |
329 qed "unique_NB"; |
342 |
330 |
343 (*If the encrypted message appears, and B has used Nonce NB, |
331 (*If the encrypted message appears, and B has used Nonce NB, |
344 then it originated with the Server! Quite messy proof.*) |
332 then it originated with the Server! Quite messy proof.*) |
345 Goal "[| B ~: bad; evs : otway |] \ |
333 Goal "[| B \\<notin> bad; evs : otway |] \ |
346 \ ==> Crypt (shrK B) {|NB, Key K|} : parts (knows Spy evs) \ |
334 \ ==> Crypt (shrK B) {|NB, Key K|} : parts (knows Spy evs) \ |
347 \ --> (ALL X'. Says B Server \ |
335 \ --> (ALL X'. Says B Server \ |
348 \ {|NA, Agent A, Agent B, X', \ |
336 \ {|NA, Agent A, Agent B, X', \ |
349 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|} \ |
337 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|}|} \ |
350 \ : set evs \ |
338 \ : set evs \ |
369 has sent the correct message.*) |
357 has sent the correct message.*) |
370 Goal "[| Says B Server {|NA, Agent A, Agent B, X', \ |
358 Goal "[| Says B Server {|NA, Agent A, Agent B, X', \ |
371 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \ |
359 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \ |
372 \ : set evs; \ |
360 \ : set evs; \ |
373 \ Gets B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \ |
361 \ Gets B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \ |
374 \ B ~: bad; evs : otway |] \ |
362 \ B \\<notin> bad; evs : otway |] \ |
375 \ ==> Says Server B \ |
363 \ ==> Says Server B \ |
376 \ {|NA, \ |
364 \ {|NA, \ |
377 \ Crypt (shrK A) {|NA, Key K|}, \ |
365 \ Crypt (shrK A) {|NA, Key K|}, \ |
378 \ Crypt (shrK B) {|NB, Key K|}|} \ |
366 \ Crypt (shrK B) {|NB, Key K|}|} \ |
379 \ : set evs"; |
367 \ : set evs"; |
384 (*The obvious combination of B_trusts_OR3 with Spy_not_see_encrypted_key*) |
372 (*The obvious combination of B_trusts_OR3 with Spy_not_see_encrypted_key*) |
385 Goal "[| Says B Server {|NA, Agent A, Agent B, X', \ |
373 Goal "[| Says B Server {|NA, Agent A, Agent B, X', \ |
386 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \ |
374 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \ |
387 \ : set evs; \ |
375 \ : set evs; \ |
388 \ Gets B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \ |
376 \ Gets B {|NA, X, Crypt (shrK B) {|NB, Key K|}|} : set evs; \ |
389 \ Notes Spy {|NA, NB, Key K|} ~: set evs; \ |
377 \ Notes Spy {|NA, NB, Key K|} \\<notin> set evs; \ |
390 \ A ~: bad; B ~: bad; evs : otway |] \ |
378 \ A \\<notin> bad; B \\<notin> bad; evs : otway |] \ |
391 \ ==> Key K ~: analz (knows Spy evs)"; |
379 \ ==> Key K \\<notin> analz (knows Spy evs)"; |
392 by (blast_tac (claset() addSDs [B_trusts_OR3, Spy_not_see_encrypted_key]) 1); |
380 by (blast_tac (claset() addSDs [B_trusts_OR3, Spy_not_see_encrypted_key]) 1); |
393 qed "B_gets_good_key"; |
381 qed "B_gets_good_key"; |
394 |
382 |
395 |
383 |
396 Goal "[| Says Server B \ |
384 Goal "[| Says Server B \ |
397 \ {|NA, Crypt (shrK A) {|NA, Key K|}, \ |
385 \ {|NA, Crypt (shrK A) {|NA, Key K|}, \ |
398 \ Crypt (shrK B) {|NB, Key K|}|} : set evs; \ |
386 \ Crypt (shrK B) {|NB, Key K|}|} : set evs; \ |
399 \ B ~: bad; evs : otway |] \ |
387 \ B \\<notin> bad; evs : otway |] \ |
400 \ ==> EX X. Says B Server {|NA, Agent A, Agent B, X, \ |
388 \ ==> \\<exists>X. Says B Server {|NA, Agent A, Agent B, X, \ |
401 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \ |
389 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |} \ |
402 \ : set evs"; |
390 \ : set evs"; |
403 by (etac rev_mp 1); |
391 by (etac rev_mp 1); |
404 by (etac otway.induct 1); |
392 by (etac otway.induct 1); |
405 by (ALLGOALS Asm_simp_tac); |
393 by (ALLGOALS Asm_simp_tac); |
412 We could probably prove that X has the expected form, but that is not |
400 We could probably prove that X has the expected form, but that is not |
413 strictly necessary for authentication.*) |
401 strictly necessary for authentication.*) |
414 Goal "[| Gets A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \ |
402 Goal "[| Gets A {|NA, Crypt (shrK A) {|NA, Key K|}|} : set evs; \ |
415 \ Says A B {|NA, Agent A, Agent B, \ |
403 \ Says A B {|NA, Agent A, Agent B, \ |
416 \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \ |
404 \ Crypt (shrK A) {|NA, Agent A, Agent B|}|} : set evs; \ |
417 \ A ~: bad; B ~: bad; evs : otway |] \ |
405 \ A \\<notin> bad; B \\<notin> bad; evs : otway |] \ |
418 \ ==> EX NB X. Says B Server {|NA, Agent A, Agent B, X, \ |
406 \ ==> \\<exists>NB X. Says B Server {|NA, Agent A, Agent B, X, \ |
419 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |}\ |
407 \ Crypt (shrK B) {|NA, NB, Agent A, Agent B|} |}\ |
420 \ : set evs"; |
408 \ : set evs"; |
421 by (blast_tac (claset() delrules [Gets_imp_knows_Spy RS parts.Inj] |
409 by (blast_tac (claset() delrules [Gets_imp_knows_Spy RS parts.Inj] |
422 addSDs [A_trusts_OR4, OR3_imp_OR2]) 1); |
410 addSDs [A_trusts_OR4, OR3_imp_OR2]) 1); |
423 qed "A_auths_B"; |
411 qed "A_auths_B"; |