minor tweaks
authorpaulson
Thu May 03 10:27:37 2001 +0200 (2001-05-03)
changeset 112806fdc4c4ccec1
parent 11279 aaa0ad8fea6b
child 11281 f2a284b2d588
minor tweaks
src/HOL/Auth/NS_Shared.thy
     1.1 --- a/src/HOL/Auth/NS_Shared.thy	Thu May 03 10:27:04 2001 +0200
     1.2 +++ b/src/HOL/Auth/NS_Shared.thy	Thu May 03 10:27:37 2001 +0200
     1.3 @@ -33,10 +33,10 @@
     1.4  	      the sender field.*)
     1.5    NS2:  "\<lbrakk>evs2 \<in> ns_shared;  Key KAB \<notin> used evs2;
     1.6  	  Says A' Server \<lbrace>Agent A, Agent B, Nonce NA\<rbrace> \<in> set evs2\<rbrakk>
     1.7 -	 \<Longrightarrow> Says Server A 
     1.8 +	 \<Longrightarrow> Says Server A
     1.9  	       (Crypt (shrK A)
    1.10  		  \<lbrace>Nonce NA, Agent B, Key KAB,
    1.11 -		    (Crypt (shrK B) \<lbrace>Key KAB, Agent A\<rbrace>)\<rbrace>) 
    1.12 +		    (Crypt (shrK B) \<lbrace>Key KAB, Agent A\<rbrace>)\<rbrace>)
    1.13  	       # evs2 \<in> ns_shared"
    1.14  
    1.15  	 (*We can't assume S=Server.  Agent A "remembers" her nonce.
    1.16 @@ -57,7 +57,7 @@
    1.17  	  We do NOT send NB-1 or similar as the Spy cannot spoof such things.
    1.18  	  Letting the Spy add or subtract 1 lets him send \<forall>nonces.
    1.19  	  Instead we distinguish the messages by sending the nonce twice.*)
    1.20 -  NS5:  "\<lbrakk>evs5 \<in> ns_shared;  
    1.21 +  NS5:  "\<lbrakk>evs5 \<in> ns_shared;
    1.22  	  Says B' A (Crypt K (Nonce NB)) \<in> set evs5;
    1.23  	  Says S  A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>)
    1.24  	    \<in> set evs5\<rbrakk>
    1.25 @@ -97,13 +97,13 @@
    1.26  
    1.27  (**** Inductive proofs about ns_shared ****)
    1.28  
    1.29 -(*Forwarding lemmas, to aid simplification*)
    1.30 +(** Forwarding lemmas, to aid simplification **)
    1.31  
    1.32  (*For reasoning about the encrypted portion of message NS3*)
    1.33  lemma NS3_msg_in_parts_spies:
    1.34       "Says S A (Crypt KA \<lbrace>N, B, K, X\<rbrace>) \<in> set evs \<Longrightarrow> X \<in> parts (spies evs)"
    1.35  by blast
    1.36 -                              
    1.37 +
    1.38  (*For reasoning about the Oops message*)
    1.39  lemma Oops_parts_spies:
    1.40       "Says Server A (Crypt (shrK A) \<lbrace>NA, B, K, X\<rbrace>) \<in> set evs
    1.41 @@ -116,7 +116,7 @@
    1.42  (*Spy never sees another agent's shared key! (unless it's bad at start)*)
    1.43  lemma Spy_see_shrK [simp]:
    1.44       "evs \<in> ns_shared \<Longrightarrow> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
    1.45 -apply (erule ns_shared.induct, force, frule_tac [4] NS3_msg_in_parts_spies)
    1.46 +apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
    1.47  apply simp_all
    1.48  apply blast+;
    1.49  done
    1.50 @@ -129,7 +129,7 @@
    1.51  (*Nobody can have used non-existent keys!*)
    1.52  lemma new_keys_not_used [rule_format, simp]:
    1.53      "evs \<in> ns_shared \<Longrightarrow> Key K \<notin> used evs \<longrightarrow> K \<notin> keysFor (parts (spies evs))"
    1.54 -apply (erule ns_shared.induct, force, frule_tac [4] NS3_msg_in_parts_spies)
    1.55 +apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
    1.56  apply simp_all
    1.57  (*Fake, NS2, NS4, NS5*)
    1.58  apply (blast dest!: keysFor_parts_insert)+
    1.59 @@ -202,7 +202,7 @@
    1.60  lemma  "\<lbrakk>evs \<in> ns_shared;  Kab \<notin> range shrK\<rbrakk> \<Longrightarrow>
    1.61           (Crypt KAB X) \<in> parts (spies evs) \<and>
    1.62           Key K \<in> parts {X} \<longrightarrow> Key K \<in> parts (spies evs)"
    1.63 -apply (erule ns_shared.induct, force, frule_tac [4] NS3_msg_in_parts_spies)
    1.64 +apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
    1.65  apply simp_all
    1.66  (*Fake*)
    1.67  apply (blast dest: parts_insert_subset_Un)
    1.68 @@ -221,7 +221,7 @@
    1.69               (Key K \<in> analz (Key`KK \<union> (spies evs))) =
    1.70               (K \<in> KK \<or> Key K \<in> analz (spies evs))"
    1.71  apply (erule ns_shared.induct, force)
    1.72 -apply (frule_tac [7] Says_Server_message_form)
    1.73 +apply (drule_tac [7] Says_Server_message_form)
    1.74  apply (erule_tac [4] Says_S_message_form [THEN disjE])
    1.75  apply analz_freshK
    1.76  apply spy_analz
    1.77 @@ -264,13 +264,13 @@
    1.78  apply (frule_tac [4] Says_S_message_form)
    1.79  apply (erule_tac [5] disjE)
    1.80  apply (simp_all add: analz_insert_eq analz_insert_freshK pushes split_ifs)
    1.81 -apply spy_analz  (*Fake*) 
    1.82 +apply spy_analz  (*Fake*)
    1.83  apply blast      (*NS2*)
    1.84  (*NS3, Server sub-case*) (**LEVEL 8 **)
    1.85  apply (blast dest!: Crypt_Spy_analz_bad A_trusts_NS2
    1.86  	     dest:  Says_imp_knows_Spy analz.Inj unique_session_keys)
    1.87 -(*NS3, Spy sub-case; also Oops*) 
    1.88 -apply (blast dest: unique_session_keys)+ 
    1.89 +(*NS3, Spy sub-case; also Oops*)
    1.90 +apply (blast dest: unique_session_keys)+
    1.91  done
    1.92  
    1.93  
    1.94 @@ -309,13 +309,13 @@
    1.95  apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
    1.96  apply (analz_mono_contra, simp_all)
    1.97  apply blast     (*Fake*)
    1.98 -(*NS2: contradiction from the assumptions  
    1.99 +(*NS2: contradiction from the assumptions
   1.100    Key K \<notin> used evs2  and Crypt K (Nonce NB) \<in> parts (spies evs2) *)
   1.101 -apply (force dest!: Crypt_imp_keysFor) 
   1.102 +apply (force dest!: Crypt_imp_keysFor)
   1.103  apply blast     (*NS3*)
   1.104  (*NS4*)
   1.105  apply (blast dest!: B_trusts_NS3
   1.106 -	     dest: Says_imp_knows_Spy [THEN analz.Inj] 
   1.107 +	     dest: Says_imp_knows_Spy [THEN analz.Inj]
   1.108                     Crypt_Spy_analz_bad unique_session_keys)
   1.109  done
   1.110  
   1.111 @@ -326,14 +326,14 @@
   1.112         \<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
   1.113         A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
   1.114        \<Longrightarrow> Says B A (Crypt K (Nonce NB)) \<in> set evs"
   1.115 -by (blast intro: A_trusts_NS4_lemma 
   1.116 +by (blast intro: A_trusts_NS4_lemma
   1.117            dest: A_trusts_NS2 Spy_not_see_encrypted_key)
   1.118  
   1.119  (*If the session key has been used in NS4 then somebody has forwarded
   1.120 -  component X in some instance of NS4.  Perhaps an interesting property, 
   1.121 +  component X in some instance of NS4.  Perhaps an interesting property,
   1.122    but not needed (after all) for the proofs below.*)
   1.123  theorem NS4_implies_NS3 [rule_format]:
   1.124 -  "evs \<in> ns_shared \<Longrightarrow> 
   1.125 +  "evs \<in> ns_shared \<Longrightarrow>
   1.126       Key K \<notin> analz (spies evs) \<longrightarrow>
   1.127       Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs \<longrightarrow>
   1.128       Crypt K (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
   1.129 @@ -346,7 +346,7 @@
   1.130  apply blast  (*NS3*)
   1.131  (*NS4*)
   1.132  apply (blast dest!: B_trusts_NS3
   1.133 -	     dest: Says_imp_knows_Spy [THEN analz.Inj] 
   1.134 +	     dest: Says_imp_knows_Spy [THEN analz.Inj]
   1.135                     unique_session_keys Crypt_Spy_analz_bad)
   1.136  done
   1.137  
   1.138 @@ -361,13 +361,13 @@
   1.139       Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) \<in> set evs"
   1.140  apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
   1.141  apply analz_mono_contra
   1.142 -apply simp_all 
   1.143 +apply simp_all
   1.144  apply blast  (*Fake*)
   1.145  apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)  (*NS2*)
   1.146  apply (blast dest!: cert_A_form) (*NS3*)
   1.147  (*NS5*)
   1.148  apply (blast dest!: A_trusts_NS2
   1.149 -	     dest: Says_imp_knows_Spy [THEN analz.Inj] 
   1.150 +	     dest: Says_imp_knows_Spy [THEN analz.Inj]
   1.151                     unique_session_keys Crypt_Spy_analz_bad)
   1.152  done
   1.153  
   1.154 @@ -379,7 +379,7 @@
   1.155         \<forall>NA NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
   1.156         A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
   1.157        \<Longrightarrow> Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) \<in> set evs"
   1.158 -by (blast intro: B_trusts_NS5_lemma 
   1.159 +by (blast intro: B_trusts_NS5_lemma
   1.160            dest: B_trusts_NS3 Spy_not_see_encrypted_key)
   1.161  
   1.162  end