diff -r 2a3cc8e1723a -r f2024fed9f0c src/HOL/Auth/NS_Shared.thy
--- a/src/HOL/Auth/NS_Shared.thy	Tue Feb 13 01:32:54 2001 +0100
+++ b/src/HOL/Auth/NS_Shared.thy	Tue Feb 13 13:16:27 2001 +0100
@@ -10,69 +10,387 @@
   Proc. Royal Soc. 426 (1989)
 *)
 
-NS_Shared = Shared + 
+theory NS_Shared = Shared:
 
-consts  ns_shared   :: event list set
+consts  ns_shared   :: "event list set"
 inductive "ns_shared"
-  intrs 
-         (*Initial trace is empty*)
-    Nil  "[]: ns_shared"
+ intros
+	(*Initial trace is empty*)
+  Nil:  "[] \<in> ns_shared"
+	(*The spy MAY say anything he CAN say.  We do not expect him to
+	  invent new nonces here, but he can also use NS1.  Common to
+	  all similar protocols.*)
+  Fake: "\<lbrakk>evs \<in> ns_shared;  X \<in> synth (analz (spies evs))\<rbrakk>
+	 \<Longrightarrow> Says Spy B X # evs \<in> ns_shared"
+
+	(*Alice initiates a protocol run, requesting to talk to any B*)
+  NS1:  "\<lbrakk>evs1 \<in> ns_shared;  Nonce NA \<notin> used evs1\<rbrakk>
+	 \<Longrightarrow> Says A Server \<lbrace>Agent A, Agent B, Nonce NA\<rbrace> # evs1  \<in>  ns_shared"
+
+	(*Server's response to Alice's message.
+	  !! It may respond more than once to A's request !!
+	  Server doesn't know who the true sender is, hence the A' in
+	      the sender field.*)
+  NS2:  "\<lbrakk>evs2 \<in> ns_shared;  Key KAB \<notin> used evs2;
+	  Says A' Server \<lbrace>Agent A, Agent B, Nonce NA\<rbrace> \<in> set evs2\<rbrakk>
+	 \<Longrightarrow> Says Server A 
+	       (Crypt (shrK A)
+		  \<lbrace>Nonce NA, Agent B, Key KAB,
+		    (Crypt (shrK B) \<lbrace>Key KAB, Agent A\<rbrace>)\<rbrace>) 
+	       # evs2 \<in> ns_shared"
+
+	 (*We can't assume S=Server.  Agent A "remembers" her nonce.
+	   Need A \<noteq> Server because we allow messages to self.*)
+  NS3:  "\<lbrakk>evs3 \<in> ns_shared;  A \<noteq> Server;
+	  Says S A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs3;
+	  Says A Server \<lbrace>Agent A, Agent B, Nonce NA\<rbrace> \<in> set evs3\<rbrakk>
+	 \<Longrightarrow> Says A B X # evs3 \<in> ns_shared"
+
+	(*Bob's nonce exchange.  He does not know who the message came
+	  from, but responds to A because she is mentioned inside.*)
+  NS4:  "\<lbrakk>evs4 \<in> ns_shared;  Nonce NB \<notin> used evs4;
+	  Says A' B (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>) \<in> set evs4\<rbrakk>
+	 \<Longrightarrow> Says B A (Crypt K (Nonce NB)) # evs4 \<in> ns_shared"
 
