src/HOL/Auth/NS_Shared.thy
changeset 11150 67387142225e
parent 11117 55358999077d
child 11188 5d539f1682c3
equal deleted inserted replaced
11149:e258b536a137 11150:67387142225e
    69   Oops: "\<lbrakk>evso \<in> ns_shared;  Says B A (Crypt K (Nonce NB)) \<in> set evso;
    69   Oops: "\<lbrakk>evso \<in> ns_shared;  Says B A (Crypt K (Nonce NB)) \<in> set evso;
    70 	  Says Server A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>)
    70 	  Says Server A (Crypt (shrK A) \<lbrace>Nonce NA, Agent B, Key K, X\<rbrace>)
    71 	      \<in> set evso\<rbrakk>
    71 	      \<in> set evso\<rbrakk>
    72 	 \<Longrightarrow> Notes Spy \<lbrace>Nonce NA, Nonce NB, Key K\<rbrace> # evso \<in> ns_shared"
    72 	 \<Longrightarrow> Notes Spy \<lbrace>Nonce NA, Nonce NB, Key K\<rbrace> # evso \<in> ns_shared"
    73 
    73 
    74 declare knows_Spy_partsEs [elim]
    74 
       
    75 declare Says_imp_knows_Spy [THEN parts.Inj, dest]
       
    76 declare parts.Body  [dest]
       
    77 declare MPair_parts [elim!]    (*can speed up some proofs*)
       
    78 
    75 declare analz_subset_parts [THEN subsetD, dest]
    79 declare analz_subset_parts [THEN subsetD, dest]
    76 declare Fake_parts_insert [THEN subsetD, dest]
    80 declare Fake_parts_insert  [THEN subsetD, dest]
    77 declare image_eq_UN [simp]  (*accelerates proofs involving nested images*)
    81 declare image_eq_UN [simp]  (*accelerates proofs involving nested images*)
    78 
    82 
    79 
    83 
    80 (*A "possibility property": there are traces that reach the end*)
    84 (*A "possibility property": there are traces that reach the end*)
    81 lemma "A \<noteq> Server \<Longrightarrow> \<exists>N K. \<exists>evs \<in> ns_shared.
    85 lemma "A \<noteq> Server \<Longrightarrow> \<exists>N K. \<exists>evs \<in> ns_shared.
   169 lemma Says_S_message_form:
   173 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;
   174      "\<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>
   175        evs \<in> ns_shared\<rbrakk>
   172       \<Longrightarrow> (K \<notin> range shrK \<and> X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>))
   176       \<Longrightarrow> (K \<notin> range shrK \<and> X = (Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>))
   173           \<or> X \<in> analz (spies evs)"
   177           \<or> X \<in> analz (spies evs)"
   174 apply (frule Says_imp_knows_Spy)
   178 by (blast dest: Says_imp_knows_Spy cert_A_form analz.Inj)
   175 (*mystery: why is this frule needed?*)
   179 
   176 apply (blast dest: cert_A_form analz.Inj)
       
   177 done
       
   178 
   180 
   179 (*Alternative version also provable
   181 (*Alternative version also provable
   180 lemma Says_S_message_form2:
   182 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;
   183   "\<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>
   184     evs \<in> ns_shared\<rbrakk>
   249 done
   251 done
   250 
   252 
   251 
   253 
   252 (** Crucial secrecy property: Spy does not see the keys sent in msg NS2 **)
   254 (** Crucial secrecy property: Spy does not see the keys sent in msg NS2 **)
   253 
   255 
   254 lemma secrecy_lemma [rule_format]:
   256 (*Beware of [rule_format] and the universal quantifier!*)
       
   257 lemma secrecy_lemma:
   255      "\<lbrakk>Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
   258      "\<lbrakk>Says Server A (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
   256                                       Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>)
   259                                       Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>)
   257               \<in> set evs;
   260               \<in> set evs;
   258          A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
   261          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>
   262       \<Longrightarrow> (\<forall>NB. Notes Spy \<lbrace>NA, NB, Key K\<rbrace> \<notin> set evs) \<longrightarrow>
   267 apply spy_analz  (*Fake*) 
   270 apply spy_analz  (*Fake*) 
   268 apply blast      (*NS2*)
   271 apply blast      (*NS2*)
   269 (*NS3, Server sub-case*) (**LEVEL 6 **)
   272 (*NS3, Server sub-case*) (**LEVEL 6 **)
   270 apply clarify
   273 apply clarify
   271 apply (frule Says_imp_knows_Spy [THEN parts.Inj, THEN A_trusts_NS2])
   274 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])
   275 apply (blast dest: Says_imp_knows_Spy analz.Inj Crypt_Spy_analz_bad)
   273 apply assumption
   276 apply assumption
   274 apply (blast dest: unique_session_keys)+ (*also proves Oops*)
   277 apply (blast dest: unique_session_keys)+ (*also proves Oops*)
   275 done
   278 done
   276 
   279 
   277 
   280 
   279 lemma Spy_not_see_encrypted_key:
   282 lemma Spy_not_see_encrypted_key:
   280      "\<lbrakk>Says Server A (Crypt K' \<lbrace>NA, Agent B, Key K, X\<rbrace>) \<in> set evs;
   283      "\<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;
   284        \<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>
   285        A \<notin> bad;  B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
   283       \<Longrightarrow> Key K \<notin> analz (spies evs)"
   286       \<Longrightarrow> Key K \<notin> analz (spies evs)"
   284 apply (frule Says_Server_message_form, assumption)
   287 by (blast dest: Says_Server_message_form secrecy_lemma)
   285 apply (auto dest: Says_Server_message_form secrecy_lemma)
       
   286 done
       
   287 
   288 
   288 
   289 
   289 (**** Guarantees available at various stages of protocol ***)
   290 (**** Guarantees available at various stages of protocol ***)
   290 
   291 
   291 (*If the encrypted message appears then it originated with the Server*)
   292 (*If the encrypted message appears then it originated with the Server*)
   292 lemma B_trusts_NS3:
   293 lemma B_trusts_NS3:
   293      "\<lbrakk>Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace> \<in> parts (spies evs);
   294      "\<lbrakk>Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace> \<in> parts (spies evs);
   294             B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
   295        B \<notin> bad;  evs \<in> ns_shared\<rbrakk>
   295           \<Longrightarrow> \<exists>NA. Says Server A
   296       \<Longrightarrow> \<exists>NA. Says Server A
   296                (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
   297                (Crypt (shrK A) \<lbrace>NA, Agent B, Key K,
   297                                  Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>)
   298                                  Crypt (shrK B) \<lbrace>Key K, Agent A\<rbrace>\<rbrace>)
   298               \<in> set evs"
   299               \<in> set evs"
   299 apply (erule rev_mp)
   300 apply (erule rev_mp)
   300 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
   301 apply (erule ns_shared.induct, force, drule_tac [4] NS3_msg_in_parts_spies)
   315 (*NS2: contradiction from the assumptions  
   316 (*NS2: contradiction from the assumptions  
   316   Key K \<notin> used evs2  and Crypt K (Nonce NB) \<in> parts (spies evs2) *)
   317   Key K \<notin> used evs2  and Crypt K (Nonce NB) \<in> parts (spies evs2) *)
   317 apply (force dest!: Crypt_imp_keysFor) 
   318 apply (force dest!: Crypt_imp_keysFor) 
   318 apply blast     (*NS3*)
   319 apply blast     (*NS3*)
   319 (*NS4*)
   320 (*NS4*)
   320 apply clarify;
   321 apply (blast dest!: B_trusts_NS3
   321 apply (frule Says_imp_knows_Spy [THEN analz.Inj])
   322 	     dest: Says_imp_knows_Spy [THEN analz.Inj] 
   322 apply (blast dest: Says_imp_knows_Spy [THEN analz.Inj] Crypt_Spy_analz_bad
   323                    Crypt_Spy_analz_bad unique_session_keys)
   323                    B_trusts_NS3 unique_session_keys)
       
   324 done
   324 done
   325 
   325 
   326 (*This version no longer assumes that K is secure*)
   326 (*This version no longer assumes that K is secure*)
   327 lemma A_trusts_NS4:
   327 lemma A_trusts_NS4:
   328      "\<lbrakk>Crypt K (Nonce NB) \<in> parts (spies evs);
   328      "\<lbrakk>Crypt K (Nonce NB) \<in> parts (spies evs);
   347 apply (simp_all add: ex_disj_distrib)
   347 apply (simp_all add: ex_disj_distrib)
   348 apply blast  (*Fake*)
   348 apply blast  (*Fake*)
   349 apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)  (*NS2*)
   349 apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)  (*NS2*)
   350 apply blast  (*NS3*)
   350 apply blast  (*NS3*)
   351 (*NS4*)
   351 (*NS4*)
   352 apply (case_tac "Ba \<in> bad")
   352 apply (blast dest!: B_trusts_NS3
   353 apply (blast dest: Says_imp_knows_Spy [THEN analz.Inj] Crypt_Spy_analz_bad);
   353 	     dest: Says_imp_knows_Spy [THEN analz.Inj] 
   354 apply (frule Says_imp_knows_Spy [THEN parts.Inj, THEN B_trusts_NS3], 
   354                    unique_session_keys Crypt_Spy_analz_bad)
   355        assumption+)
       
   356 apply (blast dest: unique_session_keys)
       
   357 done
   355 done
   358 
   356 
   359 
   357 
   360 lemma B_trusts_NS5_lemma [rule_format]:
   358 lemma B_trusts_NS5_lemma [rule_format]:
   361   "\<lbrakk>B \<notin> bad;  evs \<in> ns_shared\<rbrakk> \<Longrightarrow>
   359   "\<lbrakk>B \<notin> bad;  evs \<in> ns_shared\<rbrakk> \<Longrightarrow>
   369 apply analz_mono_contra
   367 apply analz_mono_contra
   370 apply simp_all 
   368 apply simp_all 
   371 apply blast  (*Fake*)
   369 apply blast  (*Fake*)
   372 apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)  (*NS2*)
   370 apply (blast dest!: new_keys_not_used Crypt_imp_keysFor)  (*NS2*)
   373 apply (blast dest!: cert_A_form) (*NS3*)
   371 apply (blast dest!: cert_A_form) (*NS3*)
   374 (**LEVEL 5**)
       
   375 (*NS5*)
   372 (*NS5*)
   376 apply clarify
   373 apply (blast dest!: A_trusts_NS2
   377 apply (case_tac "Aa \<in> bad")
   374 	     dest: Says_imp_knows_Spy [THEN analz.Inj] 
   378 apply (blast dest: Says_imp_knows_Spy [THEN analz.Inj] Crypt_Spy_analz_bad);
   375                    unique_session_keys Crypt_Spy_analz_bad)
   379 apply (blast dest: A_trusts_NS2 unique_session_keys)
       
   380 done
   376 done
   381 
   377 
   382 
   378 
   383 (*Very strong Oops condition reveals protocol's weakness*)
   379 (*Very strong Oops condition reveals protocol's weakness*)
   384 lemma B_trusts_NS5:
   380 lemma B_trusts_NS5:
   385      "\<lbrakk>Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace> \<in> parts (spies evs);
   381      "\<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);
   382        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;
   383        \<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>
   384        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"
   385       \<Longrightarrow> Says A B (Crypt K \<lbrace>Nonce NB, Nonce NB\<rbrace>) \<in> set evs"
   390 apply (drule B_trusts_NS3, clarify+)
   386 by (blast intro: B_trusts_NS5_lemma 
   391 apply (blast intro: B_trusts_NS5_lemma 
   387           dest: B_trusts_NS3 Spy_not_see_encrypted_key)
   392              dest: dest: Spy_not_see_encrypted_key)
       
   393 (*surprisingly delicate proof due to quantifier interactions*)
       
   394 done
       
   395 
   388 
   396 end
   389 end