streamlined a proof
authorpaulson
Fri Mar 02 13:14:37 2001 +0100 (2001-03-02)
changeset 111885d539f1682c3
parent 11187 c6e49929e544
child 11189 1ea763a5d186
streamlined a proof
src/HOL/Auth/NS_Shared.thy
     1.1 --- a/src/HOL/Auth/NS_Shared.thy	Wed Feb 28 12:37:48 2001 +0100
     1.2 +++ b/src/HOL/Auth/NS_Shared.thy	Fri Mar 02 13:14:37 2001 +0100
     1.3 @@ -269,15 +269,15 @@
     1.4  apply (simp_all add: analz_insert_eq analz_insert_freshK pushes split_ifs)
     1.5  apply spy_analz  (*Fake*) 
     1.6  apply blast      (*NS2*)
     1.7 -(*NS3, Server sub-case*) (**LEVEL 6 **)
     1.8 -apply clarify
     1.9 -apply (frule Says_imp_knows_Spy [THEN parts.Inj, THEN A_trusts_NS2])
    1.10 -apply (blast dest: Says_imp_knows_Spy analz.Inj Crypt_Spy_analz_bad)
    1.11 -apply assumption
    1.12 -apply (blast dest: unique_session_keys)+ (*also proves Oops*)
    1.13 +(*NS3, Server sub-case*) (**LEVEL 8 **)
    1.14 +apply (blast dest!: Crypt_Spy_analz_bad A_trusts_NS2
    1.15 +	     dest:  Says_imp_knows_Spy analz.Inj unique_session_keys)
    1.16 +(*NS3, Spy sub-case; also Oops*) 
    1.17 +apply (blast dest: unique_session_keys)+ 
    1.18  done
    1.19  
    1.20  
    1.21 +
    1.22  (*Final version: Server's message in the most abstract form*)
    1.23  lemma Spy_not_see_encrypted_key:
    1.24       "\<lbrakk>Says Server A (Crypt K' \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs;