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