src/HOL/Auth/NS_Shared.thy
changeset 11150 67387142225e
parent 11117 55358999077d
child 11188 5d539f1682c3
     1.1 --- a/src/HOL/Auth/NS_Shared.thy	Fri Feb 16 08:27:17 2001 +0100
     1.2 +++ b/src/HOL/Auth/NS_Shared.thy	Fri Feb 16 13:25:08 2001 +0100
     1.3 @@ -71,9 +71,13 @@
     1.4  	      \<in> set evso\<rbrakk>
     1.5  	 \<Longrightarrow> Notes Spy \<lbrace>Nonce NA, Nonce NB, Key K\<rbrace> # evso \<in> ns_shared"
     1.6  
     1.7 -declare knows_Spy_partsEs [elim]
     1.8 +
     1.9 +declare Says_imp_knows_Spy [THEN parts.Inj, dest]
    1.10 +declare parts.Body  [dest]
    1.11 +declare MPair_parts [elim!]    (*can speed up some proofs*)
    1.12 +
    1.13  declare analz_subset_parts [THEN subsetD, dest]
    1.14 -declare Fake_parts_insert [THEN subsetD, dest]
    1.15 +declare Fake_parts_insert  [THEN subsetD, dest]
    1.16  declare image_eq_UN [simp]  (*accelerates proofs involving nested images*)
    1.17  
    1.18  
    1.19 @@ -171,10 +175,8 @@
    1.20         evs \<in> ns_shared\<rbrakk>
    1.21        \<Longrightarrow> (K \<notin> range shrK \<and> X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>))
    1.22            \<or> X \<in> analz (spies evs)"
    1.23 -apply (frule Says_imp_knows_Spy)
    1.24 -(*mystery: why is this frule needed?*)
    1.25 -apply (blast dest: cert_A_form analz.Inj)
    1.26 -done
    1.27 +by (blast dest: Says_imp_knows_Spy cert_A_form analz.Inj)
    1.28 +
    1.29  
    1.30  (*Alternative version also provable
    1.31  lemma Says_S_message_form2:
    1.32 @@ -251,7 +253,8 @@
    1.33  
    1.34  (** Crucial secrecy property: Spy does not see the keys sent in msg NS2 **)
    1.35  
    1.36 -lemma secrecy_lemma [rule_format]:
    1.37 +(*Beware of [rule_format] and the universal quantifier!*)
    1.38 +lemma secrecy_lemma:
    1.39       "\<lbrakk>Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
    1.40                                        Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>)
    1.41                \<in> set evs;
    1.42 @@ -269,7 +272,7 @@
    1.43  (*NS3, Server sub-case*) (**LEVEL 6 **)
    1.44  apply clarify
    1.45  apply (frule Says_imp_knows_Spy [THEN parts.Inj, THEN A_trusts_NS2])
    1.46 -apply (blast dest: Says_imp_knows_Spy [THEN analz.Inj, THEN Crypt_Spy_analz_bad])
    1.47 +apply (blast dest: Says_imp_knows_Spy analz.Inj Crypt_Spy_analz_bad)
    1.48  apply assumption
    1.49  apply (blast dest: unique_session_keys)+ (*also proves Oops*)
    1.50  done
    1.51 @@ -281,9 +284,7 @@
    1.52         \<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
    1.53         A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
    1.54        \<Longrightarrow> Key K \<notin> analz (spies evs)"
    1.55 -apply (frule Says_Server_message_form, assumption)
    1.56 -apply (auto dest: Says_Server_message_form secrecy_lemma)
    1.57 -done
    1.58 +by (blast dest: Says_Server_message_form secrecy_lemma)
    1.59  
    1.60  
    1.61  (**** Guarantees available at various stages of protocol ***)
    1.62 @@ -291,8 +292,8 @@
    1.63  (*If the encrypted message appears then it originated with the Server*)
    1.64  lemma B_trusts_NS3:
    1.65       "\<lbrakk>Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace> \<in> parts (spies evs);
    1.66 -            B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
    1.67 -          \<Longrightarrow> \<exists>NA. Says Server A
    1.68 +       B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
    1.69 +      \<Longrightarrow> \<exists>NA. Says Server A
    1.70                 (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
    1.71                                   Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>)
    1.72                \<in> set evs"
    1.73 @@ -317,10 +318,9 @@
    1.74  apply (force dest!: Crypt_imp_keysFor) 
    1.75  apply blast     (*NS3*)
    1.76  (*NS4*)
    1.77 -apply clarify;
    1.78 -apply (frule Says_imp_knows_Spy [THEN analz.Inj])
    1.79 -apply (blast dest: Says_imp_knows_Spy [THEN analz.Inj] Crypt_Spy_analz_bad
    1.80 -                   B_trusts_NS3 unique_session_keys)
    1.81 +apply (blast dest!: B_trusts_NS3
    1.82 +	     dest: Says_imp_knows_Spy [THEN analz.Inj] 
    1.83 +                   Crypt_Spy_analz_bad unique_session_keys)
    1.84  done
    1.85  
    1.86  (*This version no longer assumes that K is secure*)
    1.87 @@ -349,11 +349,9 @@
    1.88  apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)  (*NS2*)
    1.89  apply blast  (*NS3*)
    1.90  (*NS4*)
    1.91 -apply (case_tac "Ba \<in> bad")
    1.92 -apply (blast dest: Says_imp_knows_Spy [THEN analz.Inj] Crypt_Spy_analz_bad);
    1.93 -apply (frule Says_imp_knows_Spy [THEN parts.Inj, THEN B_trusts_NS3], 
    1.94 -       assumption+)
    1.95 -apply (blast dest: unique_session_keys)
    1.96 +apply (blast dest!: B_trusts_NS3
    1.97 +	     dest: Says_imp_knows_Spy [THEN analz.Inj] 
    1.98 +                   unique_session_keys Crypt_Spy_analz_bad)
    1.99  done
   1.100  
   1.101  
   1.102 @@ -371,12 +369,10 @@
   1.103  apply blast  (*Fake*)
   1.104  apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)  (*NS2*)
   1.105  apply (blast dest!: cert_A_form) (*NS3*)
   1.106 -(**LEVEL 5**)
   1.107  (*NS5*)
   1.108 -apply clarify
   1.109 -apply (case_tac "Aa \<in> bad")
   1.110 -apply (blast dest: Says_imp_knows_Spy [THEN analz.Inj] Crypt_Spy_analz_bad);
   1.111 -apply (blast dest: A_trusts_NS2 unique_session_keys)
   1.112 +apply (blast dest!: A_trusts_NS2
   1.113 +	     dest: Says_imp_knows_Spy [THEN analz.Inj] 
   1.114 +                   unique_session_keys Crypt_Spy_analz_bad)
   1.115  done
   1.116  
   1.117  
   1.118 @@ -387,10 +383,7 @@
   1.119         \<forall>NA NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
   1.120         A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
   1.121        \<Longrightarrow> Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) \<in> set evs"
   1.122 -apply (drule B_trusts_NS3, clarify+)
   1.123 -apply (blast intro: B_trusts_NS5_lemma 
   1.124 -             dest: dest: Spy_not_see_encrypted_key)
   1.125 -(*surprisingly delicate proof due to quantifier interactions*)
   1.126 -done
   1.127 +by (blast intro: B_trusts_NS5_lemma 
   1.128 +          dest: B_trusts_NS3 Spy_not_see_encrypted_key)
   1.129  
   1.130  end