src/HOL/Auth/KerberosIV.ML
changeset 10833 c0844a30ea4e
parent 9000 c20d58286a51
child 11104 f2024fed9f0c
equal deleted inserted replaced
10832:e33b47e4246d 10833:c0844a30ea4e
   607 (*The only session keys that can be found with the help of session keys are
   607 (*The only session keys that can be found with the help of session keys are
   608   those sent by Tgs in step K4.  *)
   608   those sent by Tgs in step K4.  *)
   609 
   609 
   610 (*We take some pains to express the property
   610 (*We take some pains to express the property
   611   as a logical equivalence so that the simplifier can apply it.*)
   611   as a logical equivalence so that the simplifier can apply it.*)
   612 Goal "P --> (Key K : analz (Key``KK Un H)) --> (K:KK | Key K : analz H)  \
   612 Goal "P --> (Key K : analz (Key`KK Un H)) --> (K:KK | Key K : analz H)  \
   613 \     ==>       \
   613 \     ==>       \
   614 \     P --> (Key K : analz (Key``KK Un H)) = (K:KK | Key K : analz H)";
   614 \     P --> (Key K : analz (Key`KK Un H)) = (K:KK | Key K : analz H)";
   615 by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1);
   615 by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1);
   616 qed "Key_analz_image_Key_lemma";
   616 qed "Key_analz_image_Key_lemma";
   617 
   617 
   618 Goal "[| KeyCryptKey K K' evs; evs : kerberos |] \
   618 Goal "[| KeyCryptKey K K' evs; evs : kerberos |] \
   619 \     ==> Key K' : analz (insert (Key K) (spies evs))";
   619 \     ==> Key K' : analz (insert (Key K) (spies evs))";
   649     ftac Says_kas_message_form 5, 
   649     ftac Says_kas_message_form 5, 
   650     REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE, exE]
   650     REPEAT_FIRST (eresolve_tac [asm_rl, conjE, disjE, exE]
   651 		  ORELSE' hyp_subst_tac)];
   651 		  ORELSE' hyp_subst_tac)];
   652 
   652 
   653 Goal "[| KK <= -(range shrK); Key K : analz (spies evs); evs: kerberos |]   \
   653 Goal "[| KK <= -(range shrK); Key K : analz (spies evs); evs: kerberos |]   \
   654 \     ==> Key K : analz (Key `` KK Un spies evs)";
   654 \     ==> Key K : analz (Key ` KK Un spies evs)";
   655 by (blast_tac (claset() addDs [impOfSubs analz_mono]) 1);
   655 by (blast_tac (claset() addDs [impOfSubs analz_mono]) 1);
   656 qed "analz_mono_KK";
   656 qed "analz_mono_KK";
   657 
   657 
   658 (*For the Oops2 case of the next theorem*)
   658 (*For the Oops2 case of the next theorem*)
   659 Goal "[| evs : kerberos;  \
   659 Goal "[| evs : kerberos;  \
   671 (* in case of loss of a key to the spy. See ESORICS98.                     *)
   671 (* in case of loss of a key to the spy. See ESORICS98.                     *)
   672 (* [simplified by LCP]                                                     *)
   672 (* [simplified by LCP]                                                     *)
   673 Goal "evs : kerberos ==>                                         \
   673 Goal "evs : kerberos ==>                                         \
   674 \     (ALL SK KK. KK <= -(range shrK) -->                   \
   674 \     (ALL SK KK. KK <= -(range shrK) -->                   \
   675 \     (ALL K: KK. ~ KeyCryptKey K SK evs)   -->           \
   675 \     (ALL K: KK. ~ KeyCryptKey K SK evs)   -->           \
   676 \     (Key SK : analz (Key``KK Un (spies evs))) =        \
   676 \     (Key SK : analz (Key`KK Un (spies evs))) =        \
   677 \     (SK : KK | Key SK : analz (spies evs)))";
   677 \     (SK : KK | Key SK : analz (spies evs)))";
   678 by (etac kerberos.induct 1);
   678 by (etac kerberos.induct 1);
   679 by analz_sees_tac;
   679 by analz_sees_tac;
   680 by (REPEAT_FIRST (rtac allI));
   680 by (REPEAT_FIRST (rtac allI));
   681 by (REPEAT_FIRST (rtac (Key_analz_image_Key_lemma RS impI)));
   681 by (REPEAT_FIRST (rtac (Key_analz_image_Key_lemma RS impI)));