-         (*The spy MAY say anything he CAN say.  We do not expect him to
-           invent new nonces here, but he can also use NS1.  Common to
-           all similar protocols.*)
-    Fake "[| evs: ns_shared;  X: synth (analz (spies evs)) |]
-          ==> Says Spy B X # evs : ns_shared"
+	(*Alice responds with Nonce NB if she has seen the key before.
+	  Maybe should somehow check Nonce NA again.
+	  We do NOT send NB-1 or similar as the Spy cannot spoof such things.
+	  Letting the Spy add or subtract 1 lets him send \<forall>nonces.
+	  Instead we distinguish the messages by sending the nonce twice.*)
+  NS5:  "\<lbrakk>evs5 \<in> ns_shared;  
+	  Says B' A (Crypt K (Nonce NB)) \<in> set evs5;
+	  Says S  A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>)
+	    \<in> set evs5\<rbrakk>
+	 \<Longrightarrow> Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) # evs5 \<in> ns_shared"
+
+	(*This message models possible leaks of session keys.
+	  The two Nonces identify the protocol run: the rule insists upon
+	  the true senders in order to make them accurate.*)
+  Oops: "\<lbrakk>evso \<in> ns_shared;  Says B A (Crypt K (Nonce NB)) \<in> set evso;
+	  Says Server A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>)
+	      \<in> set evso\<rbrakk>
+	 \<Longrightarrow> Notes Spy \<lbrace>Nonce NA, Nonce NB, Key K\<rbrace> # evso \<in> ns_shared"
+
+declare knows_Spy_partsEs [elim]
+declare analz_subset_parts [THEN subsetD, dest]
+declare Fake_parts_insert [THEN subsetD, dest]
+declare image_eq_UN [simp]  (*accelerates proofs involving nested images*)
+
+
+(*A "possibility property": there are traces that reach the end*)
+lemma "A \<noteq> Server \<Longrightarrow> \<exists>N K. \<exists>evs \<in> ns_shared.
+                              Says A B (Crypt K \<lbrace>Nonce N, Nonce N\<rbrace>) \<in> set evs"
+apply (intro exI bexI)
+apply (rule_tac [2] ns_shared.Nil
+       [THEN ns_shared.NS1, THEN ns_shared.NS2, THEN ns_shared.NS3,
+	THEN ns_shared.NS4, THEN ns_shared.NS5])
+apply possibility
+done
+
+(*This version is similar, while instantiating ?K and ?N to epsilon-terms
+lemma "A \<noteq> Server \<Longrightarrow> \<exists>evs \<in> ns_shared.
+                Says A B (Crypt ?K \<lbrace>Nonce ?N, Nonce ?N\<rbrace>) \<in> set evs"
+*)
+
+
+(**** Inductive proofs about ns_shared ****)
+
+(*Forwarding lemmas, to aid simplification*)
 
-         (*Alice initiates a protocol run, requesting to talk to any B*)
-    NS1  "[| evs1: ns_shared;  Nonce NA ~: used evs1 |]
-          ==> Says A Server {|Agent A, Agent B, Nonce NA|} # evs1
-                :  ns_shared"
+(*For reasoning about the encrypted portion of message NS3*)
+lemma NS3_msg_in_parts_spies:
+     "Says S A (Crypt KA \<lbrace>N, B, K, X\<rbrace>) \<in> set evs \<Longrightarrow> X \<in> parts (spies evs)"
+by blast
+                              
+(*For reasoning about the Oops message*)
+lemma Oops_parts_spies:
+     "Says Server A (Crypt (shrK A) \<lbrace>NA, B, K, X\<rbrace>) \<in> set evs
+            \<Longrightarrow> K \<in> parts (spies evs)"
+by blast
+
+(** Theorems of the form X \<notin> parts (spies evs) imply that NOBODY
+    sends messages containing X! **)
+
+(*Spy never sees another agent's shared key! (unless it's bad at start)*)
+lemma Spy_see_shrK [simp]:
+     "evs \<in> ns_shared \<Longrightarrow> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
+apply (erule ns_shared.induct, force, frule_tac [4] NS3_msg_in_parts_spies)
+apply simp_all
+apply blast+;
+done
+
+
+lemma Spy_analz_shrK [simp]:
+     "evs \<in> ns_shared \<Longrightarrow> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)"
+by auto
+
+
+(*Nobody can have used non-existent keys!*)
+lemma new_keys_not_used [rule_format, simp]:
+    "evs \<in> ns_shared \<Longrightarrow> Key K \<notin> used evs \<longrightarrow> K \<notin> keysFor (parts (spies evs))"
+apply (erule ns_shared.induct, force, frule_tac [4] NS3_msg_in_parts_spies)
+apply simp_all
+(*Fake, NS2, NS4, NS5*)
+apply (blast dest!: keysFor_parts_insert)+
+done
+
+
+(** Lemmas concerning the form of items passed in messages **)
+
+(*Describes the form of K, X and K' when the Server sends this message.*)
+lemma Says_Server_message_form:
+     "\<lbrakk>Says Server A (Crypt K' \<lbrace>N, Agent B, Key K, X\<rbrace>) \<in> set evs;
+       evs \<in> ns_shared\<rbrakk>
+      \<Longrightarrow> K \<notin> range shrK \<and>
+          X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>) \<and>
+          K' = shrK A"
+by (erule rev_mp, erule ns_shared.induct, auto)
+
 
