src/HOL/Auth/ZhouGollmann.thy
 changeset 15068 58d216b32199 parent 15047 fa62de5862b9 child 16417 9bc16273c2d4
```     1.1 --- a/src/HOL/Auth/ZhouGollmann.thy	Tue Jul 20 14:23:09 2004 +0200
1.2 +++ b/src/HOL/Auth/ZhouGollmann.thy	Tue Jul 20 14:24:23 2004 +0200
1.3 @@ -178,7 +178,7 @@
1.4  sent it, provided @{term A} is not broken.*}
1.5
1.6  text{*Strong conclusion for a good agent*}
1.7 -lemma NRO_authenticity_good:
1.8 +lemma NRO_validity_good:
1.9       "[|NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
1.10          NRO \<in> parts (spies evs);
1.11          A \<notin> bad;  evs \<in> zg |]
1.12 @@ -197,7 +197,7 @@
1.13  done
1.14
1.15  text{*Holds also for @{term "A = Spy"}!*}
1.16 -theorem NRO_authenticity:
1.17 +theorem NRO_validity:
1.18       "[|Gets B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs;
1.19          NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
1.20          A \<notin> broken;  evs \<in> zg |]
1.21 @@ -207,8 +207,8 @@
1.22  apply (frule NRO_sender, auto)
1.23  txt{*We are left with the case where the sender is @{term Spy} and not
1.24    equal to @{term A}, because @{term "A \<notin> bad"}.
1.25 -  Thus theorem @{text NRO_authenticity_good} applies.*}
1.26 -apply (blast dest: NRO_authenticity_good [OF refl])
1.27 +  Thus theorem @{text NRO_validity_good} applies.*}
1.28 +apply (blast dest: NRO_validity_good [OF refl])
1.29  done
1.30
1.31
1.32 @@ -218,7 +218,7 @@
1.33  sent it, provided @{term B} is not broken.*}
1.34
1.35  text{*Strong conclusion for a good agent*}
1.36 -lemma NRR_authenticity_good:
1.37 +lemma NRR_validity_good:
1.38       "[|NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
1.39          NRR \<in> parts (spies evs);
1.40          B \<notin> bad;  evs \<in> zg |]
1.41 @@ -237,7 +237,7 @@
1.42  done
1.43
1.44  text{*Holds also for @{term "B = Spy"}!*}
1.45 -theorem NRR_authenticity:
1.46 +theorem NRR_validity:
1.47       "[|Says B' A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs;
1.48          NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
1.49          B \<notin> broken; evs \<in> zg|]
1.50 @@ -245,8 +245,8 @@
1.51  apply clarify
1.52  apply (frule NRR_sender, auto)
1.53  txt{*We are left with the case where @{term "B' = Spy"} and  @{term "B' \<noteq> B"},
1.54 -  i.e. @{term "B \<notin> bad"}, when we can apply @{text NRR_authenticity_good}.*}
1.55 - apply (blast dest: NRR_authenticity_good [OF refl])
1.56 +  i.e. @{term "B \<notin> bad"}, when we can apply @{text NRR_validity_good}.*}
1.57 + apply (blast dest: NRR_validity_good [OF refl])
1.58  done
1.59
1.60
1.61 @@ -256,7 +256,7 @@
1.62  sent it, provided @{term A} is not broken.  *}
1.63
1.64  text{*Strong conclusion for a good agent*}
1.65 -lemma sub_K_authenticity_good:
1.66 +lemma sub_K_validity_good:
1.67       "[|sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
1.68          sub_K \<in> parts (spies evs);
1.69          A \<notin> bad;  evs \<in> zg |]
1.70 @@ -277,7 +277,7 @@
1.71  done
1.72
1.73  text{*Holds also for @{term "A = Spy"}!*}
1.74 -theorem sub_K_authenticity:
1.75 +theorem sub_K_validity:
1.76       "[|Gets TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs;
1.77          sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
1.78          A \<notin> broken;  evs \<in> zg |]
1.79 @@ -287,8 +287,8 @@
1.80  apply (frule sub_K_sender, auto)
1.81  txt{*We are left with the case where the sender is @{term Spy} and not
1.82    equal to @{term A}, because @{term "A \<notin> bad"}.
1.83 -  Thus theorem @{text sub_K_authenticity_good} applies.*}
1.84 -apply (blast dest: sub_K_authenticity_good [OF refl])
1.85 +  Thus theorem @{text sub_K_validity_good} applies.*}
1.86 +apply (blast dest: sub_K_validity_good [OF refl])
1.87  done
1.88
1.89
1.90 @@ -299,7 +299,7 @@
1.91  and therefore @{term A} and @{term B}) can get it too.  Moreover, we know
1.92  that @{term A} sent @{term sub_K}*}
1.93
1.94 -lemma con_K_authenticity:
1.95 +lemma con_K_validity:
1.96       "[|con_K \<in> used evs;
1.97          con_K = Crypt (priK TTP)
1.98                    {|Number f_con, Agent A, Agent B, Nonce L, Key K|};
1.99 @@ -331,19 +331,19 @@
1.100  apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
1.101  txt{*ZG4*}
1.102  apply clarify
1.103 -apply (rule sub_K_authenticity, auto)
1.104 +apply (rule sub_K_validity, auto)
1.105  done
1.106
1.107  text{*If @{term con_K} exists, then @{term A} sent @{term sub_K}.  We again
1.108     assume that @{term A} is not broken. *}
1.109 -theorem B_sub_K_authenticity:
1.110 +theorem B_sub_K_validity:
1.111       "[|con_K \<in> used evs;
1.112          con_K = Crypt (priK TTP) {|Number f_con, Agent A, Agent B,
1.113                                     Nonce L, Key K|};
1.114          sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
1.115          A \<notin> broken; evs \<in> zg|]
1.116       ==> Says A TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs"
1.117 -by (blast dest: con_K_authenticity Notes_TTP_imp_Says_A)
1.118 +by (blast dest: con_K_validity Notes_TTP_imp_Says_A)
1.119
1.120
1.121  subsection{*Proving fairness*}
1.122 @@ -456,7 +456,7 @@
1.123
1.124
1.125  text{*If @{term con_K} exists at all, then @{term B} can get it, by @{text
1.126 -con_K_authenticity}.  Cannot conclude that also NRO is available to @{term B},
1.127 +con_K_validity}.  Cannot conclude that also NRO is available to @{term B},
1.128  because if @{term A} were unfair, @{term A} could build message 3 without
1.129  building message 1, which contains NRO. *}
1.130
```