332 (**** Secrecy Theorems ****) |
332 (**** Secrecy Theorems ****) |
333 |
333 |
334 (*Key compromise lemma needed to prove analz_image_keys. |
334 (*Key compromise lemma needed to prove analz_image_keys. |
335 No collection of keys can help the spy get new private keys.*) |
335 No collection of keys can help the spy get new private keys.*) |
336 Goal "evs : tls \ |
336 Goal "evs : tls \ |
337 \ ==> ALL KK. (Key(priK B) : analz (Key``KK Un (spies evs))) = \ |
337 \ ==> ALL KK. (Key(priK B) : analz (Key`KK Un (spies evs))) = \ |
338 \ (priK B : KK | B : bad)"; |
338 \ (priK B : KK | B : bad)"; |
339 by (etac tls.induct 1); |
339 by (etac tls.induct 1); |
340 by (ALLGOALS |
340 by (ALLGOALS |
341 (asm_simp_tac (analz_image_keys_ss |
341 (asm_simp_tac (analz_image_keys_ss |
342 addsimps certificate_def::keys_distinct))); |
342 addsimps certificate_def::keys_distinct))); |
355 \ (X : analz (G Un H)) = (X : analz H)"; |
355 \ (X : analz (G Un H)) = (X : analz H)"; |
356 by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1); |
356 by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1); |
357 val analz_image_keys_lemma = result(); |
357 val analz_image_keys_lemma = result(); |
358 |
358 |
359 (** Strangely, the following version doesn't work: |
359 (** Strangely, the following version doesn't work: |
360 \ ALL Z. (Nonce N : analz (Key``(sessionK``Z) Un (spies evs))) = \ |
360 \ ALL Z. (Nonce N : analz (Key`(sessionK`Z) Un (spies evs))) = \ |
361 \ (Nonce N : analz (spies evs))"; |
361 \ (Nonce N : analz (spies evs))"; |
362 **) |
362 **) |
363 |
363 |
364 Goal "evs : tls ==> \ |
364 Goal "evs : tls ==> \ |
365 \ ALL KK. KK <= range sessionK --> \ |
365 \ ALL KK. KK <= range sessionK --> \ |
366 \ (Nonce N : analz (Key``KK Un (spies evs))) = \ |
366 \ (Nonce N : analz (Key`KK Un (spies evs))) = \ |
367 \ (Nonce N : analz (spies evs))"; |
367 \ (Nonce N : analz (spies evs))"; |
368 by (etac tls.induct 1); |
368 by (etac tls.induct 1); |
369 by (ClientKeyExch_tac 7); |
369 by (ClientKeyExch_tac 7); |
370 by (REPEAT_FIRST (resolve_tac [allI, impI])); |
370 by (REPEAT_FIRST (resolve_tac [allI, impI])); |
371 by (REPEAT_FIRST (rtac analz_image_keys_lemma)); |
371 by (REPEAT_FIRST (rtac analz_image_keys_lemma)); |