-         (*Server's response to Alice's message.
-           !! It may respond more than once to A's request !!
-	   Server doesn't know who the true sender is, hence the A' in
-               the sender field.*)
-    NS2  "[| evs2: ns_shared;  Key KAB ~: used evs2;
-             Says A' Server {|Agent A, Agent B, Nonce NA|} : set evs2 |]
-          ==> Says Server A 
-                (Crypt (shrK A)
-                   {|Nonce NA, Agent B, Key KAB,
-                     (Crypt (shrK B) {|Key KAB, Agent A|})|}) 
-                # evs2 : ns_shared"
+(*If the encrypted message appears then it originated with the Server*)
+lemma A_trusts_NS2:
+     "\<lbrakk>Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
+       A \<notin> bad;  evs \<in> ns_shared\<rbrakk>
+      \<Longrightarrow> Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs"
+apply (erule rev_mp)
+apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
+apply auto
+done
+
+lemma cert_A_form:
+     "\<lbrakk>Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
+       A \<notin> bad;  evs \<in> ns_shared\<rbrakk>
+      \<Longrightarrow> K \<notin> range shrK \<and>  X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>)"
+by (blast dest!: A_trusts_NS2 Says_Server_message_form)
+
+(*EITHER describes the form of X when the following message is sent,
+  OR     reduces it to the Fake case.
+  Use Says_Server_message_form if applicable.*)
+lemma Says_S_message_form:
+     "\<lbrakk>Says S A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
+       evs \<in> ns_shared\<rbrakk>
+      \<Longrightarrow> (K \<notin> range shrK \<and> X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>))
+          \<or> X \<in> analz (spies evs)"
+apply (frule Says_imp_knows_Spy)
+(*mystery: why is this frule needed?*)
+apply (blast dest: cert_A_form  analz.Inj)
+done
+
+(*Alternative version also provable
+lemma Says_S_message_form2:
+  "\<lbrakk>Says S A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
+    evs \<in> ns_shared\<rbrakk>
+   \<Longrightarrow> Says Server A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs
+       \<or> X \<in> analz (spies evs)"
+apply (case_tac "A \<in> bad")
+apply (force dest!: Says_imp_knows_Spy [THEN analz.Inj]);
+by (blast dest!: A_trusts_NS2 Says_Server_message_form)
+*)
+
+
+(****
+ SESSION KEY COMPROMISE THEOREM.  To prove theorems of the form
+
+  Key K \<in> analz (insert (Key KAB) (spies evs)) \<Longrightarrow>
+  Key K \<in> analz (spies evs)
+
+ A more general formula must be proved inductively.
+****)
 
