ZhouGollmann: new example (fair non-repudiation protocol)
authorpaulson
Tue Aug 12 13:35:03 2003 +0200 (2003-08-12)
changeset 141452e31b8cc8788
parent 14144 7195c9b0423f
child 14146 0edd2d57eaf8
ZhouGollmann: new example (fair non-repudiation protocol)
src/HOL/Auth/CertifiedEmail.thy
src/HOL/Auth/Message.thy
src/HOL/Auth/ROOT.ML
src/HOL/Auth/ZhouGollmann.thy
src/HOL/IsaMakefile
     1.1 --- a/src/HOL/Auth/CertifiedEmail.thy	Fri Aug 08 15:05:11 2003 +0200
     1.2 +++ b/src/HOL/Auth/CertifiedEmail.thy	Tue Aug 12 13:35:03 2003 +0200
     1.3 @@ -39,12 +39,12 @@
     1.4  
     1.5  Fake: --{*The Spy may say anything he can say.  The sender field is correct,
     1.6            but agents don't use that information.*}
     1.7 -      "[| evsf \<in> certified_mail; X \<in> synth(analz(knows Spy evsf))|] 
     1.8 +      "[| evsf \<in> certified_mail; X \<in> synth(analz(spies evsf))|] 
     1.9         ==> Says Spy B X # evsf \<in> certified_mail"
    1.10  
    1.11  FakeSSL: --{*The Spy may open SSL sessions with TTP, who is the only agent
    1.12      equipped with the necessary credentials to serve as an SSL server.*}
    1.13 -	 "[| evsfssl \<in> certified_mail; X \<in> synth(analz(knows Spy evsfssl))|]
    1.14 +	 "[| evsfssl \<in> certified_mail; X \<in> synth(analz(spies evsfssl))|]
    1.15            ==> Notes TTP {|Agent Spy, Agent TTP, X|} # evsfssl \<in> certified_mail"
    1.16  
    1.17  CM1: --{*The sender approaches the recipient.  The message is a number.*}
    1.18 @@ -89,6 +89,9 @@
    1.19    ==> Gets B X#evsr \<in> certified_mail"
    1.20  
    1.21  
    1.22 +declare Says_imp_knows_Spy [THEN analz.Inj, dest]
    1.23 +declare analz_into_parts [dest]
    1.24 +
    1.25  (*A "possibility property": there are traces that reach the end*)
    1.26  lemma "\<exists>S2TTP. \<exists>evs \<in> certified_mail.
    1.27             Says TTP S (Crypt (priSK TTP) S2TTP) \<in> set evs"
    1.28 @@ -118,7 +121,7 @@
    1.29   "[|Gets R {|Agent A, Agent B, em, Number AO, Number cleartext, 
    1.30                Nonce q, S2TTP|} \<in> set evs;
    1.31      evs \<in> certified_mail|] 
    1.32 -  ==> S2TTP \<in> analz(knows Spy evs)"
    1.33 +  ==> S2TTP \<in> analz(spies evs)"
    1.34  apply (drule Gets_imp_Says, simp) 
    1.35  apply (blast dest: Says_imp_knows_Spy analz.Inj) 
    1.36  done
    1.37 @@ -128,7 +131,7 @@
    1.38  
    1.39  lemma hr_form_lemma [rule_format]:
    1.40   "evs \<in> certified_mail
    1.41 -  ==> hr \<notin> synth (analz (knows Spy evs)) --> 
    1.42 +  ==> hr \<notin> synth (analz (spies evs)) --> 
    1.43        (\<forall>S2TTP. Notes TTP {|Agent R, Agent TTP, S2TTP, pwd, hr|}
    1.44            \<in> set evs --> 
    1.45        (\<exists>clt q S em. hr = Hash {|Number clt, Nonce q, response S R q, em|}))"
    1.46 @@ -142,39 +145,39 @@
    1.47  lemma hr_form:
    1.48   "[|Notes TTP {|Agent R, Agent TTP, S2TTP, pwd, hr|} \<in> set evs;
    1.49      evs \<in> certified_mail|]
    1.50 -  ==> hr \<in> synth (analz (knows Spy evs)) | 
    1.51 +  ==> hr \<in> synth (analz (spies evs)) | 
    1.52        (\<exists>clt q S em. hr = Hash {|Number clt, Nonce q, response S R q, em|})"
    1.53  by (blast intro: hr_form_lemma) 
    1.54  
    1.55 -lemma Spy_dont_know_private_keys [rule_format]:
    1.56 -    "evs \<in> certified_mail
    1.57 -     ==> Key (privateKey b A) \<in> parts (spies evs) --> A \<in> bad"
    1.58 +lemma Spy_dont_know_private_keys [dest!]:
    1.59 +    "[|Key (privateKey b A) \<in> parts (spies evs); evs \<in> certified_mail|]
    1.60 +     ==> A \<in> bad"
    1.61 +apply (erule rev_mp) 
    1.62  apply (erule certified_mail.induct, simp_all)
    1.63  txt{*Fake*}
    1.64 -apply (blast dest: Fake_parts_insert[THEN subsetD]
    1.65 -                   analz_subset_parts[THEN subsetD])
    1.66 +apply (blast dest: Fake_parts_insert_in_Un); 
    1.67  txt{*Message 1*}
    1.68  apply blast  
    1.69  txt{*Message 3*}
    1.70  apply (frule_tac hr_form, assumption)
    1.71  apply (elim disjE exE) 
    1.72  apply (simp_all add: parts_insert2) 
    1.73 - apply (force dest!: parts_insert_subset_Un[THEN [2] rev_subsetD] 
    1.74 -                     analz_subset_parts[THEN subsetD], blast) 
    1.75 + apply (force dest!: parts_insert_subset_Un [THEN [2] rev_subsetD] 
    1.76 +                     analz_subset_parts [THEN subsetD], blast) 
    1.77  done
    1.78  
    1.79  lemma Spy_know_private_keys_iff [simp]:
    1.80      "evs \<in> certified_mail
    1.81       ==> (Key (privateKey b A) \<in> parts (spies evs)) = (A \<in> bad)"
    1.82 -by (blast intro: Spy_dont_know_private_keys parts.Inj)
    1.83 +by (blast intro: elim:); 
    1.84  
    1.85  lemma Spy_dont_know_TTPKey_parts [simp]:
    1.86 -     "evs \<in> certified_mail ==> Key (privateKey b TTP) \<notin> parts(knows Spy evs)" 
    1.87 +     "evs \<in> certified_mail ==> Key (privateKey b TTP) \<notin> parts(spies evs)" 
    1.88  by simp
    1.89  
    1.90  lemma Spy_dont_know_TTPKey_analz [simp]:
    1.91 -     "evs \<in> certified_mail ==> Key (privateKey b TTP) \<notin> analz(knows Spy evs)" 
    1.92 -by (force dest!: analz_subset_parts[THEN subsetD])
    1.93 +     "evs \<in> certified_mail ==> Key (privateKey b TTP) \<notin> analz(spies evs)"
    1.94 +by auto
    1.95  
    1.96  text{*Thus, prove any goal that assumes that @{term Spy} knows a private key
    1.97  belonging to @{term TTP}*}
    1.98 @@ -192,10 +195,9 @@
    1.99  apply (erule certified_mail.induct, simp_all)
   1.100     apply (blast  intro:parts_insertI)
   1.101  txt{*Fake SSL*}
   1.102 -apply (blast dest: analz_subset_parts[THEN subsetD] parts.Body) 
   1.103 +apply (blast dest: parts.Body) 
   1.104  txt{*Message 2*}
   1.105 -apply (blast dest!: Says_imp_knows_Spy [THEN parts.Inj] Gets_imp_Says
   1.106 -             elim!: knows_Spy_partsEs)
   1.107 +apply (blast dest!: Gets_imp_Says elim!: knows_Spy_partsEs)
   1.108  txt{*Message 3*}
   1.109  apply (frule_tac hr_form, assumption)
   1.110  apply (elim disjE exE) 
   1.111 @@ -207,8 +209,7 @@
   1.112      "evs \<in> certified_mail ==> Key (RPwd A) \<in> parts(spies evs) --> A \<in> bad"
   1.113  apply (erule certified_mail.induct, simp_all) 
   1.114  txt{*Fake*}
   1.115 -apply (blast dest: Fake_parts_insert[THEN subsetD]
   1.116 -                   analz_subset_parts[THEN subsetD])
   1.117 +apply (blast dest: Fake_parts_insert_in_Un); 
   1.118  txt{*Message 1*}
   1.119  apply blast  
   1.120  txt{*Message 3*}
   1.121 @@ -216,18 +217,18 @@
   1.122  apply (frule_tac hr_form, assumption)
   1.123  apply (elim disjE exE) 
   1.124  apply (simp_all add: parts_insert2) 
   1.125 -apply (force dest!: parts_insert_subset_Un[THEN [2] rev_subsetD]
   1.126 -                    analz_subset_parts[THEN subsetD])
   1.127 +apply (force dest!: parts_insert_subset_Un [THEN [2] rev_subsetD]
   1.128 +                    analz_subset_parts [THEN subsetD])
   1.129  done
   1.130  
   1.131  
   1.132  lemma Spy_know_RPwd_iff [simp]:
   1.133 -    "evs \<in> certified_mail ==> (Key (RPwd A) \<in> parts(knows Spy evs)) = (A\<in>bad)"
   1.134 +    "evs \<in> certified_mail ==> (Key (RPwd A) \<in> parts(spies evs)) = (A\<in>bad)"
   1.135  by (auto simp add: Spy_dont_know_RPwd) 
   1.136  
   1.137  lemma Spy_analz_RPwd_iff [simp]:
   1.138 -    "evs \<in> certified_mail ==> (Key (RPwd A) \<in> analz(knows Spy evs)) = (A\<in>bad)"
   1.139 -by (auto simp add: Spy_dont_know_RPwd [OF _ analz_subset_parts[THEN subsetD]]) 
   1.140 +    "evs \<in> certified_mail ==> (Key (RPwd A) \<in> analz(spies evs)) = (A\<in>bad)"
   1.141 +by (auto simp add: Spy_dont_know_RPwd [OF _ analz_subset_parts [THEN subsetD]])
   1.142  
   1.143  
   1.144  text{*Unused, but a guarantee of sorts*}
   1.145 @@ -237,16 +238,15 @@
   1.146  apply (erule rev_mp)
   1.147  apply (erule certified_mail.induct, simp_all) 
   1.148  txt{*Fake*}
   1.149 -apply (blast dest: Spy_dont_know_private_keys Fake_parts_insert[THEN subsetD]
   1.150 -                   analz_subset_parts[THEN subsetD])
   1.151 +apply (blast dest: Spy_dont_know_private_keys Fake_parts_insert_in_Un)
   1.152  txt{*Message 1*}
   1.153  apply blast 
   1.154  txt{*Message 3*}
   1.155  apply (frule_tac hr_form, assumption)
   1.156  apply (elim disjE exE) 
   1.157 -apply (simp_all add: parts_insert2) 
   1.158 -apply (force dest!: parts_insert_subset_Un[THEN [2] rev_subsetD]
   1.159 -                    analz_subset_parts[THEN subsetD], blast) 
   1.160 +apply (simp_all add: parts_insert2 parts_insert_knows_A) 
   1.161 + apply (blast dest!: Fake_parts_sing_imp_Un)
   1.162 +apply (blast intro: elim:);
   1.163  done
   1.164  
   1.165  
   1.166 @@ -255,8 +255,8 @@
   1.167  lemma analz_image_freshK [rule_format]:
   1.168   "evs \<in> certified_mail ==>
   1.169     \<forall>K KK. invKey (pubEK TTP) \<notin> KK -->
   1.170 -          (Key K \<in> analz (Key`KK Un (knows Spy evs))) =
   1.171 -          (K \<in> KK | Key K \<in> analz (knows Spy evs))"
   1.172 +          (Key K \<in> analz (Key`KK Un (spies evs))) =
   1.173 +          (K \<in> KK | Key K \<in> analz (spies evs))"
   1.174  apply (erule certified_mail.induct)
   1.175  apply (drule_tac [6] A=TTP in symKey_neq_priEK) 
   1.176  apply (erule_tac [6] disjE [OF hr_form]) 
   1.177 @@ -272,8 +272,8 @@
   1.178  
   1.179  lemma analz_insert_freshK:
   1.180    "[| evs \<in> certified_mail;  KAB \<noteq> invKey (pubEK TTP) |] ==>
   1.181 -      (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) =
   1.182 -      (K = KAB | Key K \<in> analz (knows Spy evs))"
   1.183 +      (Key K \<in> analz (insert (Key KAB) (spies evs))) =
   1.184 +      (K = KAB | Key K \<in> analz (spies evs))"
   1.185  by (simp only: analz_image_freshK analz_image_freshK_simps)
   1.186  
   1.187  text{*@{term S2TTP} must have originated from a valid sender
   1.188 @@ -284,11 +284,11 @@
   1.189  by (blast dest!: Notes_imp_used)
   1.190  
   1.191  
   1.192 -(*The weaker version, replacing "used evs" by "parts (knows Spy evs)", 
   1.193 +(*The weaker version, replacing "used evs" by "parts (spies evs)", 
   1.194     isn't inductive: message 3 case can't be proved *)
   1.195  lemma S2TTP_sender_lemma [rule_format]:
   1.196   "evs \<in> certified_mail ==>
   1.197 -    Key K \<notin> analz (knows Spy evs) -->
   1.198 +    Key K \<notin> analz (spies evs) -->
   1.199      (\<forall>AO. Crypt (pubEK TTP)
   1.200  	   {|Agent S, Number AO, Key K, Agent R, hs|} \<in> used evs -->
   1.201      (\<exists>m ctxt q. 
   1.202 @@ -302,11 +302,11 @@
   1.203  apply (drule_tac [5] CM2_S2TTP_parts_knows_Spy, simp)
   1.204  apply (simp add: used_Nil Crypt_notin_initState, simp_all)
   1.205  txt{*Fake*}
   1.206 -apply (blast dest: Fake_parts_sing[THEN subsetD]
   1.207 -             dest!: analz_subset_parts[THEN subsetD])  
   1.208 +apply (blast dest: Fake_parts_sing [THEN subsetD]
   1.209 +             dest!: analz_subset_parts [THEN subsetD])  
   1.210  txt{*Fake SSL*}
   1.211 -apply (blast dest: Fake_parts_sing[THEN subsetD]
   1.212 -             dest: analz_subset_parts[THEN subsetD])  
   1.213 +apply (blast dest: Fake_parts_sing [THEN subsetD]
   1.214 +             dest: analz_subset_parts [THEN subsetD])  
   1.215  txt{*Message 1*}
   1.216  apply (clarsimp, blast)
   1.217  txt{*Message 2*}
   1.218 @@ -319,7 +319,7 @@
   1.219  
   1.220  lemma S2TTP_sender:
   1.221   "[|Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|} \<in> used evs;
   1.222 -    Key K \<notin> analz (knows Spy evs);
   1.223 +    Key K \<notin> analz (spies evs);
   1.224      evs \<in> certified_mail|]
   1.225    ==> \<exists>m ctxt q. 
   1.226          hs = Hash{|Number ctxt, Nonce q, response S R q, Crypt K (Number m)|} &
   1.227 @@ -353,7 +353,7 @@
   1.228  where @{term K} is secure.*}
   1.229  lemma Key_unique_lemma [rule_format]:
   1.230       "evs \<in> certified_mail ==>
   1.231 -       Key K \<notin> analz (knows Spy evs) -->
   1.232 +       Key K \<notin> analz (spies evs) -->
   1.233         (\<forall>m cleartext q hs.
   1.234          Says S R
   1.235             {|Agent S, Agent TTP, Crypt K (Number m), Number AO,
   1.236 @@ -367,10 +367,11 @@
   1.237               Crypt (pubEK TTP) {|Agent S', Number AO', Key K, Agent R', hs'|}|}
   1.238            \<in> set evs --> R' = R & S' = S & AO' = AO & hs' = hs))" 
   1.239  apply (erule certified_mail.induct, analz_mono_contra, simp_all)
   1.240 -txt{*Fake*} 
   1.241 -apply (blast dest!: usedI S2TTP_sender analz_subset_parts[THEN subsetD]) 
   1.242 -txt{*Message 1*}
   1.243 -apply (blast dest!: Says_imp_knows_Spy [THEN parts.Inj] new_keys_not_used Crypt_imp_keysFor) 
   1.244 + prefer 2
   1.245 + txt{*Message 1*}
   1.246 + apply (blast dest!: Says_imp_knows_Spy [THEN parts.Inj] new_keys_not_used Crypt_imp_keysFor)
   1.247 +txt{*Fake*}
   1.248 +apply (auto dest!: usedI S2TTP_sender analz_subset_parts [THEN subsetD]) 
   1.249  done
   1.250  
   1.251  text{*The key determines the sender, recipient and protocol options.*}
   1.252 @@ -385,7 +386,7 @@
   1.253               Number cleartext', Nonce q',
   1.254               Crypt (pubEK TTP) {|Agent S', Number AO', Key K, Agent R', hs'|}|}
   1.255            \<in> set evs;
   1.256 -         Key K \<notin> analz (knows Spy evs);
   1.257 +         Key K \<notin> analz (spies evs);
   1.258           evs \<in> certified_mail|]
   1.259         ==> R' = R & S' = S & AO' = AO & hs' = hs"
   1.260  by (rule Key_unique_lemma, assumption+)
   1.261 @@ -400,7 +401,7 @@
   1.262        "[|Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number AO, 
   1.263                       Number cleartext, Nonce q, S2TTP|} \<in> set evs;
   1.264           S2TTP = Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|};
   1.265 -         Key K \<in> analz(knows Spy evs);
   1.266 +         Key K \<in> analz(spies evs);
   1.267  	 evs \<in> certified_mail;
   1.268           S\<noteq>Spy|]
   1.269        ==> R \<in> bad & Gets S (Crypt (priSK TTP) S2TTP) \<in> set evs"
   1.270 @@ -430,7 +431,7 @@
   1.271           S2TTP = Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|};
   1.272  	 evs \<in> certified_mail;
   1.273           S\<noteq>Spy; R \<notin> bad|]
   1.274 -      ==> Key K \<notin> analz(knows Spy evs)"
   1.275 +      ==> Key K \<notin> analz(spies evs)"
   1.276  by (blast dest: Spy_see_encrypted_key_imp) 
   1.277  
   1.278  
   1.279 @@ -471,19 +472,19 @@
   1.280  apply (erule ssubst)
   1.281  apply (erule certified_mail.induct, simp_all)
   1.282  txt{*Fake*} 
   1.283 -apply (blast dest: Fake_parts_sing[THEN subsetD]
   1.284 -             dest!: analz_subset_parts[THEN subsetD])  
   1.285 +apply (blast dest: Fake_parts_sing [THEN subsetD]
   1.286 +             dest!: analz_subset_parts [THEN subsetD])  
   1.287  txt{*Fake SSL*}
   1.288 -apply (blast dest: Fake_parts_sing[THEN subsetD]
   1.289 -            dest!: analz_subset_parts[THEN subsetD])  
   1.290 +apply (blast dest: Fake_parts_sing [THEN subsetD]
   1.291 +            dest!: analz_subset_parts [THEN subsetD])  
   1.292  txt{*Message 2*}
   1.293  apply (drule CM2_S2TTP_parts_knows_Spy, assumption)
   1.294  apply (force dest: parts_cut)
   1.295  txt{*Message 3*}
   1.296  apply (frule_tac hr_form, assumption)
   1.297  apply (elim disjE exE, simp_all) 
   1.298 -apply (blast dest: Fake_parts_sing[THEN subsetD]
   1.299 -             dest!: analz_subset_parts[THEN subsetD]) 
   1.300 +apply (blast dest: Fake_parts_sing [THEN subsetD]
   1.301 +             dest!: analz_subset_parts [THEN subsetD]) 
   1.302  done
   1.303  
   1.304  end
     2.1 --- a/src/HOL/Auth/Message.thy	Fri Aug 08 15:05:11 2003 +0200
     2.2 +++ b/src/HOL/Auth/Message.thy	Tue Aug 12 13:35:03 2003 +0200
     2.3 @@ -683,10 +683,10 @@
     2.4  done
     2.5  
     2.6  lemma analz_conj_parts [simp]: "(X \<in> analz H & X \<in> parts H) = (X \<in> analz H)"
     2.7 -by (blast intro: analz_subset_parts [THEN [2] rev_subsetD])
     2.8 +by (blast intro: analz_subset_parts [THEN subsetD])
     2.9  
    2.10  lemma analz_disj_parts [simp]: "(X \<in> analz H | X \<in> parts H) = (X \<in> parts H)"
    2.11 -by (blast intro: analz_subset_parts [THEN [2] rev_subsetD])
    2.12 +by (blast intro: analz_subset_parts [THEN subsetD])
    2.13  
    2.14  (*Without this equation, other rules for synth and analz would yield
    2.15    redundant cases*)
    2.16 @@ -994,6 +994,8 @@
    2.17  apply (simp add: parts_mono) 
    2.18  done
    2.19  
    2.20 +lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD]
    2.21 +
    2.22  method_setup spy_analz = {*
    2.23      Method.ctxt_args (fn ctxt =>
    2.24          Method.METHOD (fn facts => 
     3.1 --- a/src/HOL/Auth/ROOT.ML	Fri Aug 08 15:05:11 2003 +0200
     3.2 +++ b/src/HOL/Auth/ROOT.ML	Tue Aug 12 13:35:03 2003 +0200
     3.3 @@ -21,6 +21,8 @@
     3.4  time_use_thy "Yahalom";
     3.5  time_use_thy "Yahalom2";
     3.6  time_use_thy "Yahalom_Bad";
     3.7 +time_use_thy "ZhouGollmann";
     3.8 +
     3.9  
    3.10  (*Public-key protocols*)
    3.11  time_use_thy "NS_Public_Bad";
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Auth/ZhouGollmann.thy	Tue Aug 12 13:35:03 2003 +0200
     4.3 @@ -0,0 +1,463 @@
     4.4 +(*  Title:      HOL/Auth/ZhouGollmann
     4.5 +    ID:         $Id$
     4.6 +    Author:     Giampaolo Bella and L C Paulson, Cambridge Univ Computer Lab
     4.7 +    Copyright   2003  University of Cambridge
     4.8 +
     4.9 +The protocol of
    4.10 +  Jianying Zhou and Dieter Gollmann,
    4.11 +  A Fair Non-Repudiation Protocol,
    4.12 +  Security and Privacy 1996 (Oakland)
    4.13 +  55-61
    4.14 +*)
    4.15 +
    4.16 +theory ZhouGollmann = Public:
    4.17 +
    4.18 +syntax
    4.19 +  TTP :: agent
    4.20 +
    4.21 +translations
    4.22 +  "TTP" == "Server"
    4.23 +
    4.24 +syntax
    4.25 +  f_sub :: nat
    4.26 +  f_nro :: nat
    4.27 +  f_nrr :: nat
    4.28 +  f_con :: nat
    4.29 +
    4.30 +translations
    4.31 +  "f_sub" == "5"
    4.32 +  "f_nro" == "2"
    4.33 +  "f_nrr" == "3"
    4.34 +  "f_con" == "4"
    4.35 +
    4.36 +
    4.37 +constdefs
    4.38 +  broken :: "agent set"    
    4.39 +    --{*the compromised honest agents; TTP is included as it's not allowed to
    4.40 +        use the protocol*}
    4.41 +   "broken == insert TTP (bad - {Spy})"
    4.42 +
    4.43 +declare broken_def [simp]
    4.44 +
    4.45 +consts  zg  :: "event list set"
    4.46 +
    4.47 +inductive zg
    4.48 +  intros
    4.49 +
    4.50 +  Nil:  "[] \<in> zg"
    4.51 +
    4.52 +  Fake: "[| evsf \<in> zg;  X \<in> synth (analz (spies evsf)) |]
    4.53 +	 ==> Says Spy B X  # evsf \<in> zg"
    4.54 +
    4.55 +Reception:  "[| evsr \<in> zg; A \<noteq> B; Says A B X \<in> set evsr |]
    4.56 +	     ==> Gets B X # evsr \<in> zg"
    4.57 +
    4.58 +  (*L is fresh for honest agents.
    4.59 +    We don't require K to be fresh because we don't bother to prove secrecy!
    4.60 +    We just assume that the protocol's objective is to deliver K fairly,
    4.61 +    rather than to keep M secret.*)
    4.62 +  ZG1: "[| evs1 \<in> zg;  Nonce L \<notin> used evs1; C = Crypt K (Number m);
    4.63 +	   K \<in> symKeys;
    4.64 +	   NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|}|]
    4.65 +       ==> Says A B {|Number f_nro, Agent B, Nonce L, C, NRO|} # evs1 \<in> zg"
    4.66 +
    4.67 +  (*B must check that NRO is A's signature to learn the sender's name*)
    4.68 +  ZG2: "[| evs2 \<in> zg;
    4.69 +	   Gets B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs2;
    4.70 +	   NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
    4.71 +	   NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|}|]
    4.72 +       ==> Says B A {|Number f_nrr, Agent A, Nonce L, NRR|} # evs2  \<in>  zg"
    4.73 +
    4.74 +  (*K is symmetric must be repeated IF there's spy*)
    4.75 +  (*A must check that NRR is B's signature to learn the sender's name*)
    4.76 +  (*without spy, the matching label would be enough*)
    4.77 +  ZG3: "[| evs3 \<in> zg; C = Crypt K M; K \<in> symKeys;
    4.78 +	   Says A B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs3;
    4.79 +	   Gets A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs3;
    4.80 +	   NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
    4.81 +	   sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|}|]
    4.82 +       ==> Says A TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|}
    4.83 +	     # evs3 \<in> zg"
    4.84 +
    4.85 + (*TTP checks that sub_K is A's signature to learn who issued K, then
    4.86 +   gives credentials to A and B.  The Notes event models the availability of
    4.87 +   the credentials, but the act of fetching them is not modelled.*)
    4.88 + (*Also said TTP_prepare_ftp*)
    4.89 +  ZG4: "[| evs4 \<in> zg; K \<in> symKeys;
    4.90 +	   Gets TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|}
    4.91 +	     \<in> set evs4;
    4.92 +	   sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
    4.93 +	   con_K = Crypt (priK TTP) {|Number f_con, Agent A, Agent B,
    4.94 +				      Nonce L, Key K|}|]
    4.95 +       ==> Notes TTP {|Number f_con, Agent A, Agent B, Nonce L, Key K, con_K|}
    4.96 +	     # evs4 \<in> zg"
    4.97 +
    4.98 +
    4.99 +declare Says_imp_knows_Spy [THEN analz.Inj, dest]
   4.100 +declare Fake_parts_insert_in_Un  [dest]
   4.101 +declare analz_into_parts [dest]
   4.102 +
   4.103 +declare symKey_neq_priEK [simp]
   4.104 +declare symKey_neq_priEK [THEN not_sym, simp]
   4.105 +
   4.106 +
   4.107 +subsection {*Basic Lemmas*}
   4.108 +
   4.109 +lemma Gets_imp_Says:
   4.110 +     "[| Gets B X \<in> set evs; evs \<in> zg |] ==> \<exists>A. Says A B X \<in> set evs"
   4.111 +apply (erule rev_mp)
   4.112 +apply (erule zg.induct, auto)
   4.113 +done
   4.114 +
   4.115 +lemma Gets_imp_knows_Spy:
   4.116 +     "[| Gets B X \<in> set evs; evs \<in> zg |]  ==> X \<in> spies evs"
   4.117 +by (blast dest!: Gets_imp_Says Says_imp_knows_Spy)
   4.118 +
   4.119 +
   4.120 +text{*Lets us replace proofs about @{term "used evs"} by simpler proofs 
   4.121 +about @{term "parts (spies evs)"}.*}
   4.122 +lemma Crypt_used_imp_spies:
   4.123 +     "[| Crypt K X \<in> used evs;  K \<noteq> priK TTP; evs \<in> zg |]
   4.124 +      ==> Crypt K X \<in> parts (spies evs)"
   4.125 +apply (erule rev_mp)
   4.126 +apply (erule zg.induct)
   4.127 +apply (simp_all add: parts_insert_knows_A) 
   4.128 +done
   4.129 +
   4.130 +lemma Notes_TTP_imp_Gets:
   4.131 +     "[|Notes TTP {|Number f_con, Agent A, Agent B, Nonce L, Key K, con_K |}
   4.132 +           \<in> set evs;
   4.133 +        sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
   4.134 +        evs \<in> zg|]
   4.135 +    ==> Gets TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs"
   4.136 +apply (erule rev_mp)
   4.137 +apply (erule zg.induct, auto)
   4.138 +done
   4.139 +
   4.140 +text{*For reasoning about C, which is encrypted in message ZG2*}
   4.141 +lemma ZG2_msg_in_parts_spies:
   4.142 +     "[|Gets B {|F, B', L, C, X|} \<in> set evs; evs \<in> zg|]
   4.143 +      ==> C \<in> parts (spies evs)"
   4.144 +by (blast dest: Gets_imp_Says)
   4.145 +
   4.146 +(*classical regularity lemma on priK*)
   4.147 +lemma Spy_see_priK [simp]:
   4.148 +     "evs \<in> zg ==> (Key (priK A) \<in> parts (spies evs)) = (A \<in> bad)"
   4.149 +apply (erule zg.induct)
   4.150 +apply (frule_tac [5] ZG2_msg_in_parts_spies, auto)
   4.151 +done
   4.152 +
   4.153 +text{*So that blast can use it too*}
   4.154 +declare  Spy_see_priK [THEN [2] rev_iffD1, dest!]
   4.155 +
   4.156 +lemma Spy_analz_priK [simp]:
   4.157 +     "evs \<in> zg ==> (Key (priK A) \<in> analz (spies evs)) = (A \<in> bad)"
   4.158 +by auto 
   4.159 +
   4.160 +
   4.161 +subsection{*About NRO*}
   4.162 +
   4.163 +text{*Below we prove that if @{term NRO} exists then @{term A} definitely
   4.164 +sent it, provided @{term A} is not broken.  *}
   4.165 +
   4.166 +text{*Strong conclusion for a good agent*}
   4.167 +lemma NRO_authenticity_good:
   4.168 +     "[| NRO \<in> parts (spies evs);
   4.169 +         NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
   4.170 +         A \<notin> bad;  evs \<in> zg |]
   4.171 +     ==> Says A B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs"
   4.172 +apply clarify
   4.173 +apply (erule rev_mp)
   4.174 +apply (erule zg.induct)
   4.175 +apply (frule_tac [5] ZG2_msg_in_parts_spies, auto)  
   4.176 +done
   4.177 +
   4.178 +text{*A compromised agent: we can't be sure whether A or the Spy sends the
   4.179 +message or of the precise form of the message*}
   4.180 +lemma NRO_authenticity_bad:
   4.181 +     "[| NRO \<in> parts (spies evs);
   4.182 +         NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
   4.183 +         A \<in> bad;  evs \<in> zg |]
   4.184 +     ==> \<exists>A' \<in> {A,Spy}. \<exists>C Y. Says A' C Y \<in> set evs & NRO \<in> parts {Y}"
   4.185 +apply clarify
   4.186 +apply (erule rev_mp)
   4.187 +apply (erule zg.induct)
   4.188 +apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
   4.189 +txt{*ZG3*}
   4.190 +   prefer 4 apply blast
   4.191 +txt{*ZG2*}
   4.192 +   prefer 3 apply blast
   4.193 +txt{*Fake*}
   4.194 +apply (simp add: parts_insert_knows_A, blast) 
   4.195 +txt{*ZG1*}
   4.196 +apply (auto intro!: exI)
   4.197 +done
   4.198 +
   4.199 +theorem NRO_authenticity:
   4.200 +     "[| NRO \<in> used evs;
   4.201 +         NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
   4.202 +         A \<notin> broken;  evs \<in> zg |]
   4.203 +     ==> \<exists>C Y. Says A C Y \<in> set evs & NRO \<in> parts {Y}"
   4.204 +apply auto
   4.205 + apply (force dest!: Crypt_used_imp_spies NRO_authenticity_good)
   4.206 +apply (force dest!: Crypt_used_imp_spies NRO_authenticity_bad)
   4.207 +done
   4.208 +
   4.209 +
   4.210 +subsection{*About NRR*}
   4.211 +
   4.212 +text{*Below we prove that if @{term NRR} exists then @{term B} definitely
   4.213 +sent it, provided @{term B} is not broken.*}
   4.214 +
   4.215 +text{*Strong conclusion for a good agent*}
   4.216 +lemma NRR_authenticity_good:
   4.217 +     "[| NRR \<in> parts (spies evs);
   4.218 +         NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
   4.219 +         B \<notin> bad;  evs \<in> zg |]
   4.220 +     ==> Says B A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs"
   4.221 +apply clarify
   4.222 +apply (erule rev_mp)
   4.223 +apply (erule zg.induct)
   4.224 +apply (frule_tac [5] ZG2_msg_in_parts_spies, auto)  
   4.225 +done
   4.226 +
   4.227 +lemma NRR_authenticity_bad:
   4.228 +     "[| NRR \<in> parts (spies evs);
   4.229 +         NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
   4.230 +         B \<in> bad;  evs \<in> zg |]
   4.231 +     ==> \<exists>B' \<in> {B,Spy}. \<exists>C Y. Says B' C Y \<in> set evs & NRR \<in> parts {Y}"
   4.232 +apply clarify
   4.233 +apply (erule rev_mp)
   4.234 +apply (erule zg.induct)
   4.235 +apply (frule_tac [5] ZG2_msg_in_parts_spies)
   4.236 +apply (simp_all del: bex_simps)
   4.237 +txt{*ZG3*}
   4.238 +   prefer 4 apply blast
   4.239 +txt{*Fake*}
   4.240 +apply (simp add: parts_insert_knows_A, blast)
   4.241 +txt{*ZG1*}
   4.242 +apply (auto simp del: bex_simps)
   4.243 +txt{*ZG2*}
   4.244 +apply (force intro!: exI)
   4.245 +done
   4.246 +
   4.247 +theorem NRR_authenticity:
   4.248 +     "[| NRR \<in> used evs;
   4.249 +         NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
   4.250 +         B \<notin> broken;  evs \<in> zg |]
   4.251 +     ==> \<exists>C Y. Says B C Y \<in> set evs & NRR \<in> parts {Y}"
   4.252 +apply auto
   4.253 + apply (force dest!: Crypt_used_imp_spies NRR_authenticity_good)
   4.254 +apply (force dest!: Crypt_used_imp_spies NRR_authenticity_bad)
   4.255 +done
   4.256 +
   4.257 +
   4.258 +subsection{*Proofs About @{term sub_K}*}
   4.259 +
   4.260 +text{*Below we prove that if @{term sub_K} exists then @{term A} definitely
   4.261 +sent it, provided @{term A} is not broken.  *}
   4.262 +
   4.263 +text{*Strong conclusion for a good agent*}
   4.264 +lemma sub_K_authenticity_good:
   4.265 +     "[| sub_K \<in> parts (spies evs);
   4.266 +         sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
   4.267 +         A \<notin> bad;  evs \<in> zg |]
   4.268 +     ==> Says A TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs"
   4.269 +apply (erule rev_mp)
   4.270 +apply (erule zg.induct)
   4.271 +apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
   4.272 +txt{*Fake*} 
   4.273 +apply (blast dest!: Fake_parts_sing_imp_Un)
   4.274 +done
   4.275 +
   4.276 +text{*A compromised agent: we can't be sure whether A or the Spy sends the
   4.277 +message or of the precise form of the message*}
   4.278 +lemma sub_K_authenticity_bad:
   4.279 +     "[| sub_K \<in> parts (spies evs);
   4.280 +         sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
   4.281 +         A \<in> bad;  evs \<in> zg |]
   4.282 +     ==> \<exists>A' \<in> {A,Spy}. \<exists>C Y. Says A' C Y \<in> set evs & sub_K \<in> parts {Y}"
   4.283 +apply clarify
   4.284 +apply (erule rev_mp)
   4.285 +apply (erule zg.induct)
   4.286 +apply (frule_tac [5] ZG2_msg_in_parts_spies)
   4.287 +apply (simp_all del: bex_simps)
   4.288 +txt{*Fake*}
   4.289 +apply (simp add: parts_insert_knows_A, blast)
   4.290 +txt{*ZG1*}
   4.291 +apply (auto simp del: bex_simps)
   4.292 +txt{*ZG3*}
   4.293 +apply (force intro!: exI)
   4.294 +done
   4.295 +
   4.296 +theorem sub_K_authenticity:
   4.297 +     "[| sub_K \<in> used evs;
   4.298 +         sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
   4.299 +         A \<notin> broken;  evs \<in> zg |]
   4.300 +     ==> \<exists>C Y. Says A C Y \<in> set evs & sub_K \<in> parts {Y}"
   4.301 +apply auto
   4.302 + apply (force dest!: Crypt_used_imp_spies sub_K_authenticity_good)
   4.303 +apply (force dest!: Crypt_used_imp_spies sub_K_authenticity_bad)
   4.304 +done
   4.305 +
   4.306 +
   4.307 +subsection{*Proofs About @{term con_K}*}
   4.308 +
   4.309 +text{*Below we prove that if @{term con_K} exists, then @{term TTP} has it,
   4.310 +and therefore @{term A} and @{term B}) can get it too.  Moreover, we know
   4.311 +that @{term A} sent @{term sub_K}*}
   4.312 +
   4.313 +lemma con_K_authenticity:
   4.314 +     "[|con_K \<in> used evs;
   4.315 +        con_K = Crypt (priK TTP)
   4.316 +                  {|Number f_con, Agent A, Agent B, Nonce L, Key K|};
   4.317 +        evs \<in> zg |]
   4.318 +    ==> Notes TTP {|Number f_con, Agent A, Agent B, Nonce L, Key K, con_K|}
   4.319 +          \<in> set evs"
   4.320 +apply clarify
   4.321 +apply (erule rev_mp)
   4.322 +apply (erule zg.induct)
   4.323 +apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
   4.324 +txt{*Fake*}
   4.325 +apply (blast dest!: Fake_parts_sing_imp_Un)
   4.326 +txt{*ZG2*}
   4.327 +apply (blast dest: parts_cut)
   4.328 +done
   4.329 +
   4.330 +text{*If @{term TTP} holds @{term con_K} then @{term A} sent
   4.331 + @{term sub_K}.  We assume that @{term A} is not broken.  Nothing needs to
   4.332 + be assumed about the form of @{term con_K}!*}
   4.333 +lemma Notes_TTP_imp_Says_A:
   4.334 +     "[|Notes TTP {|Number f_con, Agent A, Agent B, Nonce L, Key K, con_K|}
   4.335 +           \<in> set evs;
   4.336 +        sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
   4.337 +        A \<notin> broken; evs \<in> zg|]
   4.338 +    ==> \<exists>C Y. Says A C Y \<in> set evs & sub_K \<in> parts {Y}"
   4.339 +by (blast dest!: Notes_TTP_imp_Gets [THEN Gets_imp_knows_Spy, THEN parts.Inj] intro: sub_K_authenticity)
   4.340 +
   4.341 +text{*If @{term con_K} exists, then @{term A} sent @{term sub_K}.*}
   4.342 +theorem B_sub_K_authenticity:
   4.343 +     "[|con_K \<in> used evs;
   4.344 +        con_K = Crypt (priK TTP) {|Number f_con, Agent A, Agent B,
   4.345 +                                   Nonce L, Key K|};
   4.346 +        sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
   4.347 +        A \<notin> broken; B \<noteq> TTP; evs \<in> zg|]
   4.348 +    ==> \<exists>C Y. Says A C Y \<in> set evs & sub_K \<in> parts {Y}"
   4.349 +by (blast dest: con_K_authenticity Notes_TTP_imp_Says_A)
   4.350 +
   4.351 +
   4.352 +subsection{*Proving fairness*}
   4.353 +
   4.354 +text{*Cannot prove that, if @{term B} has NRO, then  @{term A} has her NRR.
   4.355 +It would appear that @{term B} has a small advantage, though it is
   4.356 +useless to win disputes: @{term B} needs to present @{term con_K} as well.*}
   4.357 +
   4.358 +text{*Strange: unicity of the label protects @{term A}?*}
   4.359 +lemma A_unicity: 
   4.360 +     "[|NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, Crypt K M|};
   4.361 +        NRO \<in> parts (spies evs);
   4.362 +        Says A B {|Number f_nro, Agent B, Nonce L, Crypt K M', NRO'|}
   4.363 +          \<in> set evs;
   4.364 +        A \<notin> bad; evs \<in> zg |]
   4.365 +     ==> M'=M"
   4.366 +apply clarify
   4.367 +apply (erule rev_mp)
   4.368 +apply (erule rev_mp)
   4.369 +apply (erule zg.induct)
   4.370 +apply (frule_tac [5] ZG2_msg_in_parts_spies, auto) 
   4.371 +txt{*ZG1: freshness*}
   4.372 +apply (blast dest: parts.Body) 
   4.373 +done
   4.374 +
   4.375 +
   4.376 +text{*Fairness lemma: if @{term sub_K} exists, then @{term A} holds 
   4.377 +NRR.  Relies on unicity of labels.*}
   4.378 +lemma sub_K_implies_NRR:
   4.379 +     "[| sub_K \<in> parts (spies evs);
   4.380 +         NRO \<in> parts (spies evs);
   4.381 +         sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
   4.382 +         NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, Crypt K M|};
   4.383 +         NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, Crypt K M|};
   4.384 +         A \<notin> bad;  evs \<in> zg |]
   4.385 +     ==> Gets A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs"
   4.386 +apply clarify
   4.387 +apply (erule rev_mp)
   4.388 +apply (erule rev_mp)
   4.389 +apply (erule zg.induct)
   4.390 +apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
   4.391 +txt{*Fake*}
   4.392 +apply blast 
   4.393 +txt{*ZG1: freshness*}
   4.394 +apply (blast dest: parts.Body) 
   4.395 +txt{*ZG3*}
   4.396 +apply (blast dest: A_unicity [OF refl]) 
   4.397 +done
   4.398 +
   4.399 +
   4.400 +lemma Crypt_used_imp_L_used:
   4.401 +     "[| Crypt (priK TTP) {|F, A, B, L, K|} \<in> used evs; evs \<in> zg |]
   4.402 +      ==> L \<in> used evs"
   4.403 +apply (erule rev_mp)
   4.404 +apply (erule zg.induct, auto)
   4.405 +txt{*Fake*}
   4.406 +apply (blast dest!: Fake_parts_sing_imp_Un)
   4.407 +txt{*ZG2: freshness*}
   4.408 +apply (blast dest: parts.Body) 
   4.409 +done
   4.410 +
   4.411 +
   4.412 +text{*Fairness for @{term A}: if @{term con_K} and @{term NRO} exist, 
   4.413 +then @{term A} holds NRR.  @{term A} must be uncompromised, but there is no
   4.414 +assumption about @{term B}.*}
   4.415 +theorem A_fairness_NRO:
   4.416 +     "[|con_K \<in> used evs;
   4.417 +        NRO \<in> parts (spies evs);
   4.418 +        con_K = Crypt (priK TTP)
   4.419 +                      {|Number f_con, Agent A, Agent B, Nonce L, Key K|};
   4.420 +        NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, Crypt K M|};
   4.421 +        NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, Crypt K M|};
   4.422 +        A \<notin> bad;  evs \<in> zg |]
   4.423 +    ==> Gets A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs"
   4.424 +apply clarify
   4.425 +apply (erule rev_mp)
   4.426 +apply (erule rev_mp)
   4.427 +apply (erule zg.induct)
   4.428 +apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
   4.429 +   txt{*Fake*}
   4.430 +   apply (simp add: parts_insert_knows_A) 
   4.431 +   apply (blast dest: Fake_parts_sing_imp_Un) 
   4.432 +  txt{*ZG1*}
   4.433 +  apply (blast dest: Crypt_used_imp_L_used) 
   4.434 + txt{*ZG2*}
   4.435 + apply (blast dest: parts_cut)
   4.436 +txt{*ZG4*}
   4.437 +apply (blast intro: sub_K_implies_NRR [OF _ _ refl] 
   4.438 +             dest: Gets_imp_knows_Spy [THEN parts.Inj])
   4.439 +done
   4.440 +
   4.441 +text{*Fairness for @{term B}: NRR exists at all, then @{term B} holds NRO.
   4.442 +@{term B} must be uncompromised, but there is no assumption about @{term
   4.443 +A}. *}
   4.444 +theorem B_fairness_NRR:
   4.445 +     "[|NRR \<in> used evs;
   4.446 +        NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
   4.447 +        NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
   4.448 +        B \<notin> bad; evs \<in> zg |]
   4.449 +    ==> Gets B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs"
   4.450 +apply clarify
   4.451 +apply (erule rev_mp)
   4.452 +apply (erule zg.induct)
   4.453 +apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
   4.454 +txt{*Fake*}
   4.455 +apply (blast dest!: Fake_parts_sing_imp_Un)
   4.456 +txt{*ZG2*}
   4.457 +apply (blast dest: parts_cut)
   4.458 +done
   4.459 +
   4.460 +
   4.461 +text{*If @{term con_K} exists at all, then @{term B} can get it, by @{text
   4.462 +con_K_authenticity}.  Cannot conclude that also NRO is available to @{term B},
   4.463 +because if @{term A} were unfair, @{term A} could build message 3 without
   4.464 +building message 1, which contains NRO. *}
   4.465 +
   4.466 +end
     5.1 --- a/src/HOL/IsaMakefile	Fri Aug 08 15:05:11 2003 +0200
     5.2 +++ b/src/HOL/IsaMakefile	Tue Aug 12 13:35:03 2003 +0200
     5.3 @@ -361,9 +361,9 @@
     5.4    Auth/OtwayRees_Bad.thy Auth/Public.thy Auth/ROOT.ML \
     5.5    Auth/Recur.thy Auth/Shared.thy \
     5.6    Auth/TLS.thy Auth/WooLam.thy \
     5.7 -  Auth/Kerberos_BAN.thy \
     5.8 -  Auth/KerberosIV.ML Auth/KerberosIV.thy \
     5.9 +  Auth/Kerberos_BAN.thy Auth/KerberosIV.ML Auth/KerberosIV.thy \
    5.10    Auth/Yahalom.thy Auth/Yahalom2.thy Auth/Yahalom_Bad.thy \
    5.11 +  Auth/ZhouGollmann.thy \
    5.12    Auth/Guard/Analz.thy Auth/Guard/Extensions.thy Auth/Guard/GuardK.thy \
    5.13    Auth/Guard/Guard_Public.thy Auth/Guard/Guard_Shared.thy \
    5.14    Auth/Guard/Guard.thy Auth/Guard/List_Msg.thy \