src/HOL/Auth/NS_Shared.thy
changeset 11117 55358999077d
parent 11104 f2024fed9f0c
child 11150 67387142225e
equal deleted inserted replaced
11116:ac51bafd1afb 11117:55358999077d
   171        evs \<in> ns_shared\<rbrakk>
   171        evs \<in> ns_shared\<rbrakk>
   172       \<Longrightarrow> (K \<notin> range shrK \<and> X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>))
   172       \<Longrightarrow> (K \<notin> range shrK \<and> X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>))
   173           \<or> X \<in> analz (spies evs)"
   173           \<or> X \<in> analz (spies evs)"
   174 apply (frule Says_imp_knows_Spy)
   174 apply (frule Says_imp_knows_Spy)
   175 (*mystery: why is this frule needed?*)
   175 (*mystery: why is this frule needed?*)
   176 apply (blast dest: cert_A_form  analz.Inj)
   176 apply (blast dest: cert_A_form analz.Inj)
   177 done
   177 done
   178 
   178 
   179 (*Alternative version also provable
   179 (*Alternative version also provable
   180 lemma Says_S_message_form2:
   180 lemma Says_S_message_form2:
   181   "\<lbrakk>Says S A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
   181   "\<lbrakk>Says S A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
   222              (Key K \<in> analz (Key`KK \<union> (spies evs))) =
   222              (Key K \<in> analz (Key`KK \<union> (spies evs))) =
   223              (K \<in> KK \<or> Key K \<in> analz (spies evs))"
   223              (K \<in> KK \<or> Key K \<in> analz (spies evs))"
   224 apply (erule ns_shared.induct, force)
   224 apply (erule ns_shared.induct, force)
   225 apply (frule_tac [7] Says_Server_message_form)
   225 apply (frule_tac [7] Says_Server_message_form)
   226 apply (erule_tac [4] Says_S_message_form [THEN disjE])
   226 apply (erule_tac [4] Says_S_message_form [THEN disjE])
   227 apply (analz_freshK)
   227 apply analz_freshK
   228 apply (spy_analz)
   228 apply spy_analz
   229 done
   229 done
   230 
   230 
   231 
   231 
   232 lemma analz_insert_freshK:
   232 lemma analz_insert_freshK:
   233      "\<lbrakk>evs \<in> ns_shared;  KAB \<notin> range shrK\<rbrakk> \<Longrightarrow>
   233      "\<lbrakk>evs \<in> ns_shared;  KAB \<notin> range shrK\<rbrakk> \<Longrightarrow>