src/HOL/Auth/NS_Shared.thy
changeset 14207 f20fbb141673
parent 14200 d8598e24f8fa
child 16417 9bc16273c2d4
     1.1 --- a/src/HOL/Auth/NS_Shared.thy	Fri Sep 26 10:32:26 2003 +0200
     1.2 +++ b/src/HOL/Auth/NS_Shared.thy	Fri Sep 26 10:34:28 2003 +0200
     1.3 @@ -2,15 +2,17 @@
     1.4      ID:         $Id$
     1.5      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.6      Copyright   1996  University of Cambridge
     1.7 -
     1.8 -Inductive relation "ns_shared" for Needham-Schroeder Shared-Key protocol.
     1.9 -
    1.10 -From page 247 of
    1.11 -  Burrows, Abadi and Needham.  A Logic of Authentication.
    1.12 -  Proc. Royal Soc. 426 (1989)
    1.13  *)
    1.14  
    1.15 -theory NS_Shared = Shared:
    1.16 +header{*The Needham-Schroeder Shared-Key Protocol*}
    1.17 +
    1.18 +theory NS_Shared = Public:
    1.19 +
    1.20 +text{*
    1.21 +From page 247 of
    1.22 +  Burrows, Abadi and Needham (1989).  A Logic of Authentication.
    1.23 +  Proc. Royal Soc. 426
    1.24 +*}
    1.25  
    1.26  consts  ns_shared   :: "event list set"
    1.27  inductive "ns_shared"
    1.28 @@ -31,7 +33,7 @@
    1.29  	  !! It may respond more than once to A's request !!
    1.30  	  Server doesn't know who the true sender is, hence the A' in
    1.31  	      the sender field.*)
    1.32 -  NS2:  "\<lbrakk>evs2 \<in> ns_shared;  Key KAB \<notin> used evs2;
    1.33 +  NS2:  "\<lbrakk>evs2 \<in> ns_shared;  Key KAB \<notin> used evs2;  KAB \<in> symKeys;
    1.34  	  Says A' Server \<lbrace>Agent A, Agent B, Nonce NA\<rbrace> \<in> set evs2\<rbrakk>
    1.35  	 \<Longrightarrow> Says Server A
    1.36  	       (Crypt (shrK A)
    1.37 @@ -48,7 +50,7 @@
    1.38  
    1.39  	(*Bob's nonce exchange.  He does not know who the message came
    1.40  	  from, but responds to A because she is mentioned inside.*)
    1.41 -  NS4:  "\<lbrakk>evs4 \<in> ns_shared;  Nonce NB \<notin> used evs4;
    1.42 +  NS4:  "\<lbrakk>evs4 \<in> ns_shared;  Nonce NB \<notin> used evs4;  K \<in> symKeys;
    1.43  	  Says A' B (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>) \<in> set evs4\<rbrakk>
    1.44  	 \<Longrightarrow> Says B A (Crypt K (Nonce NB)) # evs4 \<in> ns_shared"
    1.45  
    1.46 @@ -57,7 +59,7 @@
    1.47  	  We do NOT send NB-1 or similar as the Spy cannot spoof such things.
    1.48  	  Letting the Spy add or subtract 1 lets him send all nonces.
    1.49  	  Instead we distinguish the messages by sending the nonce twice.*)
    1.50 -  NS5:  "\<lbrakk>evs5 \<in> ns_shared;
    1.51 +  NS5:  "\<lbrakk>evs5 \<in> ns_shared;  K \<in> symKeys;
    1.52  	  Says B' A (Crypt K (Nonce NB)) \<in> set evs5;
    1.53  	  Says S  A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>)
    1.54  	    \<in> set evs5\<rbrakk>
    1.55 @@ -80,14 +82,14 @@
    1.56  
    1.57  
    1.58  text{*A "possibility property": there are traces that reach the end*}
    1.59 -lemma "[| A \<noteq> Server; Key K \<notin> used [] |] 
    1.60 +lemma "[| A \<noteq> Server; Key K \<notin> used []; K \<in> symKeys |]
    1.61         ==> \<exists>N. \<exists>evs \<in> ns_shared.
    1.62                      Says A B (Crypt K \<lbrace>Nonce N, Nonce N\<rbrace>) \<in> set evs"
    1.63  apply (intro exI bexI)
    1.64  apply (rule_tac [2] ns_shared.Nil
    1.65         [THEN ns_shared.NS1, THEN ns_shared.NS2, THEN ns_shared.NS3,
    1.66  	THEN ns_shared.NS4, THEN ns_shared.NS5])
    1.67 -apply (possibility, simp add: used_Cons) 
    1.68 +apply (possibility, simp add: used_Cons)
    1.69  done
    1.70  
    1.71  (*This version is similar, while instantiating ?K and ?N to epsilon-terms
    1.72 @@ -126,8 +128,10 @@
    1.73  
    1.74  
    1.75  text{*Nobody can have used non-existent keys!*}
    1.76 -lemma new_keys_not_used [rule_format, simp]:
    1.77 -    "evs \<in> ns_shared \<Longrightarrow> Key K \<notin> used evs \<longrightarrow> K \<notin> keysFor (parts (spies evs))"
    1.78 +lemma new_keys_not_used [simp]:
    1.79 +    "[|Key K \<notin> used evs; K \<in> symKeys; evs \<in> ns_shared|]
    1.80 +     ==> K \<notin> keysFor (parts (spies evs))"
    1.81 +apply (erule rev_mp)
    1.82  apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, simp_all)
    1.83  txt{*Fake, NS2, NS4, NS5*}
    1.84  apply (force dest!: keysFor_parts_insert, blast+)
    1.85 @@ -161,15 +165,15 @@
    1.86        \<Longrightarrow> K \<notin> range shrK \<and>  X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>)"
    1.87  by (blast dest!: A_trusts_NS2 Says_Server_message_form)
    1.88  
    1.89 -(*EITHER describes the form of X when the following message is sent,
    1.90 +text{*EITHER describes the form of X when the following message is sent,
    1.91    OR     reduces it to the Fake case.
    1.92 -  Use Says_Server_message_form if applicable.*)
    1.93 +  Use @{text Says_Server_message_form} if applicable.*}
    1.94  lemma Says_S_message_form:
    1.95       "\<lbrakk>Says S A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
    1.96         evs \<in> ns_shared\<rbrakk>
    1.97        \<Longrightarrow> (K \<notin> range shrK \<and> X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>))
    1.98            \<or> X \<in> analz (spies evs)"
    1.99 -by (blast dest: Says_imp_knows_Spy cert_A_form analz.Inj)
   1.100 +by (blast dest: Says_imp_knows_Spy analz_shrK_Decrypt cert_A_form analz.Inj)
   1.101  
   1.102  
   1.103  (*Alternative version also provable
   1.104 @@ -216,9 +220,11 @@
   1.105     \<forall>K KK. KK \<subseteq> - (range shrK) \<longrightarrow>
   1.106               (Key K \<in> analz (Key`KK \<union> (spies evs))) =
   1.107               (K \<in> KK \<or> Key K \<in> analz (spies evs))"
   1.108 -apply (erule ns_shared.induct, force)
   1.109 -apply (drule_tac [7] Says_Server_message_form)
   1.110 -apply (erule_tac [4] Says_S_message_form [THEN disjE], analz_freshK, spy_analz)
   1.111 +apply (erule ns_shared.induct)
   1.112 +apply (drule_tac [8] Says_Server_message_form)
   1.113 +apply (erule_tac [5] Says_S_message_form [THEN disjE], analz_freshK, spy_analz)
   1.114 +txt{*NS2, NS3*}
   1.115 +apply blast+; 
   1.116  done
   1.117  
   1.118  
   1.119 @@ -255,10 +261,10 @@
   1.120  apply (frule_tac [7] Says_Server_message_form)
   1.121  apply (frule_tac [4] Says_S_message_form)
   1.122  apply (erule_tac [5] disjE)
   1.123 -apply (simp_all add: analz_insert_eq analz_insert_freshK pushes split_ifs, spy_analz)  
   1.124 +apply (simp_all add: analz_insert_eq analz_insert_freshK pushes split_ifs, spy_analz)
   1.125  txt{*NS2*}
   1.126  apply blast
   1.127 -txt{*NS3, Server sub-case*} 
   1.128 +txt{*NS3, Server sub-case*}
   1.129  apply (blast dest!: Crypt_Spy_analz_bad A_trusts_NS2
   1.130  	     dest:  Says_imp_knows_Spy analz.Inj unique_session_keys)
   1.131  txt{*NS3, Spy sub-case; also Oops*}
   1.132 @@ -298,13 +304,13 @@
   1.133        Crypt K (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
   1.134        Says B A (Crypt K (Nonce NB)) \<in> set evs"
   1.135  apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
   1.136 -apply (analz_mono_contra, simp_all, blast) 
   1.137 -(*NS2: contradiction from the assumptions
   1.138 -  Key K \<notin> used evs2  and Crypt K (Nonce NB) \<in> parts (spies evs2) *)
   1.139 -apply (force dest!: Crypt_imp_keysFor)     
   1.140 +apply (analz_mono_contra, simp_all, blast)
   1.141 +txt{*NS2: contradiction from the assumptions @{term "Key K \<notin> used evs2"} and
   1.142 +    @{term "Crypt K (Nonce NB) \<in> parts (spies evs2)"} *} 
   1.143 +apply (force dest!: Crypt_imp_keysFor)
   1.144  txt{*NS3*}
   1.145 -apply blast 
   1.146 -txt{*NS4*} 
   1.147 +apply blast
   1.148 +txt{*NS4*}
   1.149  apply (blast dest: B_trusts_NS3
   1.150  	           Says_imp_knows_Spy [THEN analz.Inj]
   1.151                     Crypt_Spy_analz_bad unique_session_keys)
   1.152 @@ -320,9 +326,9 @@
   1.153  by (blast intro: A_trusts_NS4_lemma
   1.154            dest: A_trusts_NS2 Spy_not_see_encrypted_key)
   1.155  
   1.156 -(*If the session key has been used in NS4 then somebody has forwarded
   1.157 +text{*If the session key has been used in NS4 then somebody has forwarded
   1.158    component X in some instance of NS4.  Perhaps an interesting property,
   1.159 -  but not needed (after all) for the proofs below.*)
   1.160 +  but not needed (after all) for the proofs below.*}
   1.161  theorem NS4_implies_NS3 [rule_format]:
   1.162    "evs \<in> ns_shared \<Longrightarrow>
   1.163       Key K \<notin> analz (spies evs) \<longrightarrow>
   1.164 @@ -332,7 +338,7 @@
   1.165  apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, analz_mono_contra)
   1.166  apply (simp_all add: ex_disj_distrib, blast)
   1.167  txt{*NS2*}
   1.168 -apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)  
   1.169 +apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)
   1.170  txt{*NS3*}
   1.171  apply blast
   1.172  txt{*NS4*}
   1.173 @@ -352,9 +358,9 @@
   1.174       Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) \<in> set evs"
   1.175  apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies, analz_mono_contra, simp_all, blast)
   1.176  txt{*NS2*}
   1.177 -apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)  
   1.178 +apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)
   1.179  txt{*NS3*}
   1.180 -apply (blast dest!: cert_A_form) 
   1.181 +apply (blast dest!: cert_A_form)
   1.182  txt{*NS5*}
   1.183  apply (blast dest!: A_trusts_NS2
   1.184  	     dest: Says_imp_knows_Spy [THEN analz.Inj]