src/HOL/Auth/NS_Shared.thy
changeset 11104 f2024fed9f0c
parent 5434 9b4bed3f394c
child 11117 55358999077d
equal deleted inserted replaced
11103:2a3cc8e1723a 11104:f2024fed9f0c
     8 From page 247 of
     8 From page 247 of
     9   Burrows, Abadi and Needham.  A Logic of Authentication.
     9   Burrows, Abadi and Needham.  A Logic of Authentication.
    10   Proc. Royal Soc. 426 (1989)
    10   Proc. Royal Soc. 426 (1989)
    11 *)
    11 *)
    12 
    12 
    13 NS_Shared = Shared + 
    13 theory NS_Shared = Shared:
    14 
    14 
    15 consts  ns_shared   :: event list set
    15 consts  ns_shared   :: "event list set"
    16 inductive "ns_shared"
    16 inductive "ns_shared"
    17   intrs 
    17  intros
    18          (*Initial trace is empty*)
    18 	(*Initial trace is empty*)
    19     Nil  "[]: ns_shared"
    19   Nil:  "[] \<in> ns_shared"
    20 
    20 	(*The spy MAY say anything he CAN say.  We do not expect him to
    21          (*The spy MAY say anything he CAN say.  We do not expect him to
    21 	  invent new nonces here, but he can also use NS1.  Common to
    22            invent new nonces here, but he can also use NS1.  Common to
    22 	  all similar protocols.*)
    23            all similar protocols.*)
    23   Fake: "\<lbrakk>evs \<in> ns_shared;  X \<in> synth (analz (spies evs))\<rbrakk>
    24     Fake "[| evs: ns_shared;  X: synth (analz (spies evs)) |]
    24 	 \<Longrightarrow> Says Spy B X # evs \<in> ns_shared"
    25           ==> Says Spy B X # evs : ns_shared"
    25 
    26 
    26 	(*Alice initiates a protocol run, requesting to talk to any B*)
    27          (*Alice initiates a protocol run, requesting to talk to any B*)
    27   NS1:  "\<lbrakk>evs1 \<in> ns_shared;  Nonce NA \<notin> used evs1\<rbrakk>
    28     NS1  "[| evs1: ns_shared;  Nonce NA ~: used evs1 |]
    28 	 \<Longrightarrow> Says A Server \<lbrace>Agent A, Agent B, Nonce NA\<rbrace> # evs1  \<in>  ns_shared"
    29           ==> Says A Server {|Agent A, Agent B, Nonce NA|} # evs1
    29 
    30                 :  ns_shared"
    30 	(*Server's response to Alice's message.
    31 
    31 	  !! It may respond more than once to A's request !!
    32          (*Server's response to Alice's message.
    32 	  Server doesn't know who the true sender is, hence the A' in
    33            !! It may respond more than once to A's request !!
    33 	      the sender field.*)
    34 	   Server doesn't know who the true sender is, hence the A' in
    34   NS2:  "\<lbrakk>evs2 \<in> ns_shared;  Key KAB \<notin> used evs2;
    35                the sender field.*)
    35 	  Says A' Server \<lbrace>Agent A, Agent B, Nonce NA\<rbrace> \<in> set evs2\<rbrakk>
    36     NS2  "[| evs2: ns_shared;  Key KAB ~: used evs2;
    36 	 \<Longrightarrow> Says Server A 
    37              Says A' Server {|Agent A, Agent B, Nonce NA|} : set evs2 |]
    37 	       (Crypt (shrK A)
    38           ==> Says Server A 
    38 		  \<lbrace>Nonce NA, Agent B, Key KAB,
    39                 (Crypt (shrK A)
    39 		    (Crypt (shrK B) \<lbrace>Key KAB, Agent A\<rbrace>)\<rbrace>) 
    40                    {|Nonce NA, Agent B, Key KAB,
    40 	       # evs2 \<in> ns_shared"
    41                      (Crypt (shrK B) {|Key KAB, Agent A|})|}) 
    41 
    42                 # evs2 : ns_shared"
    42 	 (*We can't assume S=Server.  Agent A "remembers" her nonce.
    43 
    43 	   Need A \<noteq> Server because we allow messages to self.*)
    44           (*We can't assume S=Server.  Agent A "remembers" her nonce.
    44   NS3:  "\<lbrakk>evs3 \<in> ns_shared;  A \<noteq> Server;
    45             Need A ~= Server because we allow messages to self.*)
    45 	  Says S A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs3;
    46     NS3  "[| evs3: ns_shared;  A ~= Server;
    46 	  Says A Server \<lbrace>Agent A, Agent B, Nonce NA\<rbrace> \<in> set evs3\<rbrakk>
    47              Says S A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|}) 
    47 	 \<Longrightarrow> Says A B X # evs3 \<in> ns_shared"
    48                : set evs3;
    48 
    49              Says A Server {|Agent A, Agent B, Nonce NA|} : set evs3 |]
    49 	(*Bob's nonce exchange.  He does not know who the message came
    50           ==> Says A B X # evs3 : ns_shared"
    50 	  from, but responds to A because she is mentioned inside.*)
    51 
    51   NS4:  "\<lbrakk>evs4 \<in> ns_shared;  Nonce NB \<notin> used evs4;
    52          (*Bob's nonce exchange.  He does not know who the message came
    52 	  Says A' B (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>) \<in> set evs4\<rbrakk>
    53            from, but responds to A because she is mentioned inside.*)
    53 	 \<Longrightarrow> Says B A (Crypt K (Nonce NB)) # evs4 \<in> ns_shared"
    54     NS4  "[| evs4: ns_shared;  Nonce NB ~: used evs4;
    54 
    55              Says A' B (Crypt (shrK B) {|Key K, Agent A|}) : set evs4 |]
    55 	(*Alice responds with Nonce NB if she has seen the key before.
    56           ==> Says B A (Crypt K (Nonce NB)) # evs4
    56 	  Maybe should somehow check Nonce NA again.
    57                 : ns_shared"
    57 	  We do NOT send NB-1 or similar as the Spy cannot spoof such things.
    58 
    58 	  Letting the Spy add or subtract 1 lets him send \<forall>nonces.
    59          (*Alice responds with Nonce NB if she has seen the key before.
    59 	  Instead we distinguish the messages by sending the nonce twice.*)
    60            Maybe should somehow check Nonce NA again.
    60   NS5:  "\<lbrakk>evs5 \<in> ns_shared;  
    61            We do NOT send NB-1 or similar as the Spy cannot spoof such things.
    61 	  Says B' A (Crypt K (Nonce NB)) \<in> set evs5;
    62            Letting the Spy add or subtract 1 lets him send ALL nonces.
    62 	  Says S  A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>)
    63            Instead we distinguish the messages by sending the nonce twice.*)
    63 	    \<in> set evs5\<rbrakk>
    64     NS5  "[| evs5: ns_shared;  
    64 	 \<Longrightarrow> Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) # evs5 \<in> ns_shared"
    65              Says B' A (Crypt K (Nonce NB)) : set evs5;
    65 
    66              Says S  A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
    66 	(*This message models possible leaks of session keys.
    67                : set evs5 |]
    67 	  The two Nonces identify the protocol run: the rule insists upon
    68           ==> Says A B (Crypt K {|Nonce NB, Nonce NB|}) # evs5 : ns_shared"
    68 	  the true senders in order to make them accurate.*)
    69   
    69   Oops: "\<lbrakk>evso \<in> ns_shared;  Says B A (Crypt K (Nonce NB)) \<in> set evso;
    70          (*This message models possible leaks of session keys.
    70 	  Says Server A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>)
    71            The two Nonces identify the protocol run: the rule insists upon
    71 	      \<in> set evso\<rbrakk>
    72            the true senders in order to make them accurate.*)
    72 	 \<Longrightarrow> Notes Spy \<lbrace>Nonce NA, Nonce NB, Key K\<rbrace> # evso \<in> ns_shared"
    73     Oops "[| evso: ns_shared;  Says B A (Crypt K (Nonce NB)) : set evso;
    73 
    74              Says Server A (Crypt (shrK A) {|Nonce NA, Agent B, Key K, X|})
    74 declare knows_Spy_partsEs [elim]
    75                : set evso |]
    75 declare analz_subset_parts [THEN subsetD, dest]
    76           ==> Notes Spy {|Nonce NA, Nonce NB, Key K|} # evso : ns_shared"
    76 declare Fake_parts_insert [THEN subsetD, dest]
       
    77 declare image_eq_UN [simp]  (*accelerates proofs involving nested images*)
       
    78 
       
    79 
       
    80 (*A "possibility property": there are traces that reach the end*)
       
    81 lemma "A \<noteq> Server \<Longrightarrow> \<exists>N K. \<exists>evs \<in> ns_shared.
       
    82                               Says A B (Crypt K \<lbrace>Nonce N, Nonce N\<rbrace>) \<in> set evs"
       
    83 apply (intro exI bexI)
       
    84 apply (rule_tac [2] ns_shared.Nil
       
    85        [THEN ns_shared.NS1, THEN ns_shared.NS2, THEN ns_shared.NS3,
       
    86 	THEN ns_shared.NS4, THEN ns_shared.NS5])
       
    87 apply possibility
       
    88 done
       
    89 
       
    90 (*This version is similar, while instantiating ?K and ?N to epsilon-terms
       
    91 lemma "A \<noteq> Server \<Longrightarrow> \<exists>evs \<in> ns_shared.
       
    92                 Says A B (Crypt ?K \<lbrace>Nonce ?N, Nonce ?N\<rbrace>) \<in> set evs"
       
    93 *)
       
    94 
       
    95 
       
    96 (**** Inductive proofs about ns_shared ****)
       
    97 
       
    98 (*Forwarding lemmas, to aid simplification*)
       
    99 
       
   100 (*For reasoning about the encrypted portion of message NS3*)
       
   101 lemma NS3_msg_in_parts_spies:
       
   102      "Says S A (Crypt KA \<lbrace>N, B, K, X\<rbrace>) \<in> set evs \<Longrightarrow> X \<in> parts (spies evs)"
       
   103 by blast
       
   104                               
       
   105 (*For reasoning about the Oops message*)
       
   106 lemma Oops_parts_spies:
       
   107      "Says Server A (Crypt (shrK A) \<lbrace>NA, B, K, X\<rbrace>) \<in> set evs
       
   108             \<Longrightarrow> K \<in> parts (spies evs)"
       
   109 by blast
       
   110 
       
   111 (** Theorems of the form X \<notin> parts (spies evs) imply that NOBODY
       
   112     sends messages containing X! **)
       
   113 
       
   114 (*Spy never sees another agent's shared key! (unless it's bad at start)*)
       
   115 lemma Spy_see_shrK [simp]:
       
   116      "evs \<in> ns_shared \<Longrightarrow> (Key (shrK A) \<in> parts (spies evs)) = (A \<in> bad)"
       
   117 apply (erule ns_shared.induct, force, frule_tac [4] NS3_msg_in_parts_spies)
       
   118 apply simp_all
       
   119 apply blast+;
       
   120 done
       
   121 
       
   122 
       
   123 lemma Spy_analz_shrK [simp]:
       
   124      "evs \<in> ns_shared \<Longrightarrow> (Key (shrK A) \<in> analz (spies evs)) = (A \<in> bad)"
       
   125 by auto
       
   126 
       
   127 
       
   128 (*Nobody can have used non-existent keys!*)
       
   129 lemma new_keys_not_used [rule_format, simp]:
       
   130     "evs \<in> ns_shared \<Longrightarrow> Key K \<notin> used evs \<longrightarrow> K \<notin> keysFor (parts (spies evs))"
       
   131 apply (erule ns_shared.induct, force, frule_tac [4] NS3_msg_in_parts_spies)
       
   132 apply simp_all
       
   133 (*Fake, NS2, NS4, NS5*)
       
   134 apply (blast dest!: keysFor_parts_insert)+
       
   135 done
       
   136 
       
   137 
       
   138 (** Lemmas concerning the form of items passed in messages **)
       
   139 
       
   140 (*Describes the form of K, X and K' when the Server sends this message.*)
       
   141 lemma Says_Server_message_form:
       
   142      "\<lbrakk>Says Server A (Crypt K' \<lbrace>N, Agent B, Key K, X\<rbrace>) \<in> set evs;
       
   143        evs \<in> ns_shared\<rbrakk>
       
   144       \<Longrightarrow> K \<notin> range shrK \<and>
       
   145           X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>) \<and>
       
   146           K' = shrK A"
       
   147 by (erule rev_mp, erule ns_shared.induct, auto)
       
   148 
       
   149 
       
   150 (*If the encrypted message appears then it originated with the Server*)
       
   151 lemma A_trusts_NS2:
       
   152      "\<lbrakk>Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
       
   153        A \<notin> bad;  evs \<in> ns_shared\<rbrakk>
       
   154       \<Longrightarrow> Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs"
       
   155 apply (erule rev_mp)
       
   156 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
       
   157 apply auto
       
   158 done
       
   159 
       
   160 lemma cert_A_form:
       
   161      "\<lbrakk>Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
       
   162        A \<notin> bad;  evs \<in> ns_shared\<rbrakk>
       
   163       \<Longrightarrow> K \<notin> range shrK \<and>  X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>)"
       
   164 by (blast dest!: A_trusts_NS2 Says_Server_message_form)
       
   165 
       
   166 (*EITHER describes the form of X when the following message is sent,
       
   167   OR     reduces it to the Fake case.
       
   168   Use Says_Server_message_form if applicable.*)
       
   169 lemma Says_S_message_form:
       
   170      "\<lbrakk>Says S A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
       
   171        evs \<in> ns_shared\<rbrakk>
       
   172       \<Longrightarrow> (K \<notin> range shrK \<and> X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>))
       
   173           \<or> X \<in> analz (spies evs)"
       
   174 apply (frule Says_imp_knows_Spy)
       
   175 (*mystery: why is this frule needed?*)
       
   176 apply (blast dest: cert_A_form  analz.Inj)
       
   177 done
       
   178 
       
   179 (*Alternative version also provable
       
   180 lemma Says_S_message_form2:
       
   181   "\<lbrakk>Says S A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
       
   182     evs \<in> ns_shared\<rbrakk>
       
   183    \<Longrightarrow> Says Server A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>) \<in> set evs
       
   184        \<or> X \<in> analz (spies evs)"
       
   185 apply (case_tac "A \<in> bad")
       
   186 apply (force dest!: Says_imp_knows_Spy [THEN analz.Inj]);
       
   187 by (blast dest!: A_trusts_NS2 Says_Server_message_form)
       
   188 *)
       
   189 
       
   190 
       
   191 (****
       
   192  SESSION KEY COMPROMISE THEOREM.  To prove theorems of the form
       
   193 
       
   194   Key K \<in> analz (insert (Key KAB) (spies evs)) \<Longrightarrow>
       
   195   Key K \<in> analz (spies evs)
       
   196 
       
   197  A more general formula must be proved inductively.
       
   198 ****)
       
   199 
       
   200 (*NOT useful in this form, but it says that session keys are not used
       
   201   to encrypt messages containing other keys, in the actual protocol.
       
   202   We require that agents should behave like this subsequently also.*)
       
   203 lemma  "\<lbrakk>evs \<in> ns_shared;  Kab \<notin> range shrK\<rbrakk> \<Longrightarrow>
       
   204          (Crypt KAB X) \<in> parts (spies evs) \<and>
       
   205          Key K \<in> parts {X} \<longrightarrow> Key K \<in> parts (spies evs)"
       
   206 apply (erule ns_shared.induct, force, frule_tac [4] NS3_msg_in_parts_spies)
       
   207 apply simp_all
       
   208 (*Fake*)
       
   209 apply (blast dest: parts_insert_subset_Un)
       
   210 (*Base, NS4 and NS5*)
       
   211 apply auto
       
   212 done
       
   213 
       
   214 
       
   215 (** Session keys are not used to encrypt other session keys **)
       
   216 
       
   217 (*The equality makes the induction hypothesis easier to apply*)
       
   218 
       
   219 lemma analz_image_freshK [rule_format]:
       
   220  "evs \<in> ns_shared \<Longrightarrow>
       
   221    \<forall>K KK. KK \<subseteq> - (range shrK) \<longrightarrow>
       
   222              (Key K \<in> analz (Key`KK \<union> (spies evs))) =
       
   223              (K \<in> KK \<or> Key K \<in> analz (spies evs))"
       
   224 apply (erule ns_shared.induct, force)
       
   225 apply (frule_tac [7] Says_Server_message_form)
       
   226 apply (erule_tac [4] Says_S_message_form [THEN disjE])
       
   227 apply (analz_freshK)
       
   228 apply (spy_analz)
       
   229 done
       
   230 
       
   231 
       
   232 lemma analz_insert_freshK:
       
   233      "\<lbrakk>evs \<in> ns_shared;  KAB \<notin> range shrK\<rbrakk> \<Longrightarrow>
       
   234        Key K \<in> analz (insert (Key KAB) (spies evs)) =
       
   235        (K = KAB \<or> Key K \<in> analz (spies evs))"
       
   236 by (simp only: analz_image_freshK analz_image_freshK_simps)
       
   237 
       
   238 
       
   239 (** The session key K uniquely identifies the message **)
       
   240 
       
   241 (*In messages of this form, the session key uniquely identifies the rest*)
       
   242 lemma unique_session_keys:
       
   243      "\<lbrakk>Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
       
   244        Says Server A' (Crypt (shrK A') \<lbrace>NA', Agent B', Key K, X'\<rbrace>) \<in> set evs;
       
   245        evs \<in> ns_shared\<rbrakk> \<Longrightarrow> A=A' \<and> NA=NA' \<and> B=B' \<and> X = X'"
       
   246 apply (erule rev_mp, erule rev_mp, erule ns_shared.induct)
       
   247 apply simp_all
       
   248 apply blast+
       
   249 done
       
   250 
       
   251 
       
   252 (** Crucial secrecy property: Spy does not see the keys sent in msg NS2 **)
       
   253 
       
   254 lemma secrecy_lemma [rule_format]:
       
   255      "\<lbrakk>Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
       
   256                                       Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>)
       
   257               \<in> set evs;
       
   258          A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
       
   259       \<Longrightarrow> (\<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs) \<longrightarrow>
       
   260          Key K \<notin> analz (spies evs)"
       
   261 apply (erule rev_mp)
       
   262 apply (erule ns_shared.induct, force)
       
   263 apply (frule_tac [7] Says_Server_message_form)
       
   264 apply (frule_tac [4] Says_S_message_form)
       
   265 apply (erule_tac [5] disjE)
       
   266 apply (simp_all add: analz_insert_eq analz_insert_freshK pushes split_ifs)
       
   267 apply spy_analz  (*Fake*) 
       
   268 apply blast      (*NS2*)
       
   269 (*NS3, Server sub-case*) (**LEVEL 6 **)
       
   270 apply clarify
       
   271 apply (frule Says_imp_knows_Spy [THEN parts.Inj, THEN A_trusts_NS2])
       
   272 apply (blast dest: Says_imp_knows_Spy [THEN analz.Inj, THEN Crypt_Spy_analz_bad])
       
   273 apply assumption
       
   274 apply (blast dest: unique_session_keys)+ (*also proves Oops*)
       
   275 done
       
   276 
       
   277 
       
   278 (*Final version: Server's message in the most abstract form*)
       
   279 lemma Spy_not_see_encrypted_key:
       
   280      "\<lbrakk>Says Server A (Crypt K' \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
       
   281        \<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
       
   282        A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
       
   283       \<Longrightarrow> Key K \<notin> analz (spies evs)"
       
   284 apply (frule Says_Server_message_form, assumption)
       
   285 apply (auto dest: Says_Server_message_form secrecy_lemma)
       
   286 done
       
   287 
       
   288 
       
   289 (**** Guarantees available at various stages of protocol ***)
       
   290 
       
   291 (*If the encrypted message appears then it originated with the Server*)
       
   292 lemma B_trusts_NS3:
       
   293      "\<lbrakk>Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace> \<in> parts (spies evs);
       
   294             B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
       
   295           \<Longrightarrow> \<exists>NA. Says Server A
       
   296                (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
       
   297                                  Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>)
       
   298               \<in> set evs"
       
   299 apply (erule rev_mp)
       
   300 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
       
   301 apply auto
       
   302 done
       
   303 
       
   304 
       
   305 lemma A_trusts_NS4_lemma [rule_format]:
       
   306    "evs \<in> ns_shared \<Longrightarrow>
       
   307       Key K \<notin> analz (spies evs) \<longrightarrow>
       
   308       Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs \<longrightarrow>
       
   309       Crypt K (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
       
   310       Says B A (Crypt K (Nonce NB)) \<in> set evs"
       
   311 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
       
   312 apply analz_mono_contra
       
   313 apply simp_all
       
   314 apply blast     (*Fake*)
       
   315 (*NS2: contradiction from the assumptions  
       
   316   Key K \<notin> used evs2  and Crypt K (Nonce NB) \<in> parts (spies evs2) *)
       
   317 apply (force dest!: Crypt_imp_keysFor) 
       
   318 apply blast     (*NS3*)
       
   319 (*NS4*)
       
   320 apply clarify;
       
   321 apply (frule Says_imp_knows_Spy [THEN analz.Inj])
       
   322 apply (blast dest: Says_imp_knows_Spy [THEN analz.Inj] Crypt_Spy_analz_bad
       
   323                    B_trusts_NS3 unique_session_keys)
       
   324 done
       
   325 
       
   326 (*This version no longer assumes that K is secure*)
       
   327 lemma A_trusts_NS4:
       
   328      "\<lbrakk>Crypt K (Nonce NB) \<in> parts (spies evs);
       
   329        Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace> \<in> parts (spies evs);
       
   330        \<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
       
   331        A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
       
   332       \<Longrightarrow> Says B A (Crypt K (Nonce NB)) \<in> set evs"
       
   333 by (blast intro: A_trusts_NS4_lemma 
       
   334           dest: A_trusts_NS2 Spy_not_see_encrypted_key)
       
   335 
       
   336 (*If the session key has been used in NS4 then somebody has forwarded
       
   337   component X in some instance of NS4.  Perhaps an interesting property, 
       
   338   but not needed (after all) for the proofs below.*)
       
   339 theorem NS4_implies_NS3 [rule_format]:
       
   340   "evs \<in> ns_shared \<Longrightarrow> 
       
   341      Key K \<notin> analz (spies evs) \<longrightarrow>
       
   342      Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs \<longrightarrow>
       
   343      Crypt K (Nonce NB) \<in> parts (spies evs) \<longrightarrow>
       
   344      (\<exists>A'. Says A' B X \<in> set evs)"
       
   345 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
       
   346 apply analz_mono_contra
       
   347 apply (simp_all add: ex_disj_distrib)
       
   348 apply blast  (*Fake*)
       
   349 apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)  (*NS2*)
       
   350 apply blast  (*NS3*)
       
   351 (*NS4*)
       
   352 apply (case_tac "Ba \<in> bad")
       
   353 apply (blast dest: Says_imp_knows_Spy [THEN analz.Inj] Crypt_Spy_analz_bad);
       
   354 apply (frule Says_imp_knows_Spy [THEN parts.Inj, THEN B_trusts_NS3], 
       
   355        assumption+)
       
   356 apply (blast dest: unique_session_keys)
       
   357 done
       
   358 
       
   359 
       
   360 lemma B_trusts_NS5_lemma [rule_format]:
       
   361   "\<lbrakk>B \<notin> bad;  evs \<in> ns_shared\<rbrakk> \<Longrightarrow>
       
   362      Key K \<notin> analz (spies evs) \<longrightarrow>
       
   363      Says Server A
       
   364 	  (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
       
   365 			    Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>) \<in> set evs \<longrightarrow>
       
   366      Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace> \<in> parts (spies evs) \<longrightarrow>
       
   367      Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) \<in> set evs"
       
   368 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
       
   369 apply analz_mono_contra
       
   370 apply simp_all 
       
   371 apply blast  (*Fake*)
       
   372 apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)  (*NS2*)
       
   373 apply (blast dest!: cert_A_form) (*NS3*)
       
   374 (**LEVEL 5**)
       
   375 (*NS5*)
       
   376 apply clarify
       
   377 apply (case_tac "Aa \<in> bad")
       
   378 apply (blast dest: Says_imp_knows_Spy [THEN analz.Inj] Crypt_Spy_analz_bad);
       
   379 apply (blast dest: A_trusts_NS2 unique_session_keys)
       
   380 done
       
   381 
       
   382 
       
   383 (*Very strong Oops condition reveals protocol's weakness*)
       
   384 lemma B_trusts_NS5:
       
   385      "\<lbrakk>Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace> \<in> parts (spies evs);
       
   386        Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace> \<in> parts (spies evs);
       
   387        \<forall>NA NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs;
       
   388        A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
       
   389       \<Longrightarrow> Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) \<in> set evs"
       
   390 apply (drule B_trusts_NS3, clarify+)
       
   391 apply (blast intro: B_trusts_NS5_lemma 
       
   392              dest: dest: Spy_not_see_encrypted_key)
       
   393 (*surprisingly delicate proof due to quantifier interactions*)
       
   394 done
    77 
   395 
    78 end
   396 end