-          (*We can't assume S=Server.  Agent A "remembers" her nonce.
-            Need A ~= Server because we allow messages to self.*)
-    NS3  "[| evs3: ns_shared;  A ~= Server;
-             Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|}) 
-               : set evs3;
-             Says A Server {|Agent A, Agent B, Nonce NA|} : set evs3 |]
-          ==> Says A B X # evs3 : ns_shared"
+(*NOT useful in this form, but it says that session keys are not used
+  to encrypt messages containing other keys, in the actual protocol.
+  We require that agents should behave like this subsequently also.*)
+lemma  "\<lbrakk>evs \<in> ns_shared;  Kab \<notin> range shrK\<rbrakk> \<Longrightarrow>
+         (Crypt KAB X) \<in> parts (spies evs) \<and>
+         Key K \<in> parts {X} \<longrightarrow> Key K \<in> parts (spies evs)"
+apply (erule ns_shared.induct, force, frule_tac [4] NS3_msg_in_parts_spies)
+apply simp_all
+(*Fake*)
+apply (blast dest: parts_insert_subset_Un)
+(*Base, NS4 and NS5*)
+apply auto
+done
+
+
+(** Session keys are not used to encrypt other session keys **)
+
+(*The equality makes the induction hypothesis easier to apply*)
+
+lemma analz_image_freshK [rule_format]:
+ "evs \<in> ns_shared \<Longrightarrow>
+   \<forall>K KK. KK \<subseteq> - (range shrK) \<longrightarrow>
+             (Key K \<in> analz (Key`KK \<union> (spies evs))) =
+             (K \<in> KK \<or> Key K \<in> analz (spies evs))"
+apply (erule ns_shared.induct, force)
+apply (frule_tac [7] Says_Server_message_form)
+apply (erule_tac [4] Says_S_message_form [THEN disjE])
+apply (analz_freshK)
+apply (spy_analz)
+done
+
+
+lemma analz_insert_freshK:
+     "\<lbrakk>evs \<in> ns_shared;  KAB \<notin> range shrK\<rbrakk> \<Longrightarrow>
+       Key K \<in> analz (insert (Key KAB) (spies evs)) =
+       (K = KAB \<or> Key K \<in> analz (spies evs))"
+by (simp only: analz_image_freshK analz_image_freshK_simps)
+
+
+(** The session key K uniquely identifies the message **)
 
-         (*Bob's nonce exchange.  He does not know who the message came
-           from, but responds to A because she is mentioned inside.*)
-    NS4  "[| evs4: ns_shared;  Nonce NB ~: used evs4;
-             Says A' B (Crypt (shrK B) {|Key K, Agent A|}) : set evs4 |]
-          ==> Says B A (Crypt K (Nonce NB)) # evs4
-                : ns_shared"
+(*In messages of this form, the session key uniquely identifies the rest*)
+lemma unique_session_keys:
+     "\<lbrakk>Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
+       Says Server A' (Crypt (shrK A') \<lbrace>NA', Agent B', Key K, X'\<rbrace>) \<in> set evs;
+       evs \<in> ns_shared\<rbrakk> \<Longrightarrow> A=A' \<and> NA=NA' \<and> B=B' \<and> X = X'"
+apply (erule rev_mp, erule rev_mp, erule ns_shared.induct)
+apply simp_all
+apply blast+
+done
+
+
+(** Crucial secrecy property: Spy does not see the keys sent in msg NS2 **)
+
+lemma secrecy_lemma [rule_format]:
+     "\<lbrakk>Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
+                                      Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>)
+              \<in> set evs;
+         A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
+      \<Longrightarrow> (\<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs) \<longrightarrow>
+         Key K \<notin> analz (spies evs)"
+apply (erule rev_mp)
+apply (erule ns_shared.induct, force)
+apply (frule_tac [7] Says_Server_message_form)
+apply (frule_tac [4] Says_S_message_form)
+apply (erule_tac [5] disjE)
+apply (simp_all add: analz_insert_eq analz_insert_freshK pushes split_ifs)
+apply spy_analz  (*Fake*) 
+apply blast      (*NS2*)
+(*NS3, Server sub-case*) (**LEVEL 6 **)
+apply clarify
+apply (frule Says_imp_knows_Spy [THEN parts.Inj, THEN A_trusts_NS2])
+apply (blast dest: Says_imp_knows_Spy [THEN analz.Inj, THEN Crypt_Spy_analz_bad])
+apply assumption
+apply (blast dest: unique_session_keys)+ (*also proves Oops*)
+done
+
+
+(*Final version: Server's message in the most abstract form*)
+lemma Spy_not_see_encrypted_key:
+     "\<lbrakk>Says Server A (Crypt K' \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
+       \<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
+       A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
+      \<Longrightarrow> Key K \<notin> analz (spies evs)"
+apply (frule Says_Server_message_form, assumption)
+apply (auto dest: Says_Server_message_form secrecy_lemma)
+done
+
+
+(**** Guarantees available at various stages of protocol ***)
 
-         (*Alice responds with Nonce NB if she has seen the key before.
-           Maybe should somehow check Nonce NA again.
-           We do NOT send NB-1 or similar as the Spy cannot spoof such things.
-           Letting the Spy add or subtract 1 lets him send ALL nonces.
-           Instead we distinguish the messages by sending the nonce twice.*)
-    NS5  "[| evs5: ns_shared;  
-             Says B' A (Crypt K (Nonce NB)) : set evs5;
-             Says S  A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
-               : set evs5 |]
-          ==> Says A B (Crypt K {|Nonce NB, Nonce NB|}) # evs5 : ns_shared"
-  
-         (*This message models possible leaks of session keys.
-           The two Nonces identify the protocol run: the rule insists upon
-           the true senders in order to make them accurate.*)
-    Oops "[| evso: ns_shared;  Says B A (Crypt K (Nonce NB)) : set evso;
-             Says Server A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
-               : set evso |]
-          ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso : ns_shared"
+(*If the encrypted message appears then it originated with the Server*)
+lemma B_trusts_NS3:
+     "\<lbrakk>Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace> \<in> parts (spies evs);
+            B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
+          \<Longrightarrow> \<exists>NA. Says Server A
+               (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
+                                 Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>)
+              \<in> set evs"
+apply (erule rev_mp)
+apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
+apply auto
+done
+
+
+lemma A_trusts_NS4_lemma [rule_format]:
+   "evs \<in> ns_shared \<Longrightarrow>
+      Key K \<notin> analz (spies evs) \<longrightarrow>
+      Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs \<longrightarrow>
+      Crypt K (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
+      Says B A (Crypt K (Nonce NB)) \<in> set evs"
+apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
+apply analz_mono_contra
+apply simp_all
+apply blast     (*Fake*)
+(*NS2: contradiction from the assumptions  
+  Key K \<notin> used evs2  and Crypt K (Nonce NB) \<in> parts (spies evs2) *)
+apply (force dest!: Crypt_imp_keysFor) 
+apply blast     (*NS3*)
+(*NS4*)
+apply clarify;
+apply (frule Says_imp_knows_Spy [THEN analz.Inj])
+apply (blast dest: Says_imp_knows_Spy [THEN analz.Inj] Crypt_Spy_analz_bad
+                   B_trusts_NS3 unique_session_keys)
+done
+
+(*This version no longer assumes that K is secure*)
+lemma A_trusts_NS4:
+     "\<lbrakk>Crypt K (Nonce NB) \<in> parts (spies evs);
+       Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
+       \<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
+       A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
+      \<Longrightarrow> Says B A (Crypt K (Nonce NB)) \<in> set evs"
+by (blast intro: A_trusts_NS4_lemma 
+          dest: A_trusts_NS2 Spy_not_see_encrypted_key)
+
+(*If the session key has been used in NS4 then somebody has forwarded
+  component X in some instance of NS4.  Perhaps an interesting property, 
+  but not needed (after all) for the proofs below.*)
+theorem NS4_implies_NS3 [rule_format]:
+  "evs \<in> ns_shared \<Longrightarrow> 
+     Key K \<notin> analz (spies evs) \<longrightarrow>
+     Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs \<longrightarrow>
+     Crypt K (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
+     (\<exists>A'. Says A' B X \<in> set evs)"
+apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
+apply analz_mono_contra
+apply (simp_all add: ex_disj_distrib)
+apply blast  (*Fake*)
+apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)  (*NS2*)
+apply blast  (*NS3*)
+(*NS4*)
+apply (case_tac "Ba \<in> bad")
+apply (blast dest: Says_imp_knows_Spy [THEN analz.Inj] Crypt_Spy_analz_bad);
+apply (frule Says_imp_knows_Spy [THEN parts.Inj, THEN B_trusts_NS3], 
+       assumption+)
+apply (blast dest: unique_session_keys)
+done
+
+
+lemma B_trusts_NS5_lemma [rule_format]:
+  "\<lbrakk>B \<notin> bad;  evs \<in> ns_shared\<rbrakk> \<Longrightarrow>
+     Key K \<notin> analz (spies evs) \<longrightarrow>
+     Says Server A
+	  (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
+			    Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>) \<in> set evs \<longrightarrow>
+     Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace> \<in> parts (spies evs) \<longrightarrow>
+     Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) \<in> set evs"
+apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
+apply analz_mono_contra
+apply simp_all 
+apply blast  (*Fake*)
+apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)  (*NS2*)
+apply (blast dest!: cert_A_form) (*NS3*)
+(**LEVEL 5**)
+(*NS5*)
+apply clarify
+apply (case_tac "Aa \<in> bad")
+apply (blast dest: Says_imp_knows_Spy [THEN analz.Inj] Crypt_Spy_analz_bad);
+apply (blast dest: A_trusts_NS2 unique_session_keys)
+done
+
+
+(*Very strong Oops condition reveals protocol's weakness*)
+lemma B_trusts_NS5:
+     "\<lbrakk>Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace> \<in> parts (spies evs);
+       Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace> \<in> parts (spies evs);
+       \<forall>NA NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
+       A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
+      \<Longrightarrow> Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) \<in> set evs"
+apply (drule B_trusts_NS3, clarify+)
+apply (blast intro: B_trusts_NS5_lemma 
+             dest: dest: Spy_not_see_encrypted_key)
+(*surprisingly delicate proof due to quantifier interactions*)
+done
 
 end