--- 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