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