src/HOL/Auth/ZhouGollmann.thy
changeset 15047 fa62de5862b9
parent 14741 36582c356db7
child 15068 58d216b32199
     1.1 --- a/src/HOL/Auth/ZhouGollmann.thy	Thu Jul 15 13:24:45 2004 +0200
     1.2 +++ b/src/HOL/Auth/ZhouGollmann.thy	Thu Jul 15 15:32:32 2004 +0200
     1.3 @@ -198,15 +198,17 @@
     1.4  
     1.5  text{*Holds also for @{term "A = Spy"}!*}
     1.6  theorem NRO_authenticity:
     1.7 -     "[|Says A' B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs;
     1.8 +     "[|Gets B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs;
     1.9          NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
    1.10          A \<notin> broken;  evs \<in> zg |]
    1.11       ==> Says A B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs"
    1.12 +apply (drule Gets_imp_Says, assumption) 
    1.13  apply clarify 
    1.14  apply (frule NRO_sender, auto)
    1.15 -txt{*We are left with the case where @{term "A' = Spy"} and  @{term "A' \<noteq> A"},
    1.16 -  i.e. @{term "A \<notin> bad"}, when we can apply @{text NRO_authenticity_good}.*}
    1.17 - apply (blast dest: NRO_authenticity_good [OF refl])
    1.18 +txt{*We are left with the case where the sender is @{term Spy} and not
    1.19 +  equal to @{term A}, because @{term "A \<notin> bad"}. 
    1.20 +  Thus theorem @{text NRO_authenticity_good} applies.*}
    1.21 +apply (blast dest: NRO_authenticity_good [OF refl])
    1.22  done
    1.23  
    1.24  
    1.25 @@ -276,15 +278,17 @@
    1.26  
    1.27  text{*Holds also for @{term "A = Spy"}!*}
    1.28  theorem sub_K_authenticity:
    1.29 -     "[|Says A' TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs;
    1.30 +     "[|Gets TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs;
    1.31          sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
    1.32          A \<notin> broken;  evs \<in> zg |]
    1.33       ==> Says A TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs"
    1.34 +apply (drule Gets_imp_Says, assumption) 
    1.35  apply clarify 
    1.36  apply (frule sub_K_sender, auto)
    1.37 -txt{*We are left with the case where @{term "A' = Spy"} and  @{term "A' \<noteq> A"},
    1.38 -  i.e. @{term "A \<notin> bad"}, when we can apply @{text sub_K_authenticity_good}.*}
    1.39 - apply (blast dest: sub_K_authenticity_good [OF refl])
    1.40 +txt{*We are left with the case where the sender is @{term Spy} and not
    1.41 +  equal to @{term A}, because @{term "A \<notin> bad"}. 
    1.42 +  Thus theorem @{text sub_K_authenticity_good} applies.*}
    1.43 +apply (blast dest: sub_K_authenticity_good [OF refl])
    1.44  done
    1.45  
    1.46  
    1.47 @@ -326,7 +330,7 @@
    1.48  apply (erule zg.induct)
    1.49  apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
    1.50  txt{*ZG4*}
    1.51 -apply (clarify dest!: Gets_imp_Says) 
    1.52 +apply clarify 
    1.53  apply (rule sub_K_authenticity, auto) 
    1.54  done
    1.55