# HG changeset patch
# User paulson
# Date 1060688103 -7200
# Node ID 2e31b8cc8788308bf6d47cf439cb08c2784b6a62
# Parent  7195c9b0423f3ddabf4143d467cb99130b6222b4
ZhouGollmann: new example (fair non-repudiation protocol)

diff -r 7195c9b0423f -r 2e31b8cc8788 src/HOL/Auth/CertifiedEmail.thy
--- a/src/HOL/Auth/CertifiedEmail.thy	Fri Aug 08 15:05:11 2003 +0200
+++ b/src/HOL/Auth/CertifiedEmail.thy	Tue Aug 12 13:35:03 2003 +0200
@@ -39,12 +39,12 @@
 
 Fake: --{*The Spy may say anything he can say.  The sender field is correct,
           but agents don't use that information.*}
-      "[| evsf \<in> certified_mail; X \<in> synth(analz(knows Spy evsf))|] 
+      "[| evsf \<in> certified_mail; X \<in> synth(analz(spies evsf))|] 
        ==> Says Spy B X # evsf \<in> certified_mail"
 
 FakeSSL: --{*The Spy may open SSL sessions with TTP, who is the only agent
     equipped with the necessary credentials to serve as an SSL server.*}
-	 "[| evsfssl \<in> certified_mail; X \<in> synth(analz(knows Spy evsfssl))|]
+	 "[| evsfssl \<in> certified_mail; X \<in> synth(analz(spies evsfssl))|]
           ==> Notes TTP {|Agent Spy, Agent TTP, X|} # evsfssl \<in> certified_mail"
 
 CM1: --{*The sender approaches the recipient.  The message is a number.*}
@@ -89,6 +89,9 @@
   ==> Gets B X#evsr \<in> certified_mail"
 
 
+declare Says_imp_knows_Spy [THEN analz.Inj, dest]
+declare analz_into_parts [dest]
+
 (*A "possibility property": there are traces that reach the end*)
 lemma "\<exists>S2TTP. \<exists>evs \<in> certified_mail.
            Says TTP S (Crypt (priSK TTP) S2TTP) \<in> set evs"
@@ -118,7 +121,7 @@
  "[|Gets R {|Agent A, Agent B, em, Number AO, Number cleartext, 
               Nonce q, S2TTP|} \<in> set evs;
     evs \<in> certified_mail|] 
-  ==> S2TTP \<in> analz(knows Spy evs)"
+  ==> S2TTP \<in> analz(spies evs)"
 apply (drule Gets_imp_Says, simp) 
 apply (blast dest: Says_imp_knows_Spy analz.Inj) 
 done
@@ -128,7 +131,7 @@
 
 lemma hr_form_lemma [rule_format]:
  "evs \<in> certified_mail
-  ==> hr \<notin> synth (analz (knows Spy evs)) --> 
+  ==> hr \<notin> synth (analz (spies evs)) --> 
       (\<forall>S2TTP. Notes TTP {|Agent R, Agent TTP, S2TTP, pwd, hr|}
           \<in> set evs --> 
       (\<exists>clt q S em. hr = Hash {|Number clt, Nonce q, response S R q, em|}))"
@@ -142,39 +145,39 @@
 lemma hr_form:
  "[|Notes TTP {|Agent R, Agent TTP, S2TTP, pwd, hr|} \<in> set evs;
     evs \<in> certified_mail|]
-  ==> hr \<in> synth (analz (knows Spy evs)) | 
+  ==> hr \<in> synth (analz (spies evs)) | 
       (\<exists>clt q S em. hr = Hash {|Number clt, Nonce q, response S R q, em|})"
 by (blast intro: hr_form_lemma) 
 
-lemma Spy_dont_know_private_keys [rule_format]:
-    "evs \<in> certified_mail
-     ==> Key (privateKey b A) \<in> parts (spies evs) --> A \<in> bad"
+lemma Spy_dont_know_private_keys [dest!]:
+    "[|Key (privateKey b A) \<in> parts (spies evs); evs \<in> certified_mail|]
+     ==> A \<in> bad"
+apply (erule rev_mp) 
 apply (erule certified_mail.induct, simp_all)
 txt{*Fake*}
-apply (blast dest: Fake_parts_insert[THEN subsetD]
-                   analz_subset_parts[THEN subsetD])
+apply (blast dest: Fake_parts_insert_in_Un); 
 txt{*Message 1*}
 apply blast  
 txt{*Message 3*}
 apply (frule_tac hr_form, assumption)
 apply (elim disjE exE) 
 apply (simp_all add: parts_insert2) 
- apply (force dest!: parts_insert_subset_Un[THEN [2] rev_subsetD] 
-                     analz_subset_parts[THEN subsetD], blast) 
+ apply (force dest!: parts_insert_subset_Un [THEN [2] rev_subsetD] 
+                     analz_subset_parts [THEN subsetD], blast) 
 done
 
 lemma Spy_know_private_keys_iff [simp]:
     "evs \<in> certified_mail
      ==> (Key (privateKey b A) \<in> parts (spies evs)) = (A \<in> bad)"
-by (blast intro: Spy_dont_know_private_keys parts.Inj)
+by (blast intro: elim:); 
 
 lemma Spy_dont_know_TTPKey_parts [simp]:
-     "evs \<in> certified_mail ==> Key (privateKey b TTP) \<notin> parts(knows Spy evs)" 
+     "evs \<in> certified_mail ==> Key (privateKey b TTP) \<notin> parts(spies evs)" 
 by simp
 
 lemma Spy_dont_know_TTPKey_analz [simp]:
-     "evs \<in> certified_mail ==> Key (privateKey b TTP) \<notin> analz(knows Spy evs)" 
-by (force dest!: analz_subset_parts[THEN subsetD])
+     "evs \<in> certified_mail ==> Key (privateKey b TTP) \<notin> analz(spies evs)"
+by auto
 
 text{*Thus, prove any goal that assumes that @{term Spy} knows a private key
 belonging to @{term TTP}*}
@@ -192,10 +195,9 @@
 apply (erule certified_mail.induct, simp_all)
    apply (blast  intro:parts_insertI)
 txt{*Fake SSL*}
-apply (blast dest: analz_subset_parts[THEN subsetD] parts.Body) 
+apply (blast dest: parts.Body) 
 txt{*Message 2*}
-apply (blast dest!: Says_imp_knows_Spy [THEN parts.Inj] Gets_imp_Says
-             elim!: knows_Spy_partsEs)
+apply (blast dest!: Gets_imp_Says elim!: knows_Spy_partsEs)
 txt{*Message 3*}
 apply (frule_tac hr_form, assumption)
 apply (elim disjE exE) 
@@ -207,8 +209,7 @@
     "evs \<in> certified_mail ==> Key (RPwd A) \<in> parts(spies evs) --> A \<in> bad"
 apply (erule certified_mail.induct, simp_all) 
 txt{*Fake*}
-apply (blast dest: Fake_parts_insert[THEN subsetD]
-                   analz_subset_parts[THEN subsetD])
+apply (blast dest: Fake_parts_insert_in_Un); 
 txt{*Message 1*}
 apply blast  
 txt{*Message 3*}
@@ -216,18 +217,18 @@
 apply (frule_tac hr_form, assumption)
 apply (elim disjE exE) 
 apply (simp_all add: parts_insert2) 
-apply (force dest!: parts_insert_subset_Un[THEN [2] rev_subsetD]
-                    analz_subset_parts[THEN subsetD])
+apply (force dest!: parts_insert_subset_Un [THEN [2] rev_subsetD]
+                    analz_subset_parts [THEN subsetD])
 done
 
 
 lemma Spy_know_RPwd_iff [simp]:
-    "evs \<in> certified_mail ==> (Key (RPwd A) \<in> parts(knows Spy evs)) = (A\<in>bad)"
+    "evs \<in> certified_mail ==> (Key (RPwd A) \<in> parts(spies evs)) = (A\<in>bad)"
 by (auto simp add: Spy_dont_know_RPwd) 
 
 lemma Spy_analz_RPwd_iff [simp]:
-    "evs \<in> certified_mail ==> (Key (RPwd A) \<in> analz(knows Spy evs)) = (A\<in>bad)"
-by (auto simp add: Spy_dont_know_RPwd [OF _ analz_subset_parts[THEN subsetD]]) 
+    "evs \<in> certified_mail ==> (Key (RPwd A) \<in> analz(spies evs)) = (A\<in>bad)"
+by (auto simp add: Spy_dont_know_RPwd [OF _ analz_subset_parts [THEN subsetD]])
 
 
 text{*Unused, but a guarantee of sorts*}
@@ -237,16 +238,15 @@
 apply (erule rev_mp)
 apply (erule certified_mail.induct, simp_all) 
 txt{*Fake*}
-apply (blast dest: Spy_dont_know_private_keys Fake_parts_insert[THEN subsetD]
-                   analz_subset_parts[THEN subsetD])
+apply (blast dest: Spy_dont_know_private_keys Fake_parts_insert_in_Un)
 txt{*Message 1*}
 apply blast 
 txt{*Message 3*}
 apply (frule_tac hr_form, assumption)
 apply (elim disjE exE) 
-apply (simp_all add: parts_insert2) 
-apply (force dest!: parts_insert_subset_Un[THEN [2] rev_subsetD]
-                    analz_subset_parts[THEN subsetD], blast) 
+apply (simp_all add: parts_insert2 parts_insert_knows_A) 
+ apply (blast dest!: Fake_parts_sing_imp_Un)
+apply (blast intro: elim:);
 done
 
 
@@ -255,8 +255,8 @@
 lemma analz_image_freshK [rule_format]:
  "evs \<in> certified_mail ==>
    \<forall>K KK. invKey (pubEK TTP) \<notin> KK -->
-          (Key K \<in> analz (Key`KK Un (knows Spy evs))) =
-          (K \<in> KK | Key K \<in> analz (knows Spy evs))"
+          (Key K \<in> analz (Key`KK Un (spies evs))) =
+          (K \<in> KK | Key K \<in> analz (spies evs))"
 apply (erule certified_mail.induct)
 apply (drule_tac [6] A=TTP in symKey_neq_priEK) 
 apply (erule_tac [6] disjE [OF hr_form]) 
@@ -272,8 +272,8 @@
 
 lemma analz_insert_freshK:
   "[| evs \<in> certified_mail;  KAB \<noteq> invKey (pubEK TTP) |] ==>
-      (Key K \<in> analz (insert (Key KAB) (knows Spy evs))) =
-      (K = KAB | Key K \<in> analz (knows Spy evs))"
+      (Key K \<in> analz (insert (Key KAB) (spies evs))) =
+      (K = KAB | Key K \<in> analz (spies evs))"
 by (simp only: analz_image_freshK analz_image_freshK_simps)
 
 text{*@{term S2TTP} must have originated from a valid sender
@@ -284,11 +284,11 @@
 by (blast dest!: Notes_imp_used)
 
 
-(*The weaker version, replacing "used evs" by "parts (knows Spy evs)", 
+(*The weaker version, replacing "used evs" by "parts (spies evs)", 
    isn't inductive: message 3 case can't be proved *)
 lemma S2TTP_sender_lemma [rule_format]:
  "evs \<in> certified_mail ==>
-    Key K \<notin> analz (knows Spy evs) -->
+    Key K \<notin> analz (spies evs) -->
     (\<forall>AO. Crypt (pubEK TTP)
 	   {|Agent S, Number AO, Key K, Agent R, hs|} \<in> used evs -->
     (\<exists>m ctxt q. 
@@ -302,11 +302,11 @@
 apply (drule_tac [5] CM2_S2TTP_parts_knows_Spy, simp)
 apply (simp add: used_Nil Crypt_notin_initState, simp_all)
 txt{*Fake*}
-apply (blast dest: Fake_parts_sing[THEN subsetD]
-             dest!: analz_subset_parts[THEN subsetD])  
+apply (blast dest: Fake_parts_sing [THEN subsetD]
+             dest!: analz_subset_parts [THEN subsetD])  
 txt{*Fake SSL*}
-apply (blast dest: Fake_parts_sing[THEN subsetD]
-             dest: analz_subset_parts[THEN subsetD])  
+apply (blast dest: Fake_parts_sing [THEN subsetD]
+             dest: analz_subset_parts [THEN subsetD])  
 txt{*Message 1*}
 apply (clarsimp, blast)
 txt{*Message 2*}
@@ -319,7 +319,7 @@
 
 lemma S2TTP_sender:
  "[|Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|} \<in> used evs;
-    Key K \<notin> analz (knows Spy evs);
+    Key K \<notin> analz (spies evs);
     evs \<in> certified_mail|]
   ==> \<exists>m ctxt q. 
         hs = Hash{|Number ctxt, Nonce q, response S R q, Crypt K (Number m)|} &
@@ -353,7 +353,7 @@
 where @{term K} is secure.*}
 lemma Key_unique_lemma [rule_format]:
      "evs \<in> certified_mail ==>
-       Key K \<notin> analz (knows Spy evs) -->
+       Key K \<notin> analz (spies evs) -->
        (\<forall>m cleartext q hs.
         Says S R
            {|Agent S, Agent TTP, Crypt K (Number m), Number AO,
@@ -367,10 +367,11 @@
              Crypt (pubEK TTP) {|Agent S', Number AO', Key K, Agent R', hs'|}|}
           \<in> set evs --> R' = R & S' = S & AO' = AO & hs' = hs))" 
 apply (erule certified_mail.induct, analz_mono_contra, simp_all)
-txt{*Fake*} 
-apply (blast dest!: usedI S2TTP_sender analz_subset_parts[THEN subsetD]) 
-txt{*Message 1*}
-apply (blast dest!: Says_imp_knows_Spy [THEN parts.Inj] new_keys_not_used Crypt_imp_keysFor) 
+ prefer 2
+ txt{*Message 1*}
+ apply (blast dest!: Says_imp_knows_Spy [THEN parts.Inj] new_keys_not_used Crypt_imp_keysFor)
+txt{*Fake*}
+apply (auto dest!: usedI S2TTP_sender analz_subset_parts [THEN subsetD]) 
 done
 
 text{*The key determines the sender, recipient and protocol options.*}
@@ -385,7 +386,7 @@
              Number cleartext', Nonce q',
              Crypt (pubEK TTP) {|Agent S', Number AO', Key K, Agent R', hs'|}|}
           \<in> set evs;
-         Key K \<notin> analz (knows Spy evs);
+         Key K \<notin> analz (spies evs);
          evs \<in> certified_mail|]
        ==> R' = R & S' = S & AO' = AO & hs' = hs"
 by (rule Key_unique_lemma, assumption+)
@@ -400,7 +401,7 @@
       "[|Says S R {|Agent S, Agent TTP, Crypt K (Number m), Number AO, 
                      Number cleartext, Nonce q, S2TTP|} \<in> set evs;
          S2TTP = Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|};
-         Key K \<in> analz(knows Spy evs);
+         Key K \<in> analz(spies evs);
 	 evs \<in> certified_mail;
          S\<noteq>Spy|]
       ==> R \<in> bad & Gets S (Crypt (priSK TTP) S2TTP) \<in> set evs"
@@ -430,7 +431,7 @@
          S2TTP = Crypt (pubEK TTP) {|Agent S, Number AO, Key K, Agent R, hs|};
 	 evs \<in> certified_mail;
          S\<noteq>Spy; R \<notin> bad|]
-      ==> Key K \<notin> analz(knows Spy evs)"
+      ==> Key K \<notin> analz(spies evs)"
 by (blast dest: Spy_see_encrypted_key_imp) 
 
 
@@ -471,19 +472,19 @@
 apply (erule ssubst)
 apply (erule certified_mail.induct, simp_all)
 txt{*Fake*} 
-apply (blast dest: Fake_parts_sing[THEN subsetD]
-             dest!: analz_subset_parts[THEN subsetD])  
+apply (blast dest: Fake_parts_sing [THEN subsetD]
+             dest!: analz_subset_parts [THEN subsetD])  
 txt{*Fake SSL*}
-apply (blast dest: Fake_parts_sing[THEN subsetD]
-            dest!: analz_subset_parts[THEN subsetD])  
+apply (blast dest: Fake_parts_sing [THEN subsetD]
+            dest!: analz_subset_parts [THEN subsetD])  
 txt{*Message 2*}
 apply (drule CM2_S2TTP_parts_knows_Spy, assumption)
 apply (force dest: parts_cut)
 txt{*Message 3*}
 apply (frule_tac hr_form, assumption)
 apply (elim disjE exE, simp_all) 
-apply (blast dest: Fake_parts_sing[THEN subsetD]
-             dest!: analz_subset_parts[THEN subsetD]) 
+apply (blast dest: Fake_parts_sing [THEN subsetD]
+             dest!: analz_subset_parts [THEN subsetD]) 
 done
 
 end
diff -r 7195c9b0423f -r 2e31b8cc8788 src/HOL/Auth/Message.thy
--- a/src/HOL/Auth/Message.thy	Fri Aug 08 15:05:11 2003 +0200
+++ b/src/HOL/Auth/Message.thy	Tue Aug 12 13:35:03 2003 +0200
@@ -683,10 +683,10 @@
 done
 
 lemma analz_conj_parts [simp]: "(X \<in> analz H & X \<in> parts H) = (X \<in> analz H)"
-by (blast intro: analz_subset_parts [THEN [2] rev_subsetD])
+by (blast intro: analz_subset_parts [THEN subsetD])
 
 lemma analz_disj_parts [simp]: "(X \<in> analz H | X \<in> parts H) = (X \<in> parts H)"
-by (blast intro: analz_subset_parts [THEN [2] rev_subsetD])
+by (blast intro: analz_subset_parts [THEN subsetD])
 
 (*Without this equation, other rules for synth and analz would yield
   redundant cases*)
@@ -994,6 +994,8 @@
 apply (simp add: parts_mono) 
 done
 
+lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD]
+
 method_setup spy_analz = {*
     Method.ctxt_args (fn ctxt =>
         Method.METHOD (fn facts => 
diff -r 7195c9b0423f -r 2e31b8cc8788 src/HOL/Auth/ROOT.ML
--- a/src/HOL/Auth/ROOT.ML	Fri Aug 08 15:05:11 2003 +0200
+++ b/src/HOL/Auth/ROOT.ML	Tue Aug 12 13:35:03 2003 +0200
@@ -21,6 +21,8 @@
 time_use_thy "Yahalom";
 time_use_thy "Yahalom2";
 time_use_thy "Yahalom_Bad";
+time_use_thy "ZhouGollmann";
+
 
 (*Public-key protocols*)
 time_use_thy "NS_Public_Bad";
diff -r 7195c9b0423f -r 2e31b8cc8788 src/HOL/Auth/ZhouGollmann.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Auth/ZhouGollmann.thy	Tue Aug 12 13:35:03 2003 +0200
@@ -0,0 +1,463 @@
+(*  Title:      HOL/Auth/ZhouGollmann
+    ID:         $Id$
+    Author:     Giampaolo Bella and L C Paulson, Cambridge Univ Computer Lab
+    Copyright   2003  University of Cambridge
+
+The protocol of
+  Jianying Zhou and Dieter Gollmann,
+  A Fair Non-Repudiation Protocol,
+  Security and Privacy 1996 (Oakland)
+  55-61
+*)
+
+theory ZhouGollmann = Public:
+
+syntax
+  TTP :: agent
+
+translations
+  "TTP" == "Server"
+
+syntax
+  f_sub :: nat
+  f_nro :: nat
+  f_nrr :: nat
+  f_con :: nat
+
+translations
+  "f_sub" == "5"
+  "f_nro" == "2"
+  "f_nrr" == "3"
+  "f_con" == "4"
+
+
+constdefs
+  broken :: "agent set"    
+    --{*the compromised honest agents; TTP is included as it's not allowed to
+        use the protocol*}
+   "broken == insert TTP (bad - {Spy})"
+
+declare broken_def [simp]
+
+consts  zg  :: "event list set"
+
+inductive zg
+  intros
+
+  Nil:  "[] \<in> zg"
+
+  Fake: "[| evsf \<in> zg;  X \<in> synth (analz (spies evsf)) |]
+	 ==> Says Spy B X  # evsf \<in> zg"
+
+Reception:  "[| evsr \<in> zg; A \<noteq> B; Says A B X \<in> set evsr |]
+	     ==> Gets B X # evsr \<in> zg"
+
+  (*L is fresh for honest agents.
+    We don't require K to be fresh because we don't bother to prove secrecy!
+    We just assume that the protocol's objective is to deliver K fairly,
+    rather than to keep M secret.*)
+  ZG1: "[| evs1 \<in> zg;  Nonce L \<notin> used evs1; C = Crypt K (Number m);
+	   K \<in> symKeys;
+	   NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|}|]
+       ==> Says A B {|Number f_nro, Agent B, Nonce L, C, NRO|} # evs1 \<in> zg"
+
+  (*B must check that NRO is A's signature to learn the sender's name*)
+  ZG2: "[| evs2 \<in> zg;
+	   Gets B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs2;
+	   NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
+	   NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|}|]
+       ==> Says B A {|Number f_nrr, Agent A, Nonce L, NRR|} # evs2  \<in>  zg"
+
+  (*K is symmetric must be repeated IF there's spy*)
+  (*A must check that NRR is B's signature to learn the sender's name*)
+  (*without spy, the matching label would be enough*)
+  ZG3: "[| evs3 \<in> zg; C = Crypt K M; K \<in> symKeys;
+	   Says A B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs3;
+	   Gets A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs3;
+	   NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
+	   sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|}|]
+       ==> Says A TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|}
+	     # evs3 \<in> zg"
+
+ (*TTP checks that sub_K is A's signature to learn who issued K, then
+   gives credentials to A and B.  The Notes event models the availability of
+   the credentials, but the act of fetching them is not modelled.*)
+ (*Also said TTP_prepare_ftp*)
+  ZG4: "[| evs4 \<in> zg; K \<in> symKeys;
+	   Gets TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|}
+	     \<in> set evs4;
+	   sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
+	   con_K = Crypt (priK TTP) {|Number f_con, Agent A, Agent B,
+				      Nonce L, Key K|}|]
+       ==> Notes TTP {|Number f_con, Agent A, Agent B, Nonce L, Key K, con_K|}
+	     # evs4 \<in> zg"
+
+
+declare Says_imp_knows_Spy [THEN analz.Inj, dest]
+declare Fake_parts_insert_in_Un  [dest]
+declare analz_into_parts [dest]
+
+declare symKey_neq_priEK [simp]
+declare symKey_neq_priEK [THEN not_sym, simp]
+
+
+subsection {*Basic Lemmas*}
+
+lemma Gets_imp_Says:
+     "[| Gets B X \<in> set evs; evs \<in> zg |] ==> \<exists>A. Says A B X \<in> set evs"
+apply (erule rev_mp)
+apply (erule zg.induct, auto)
+done
+
+lemma Gets_imp_knows_Spy:
+     "[| Gets B X \<in> set evs; evs \<in> zg |]  ==> X \<in> spies evs"
+by (blast dest!: Gets_imp_Says Says_imp_knows_Spy)
+
+
+text{*Lets us replace proofs about @{term "used evs"} by simpler proofs 
+about @{term "parts (spies evs)"}.*}
+lemma Crypt_used_imp_spies:
+     "[| Crypt K X \<in> used evs;  K \<noteq> priK TTP; evs \<in> zg |]
+      ==> Crypt K X \<in> parts (spies evs)"
+apply (erule rev_mp)
+apply (erule zg.induct)
+apply (simp_all add: parts_insert_knows_A) 
+done
+
+lemma Notes_TTP_imp_Gets:
+     "[|Notes TTP {|Number f_con, Agent A, Agent B, Nonce L, Key K, con_K |}
+           \<in> set evs;
+        sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
+        evs \<in> zg|]
+    ==> Gets TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs"
+apply (erule rev_mp)
+apply (erule zg.induct, auto)
+done
+
+text{*For reasoning about C, which is encrypted in message ZG2*}
+lemma ZG2_msg_in_parts_spies:
+     "[|Gets B {|F, B', L, C, X|} \<in> set evs; evs \<in> zg|]
+      ==> C \<in> parts (spies evs)"
+by (blast dest: Gets_imp_Says)
+
+(*classical regularity lemma on priK*)
+lemma Spy_see_priK [simp]:
+     "evs \<in> zg ==> (Key (priK A) \<in> parts (spies evs)) = (A \<in> bad)"
+apply (erule zg.induct)
+apply (frule_tac [5] ZG2_msg_in_parts_spies, auto)
+done
+
+text{*So that blast can use it too*}
+declare  Spy_see_priK [THEN [2] rev_iffD1, dest!]
+
+lemma Spy_analz_priK [simp]:
+     "evs \<in> zg ==> (Key (priK A) \<in> analz (spies evs)) = (A \<in> bad)"
+by auto 
+
+
+subsection{*About NRO*}
+
+text{*Below we prove that if @{term NRO} exists then @{term A} definitely
+sent it, provided @{term A} is not broken.  *}
+
+text{*Strong conclusion for a good agent*}
+lemma NRO_authenticity_good:
+     "[| NRO \<in> parts (spies evs);
+         NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
+         A \<notin> bad;  evs \<in> zg |]
+     ==> Says A B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs"
+apply clarify
+apply (erule rev_mp)
+apply (erule zg.induct)
+apply (frule_tac [5] ZG2_msg_in_parts_spies, auto)  
+done
+
+text{*A compromised agent: we can't be sure whether A or the Spy sends the
+message or of the precise form of the message*}
+lemma NRO_authenticity_bad:
+     "[| NRO \<in> parts (spies evs);
+         NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
+         A \<in> bad;  evs \<in> zg |]
+     ==> \<exists>A' \<in> {A,Spy}. \<exists>C Y. Says A' C Y \<in> set evs & NRO \<in> parts {Y}"
+apply clarify
+apply (erule rev_mp)
+apply (erule zg.induct)
+apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
+txt{*ZG3*}
+   prefer 4 apply blast
+txt{*ZG2*}
+   prefer 3 apply blast
+txt{*Fake*}
+apply (simp add: parts_insert_knows_A, blast) 
+txt{*ZG1*}
+apply (auto intro!: exI)
+done
+
+theorem NRO_authenticity:
+     "[| NRO \<in> used evs;
+         NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
+         A \<notin> broken;  evs \<in> zg |]
+     ==> \<exists>C Y. Says A C Y \<in> set evs & NRO \<in> parts {Y}"
+apply auto
+ apply (force dest!: Crypt_used_imp_spies NRO_authenticity_good)
+apply (force dest!: Crypt_used_imp_spies NRO_authenticity_bad)
+done
+
+
+subsection{*About NRR*}
+
+text{*Below we prove that if @{term NRR} exists then @{term B} definitely
+sent it, provided @{term B} is not broken.*}
+
+text{*Strong conclusion for a good agent*}
+lemma NRR_authenticity_good:
+     "[| NRR \<in> parts (spies evs);
+         NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
+         B \<notin> bad;  evs \<in> zg |]
+     ==> Says B A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs"
+apply clarify
+apply (erule rev_mp)
+apply (erule zg.induct)
+apply (frule_tac [5] ZG2_msg_in_parts_spies, auto)  
+done
+
+lemma NRR_authenticity_bad:
+     "[| NRR \<in> parts (spies evs);
+         NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
+         B \<in> bad;  evs \<in> zg |]
+     ==> \<exists>B' \<in> {B,Spy}. \<exists>C Y. Says B' C Y \<in> set evs & NRR \<in> parts {Y}"
+apply clarify
+apply (erule rev_mp)
+apply (erule zg.induct)
+apply (frule_tac [5] ZG2_msg_in_parts_spies)
+apply (simp_all del: bex_simps)
+txt{*ZG3*}
+   prefer 4 apply blast
+txt{*Fake*}
+apply (simp add: parts_insert_knows_A, blast)
+txt{*ZG1*}
+apply (auto simp del: bex_simps)
+txt{*ZG2*}
+apply (force intro!: exI)
+done
+
+theorem NRR_authenticity:
+     "[| NRR \<in> used evs;
+         NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
+         B \<notin> broken;  evs \<in> zg |]
+     ==> \<exists>C Y. Says B C Y \<in> set evs & NRR \<in> parts {Y}"
+apply auto
+ apply (force dest!: Crypt_used_imp_spies NRR_authenticity_good)
+apply (force dest!: Crypt_used_imp_spies NRR_authenticity_bad)
+done
+
+
+subsection{*Proofs About @{term sub_K}*}
+
+text{*Below we prove that if @{term sub_K} exists then @{term A} definitely
+sent it, provided @{term A} is not broken.  *}
+
+text{*Strong conclusion for a good agent*}
+lemma sub_K_authenticity_good:
+     "[| sub_K \<in> parts (spies evs);
+         sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
+         A \<notin> bad;  evs \<in> zg |]
+     ==> Says A TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs"
+apply (erule rev_mp)
+apply (erule zg.induct)
+apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
+txt{*Fake*} 
+apply (blast dest!: Fake_parts_sing_imp_Un)
+done
+
+text{*A compromised agent: we can't be sure whether A or the Spy sends the
+message or of the precise form of the message*}
+lemma sub_K_authenticity_bad:
+     "[| sub_K \<in> parts (spies evs);
+         sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
+         A \<in> bad;  evs \<in> zg |]
+     ==> \<exists>A' \<in> {A,Spy}. \<exists>C Y. Says A' C Y \<in> set evs & sub_K \<in> parts {Y}"
+apply clarify
+apply (erule rev_mp)
+apply (erule zg.induct)
+apply (frule_tac [5] ZG2_msg_in_parts_spies)
+apply (simp_all del: bex_simps)
+txt{*Fake*}
+apply (simp add: parts_insert_knows_A, blast)
+txt{*ZG1*}
+apply (auto simp del: bex_simps)
+txt{*ZG3*}
+apply (force intro!: exI)
+done
+
+theorem sub_K_authenticity:
+     "[| sub_K \<in> used evs;
+         sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
+         A \<notin> broken;  evs \<in> zg |]
+     ==> \<exists>C Y. Says A C Y \<in> set evs & sub_K \<in> parts {Y}"
+apply auto
+ apply (force dest!: Crypt_used_imp_spies sub_K_authenticity_good)
+apply (force dest!: Crypt_used_imp_spies sub_K_authenticity_bad)
+done
+
+
+subsection{*Proofs About @{term con_K}*}
+
+text{*Below we prove that if @{term con_K} exists, then @{term TTP} has it,
+and therefore @{term A} and @{term B}) can get it too.  Moreover, we know
+that @{term A} sent @{term sub_K}*}
+
+lemma con_K_authenticity:
+     "[|con_K \<in> used evs;
+        con_K = Crypt (priK TTP)
+                  {|Number f_con, Agent A, Agent B, Nonce L, Key K|};
+        evs \<in> zg |]
+    ==> Notes TTP {|Number f_con, Agent A, Agent B, Nonce L, Key K, con_K|}
+          \<in> set evs"
+apply clarify
+apply (erule rev_mp)
+apply (erule zg.induct)
+apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
+txt{*Fake*}
+apply (blast dest!: Fake_parts_sing_imp_Un)
+txt{*ZG2*}
+apply (blast dest: parts_cut)
+done
+
+text{*If @{term TTP} holds @{term con_K} then @{term A} sent
+ @{term sub_K}.  We assume that @{term A} is not broken.  Nothing needs to
+ be assumed about the form of @{term con_K}!*}
+lemma Notes_TTP_imp_Says_A:
+     "[|Notes TTP {|Number f_con, Agent A, Agent B, Nonce L, Key K, con_K|}
+           \<in> set evs;
+        sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
+        A \<notin> broken; evs \<in> zg|]
+    ==> \<exists>C Y. Says A C Y \<in> set evs & sub_K \<in> parts {Y}"
+by (blast dest!: Notes_TTP_imp_Gets [THEN Gets_imp_knows_Spy, THEN parts.Inj] intro: sub_K_authenticity)
+
+text{*If @{term con_K} exists, then @{term A} sent @{term sub_K}.*}
+theorem B_sub_K_authenticity:
+     "[|con_K \<in> used evs;
+        con_K = Crypt (priK TTP) {|Number f_con, Agent A, Agent B,
+                                   Nonce L, Key K|};
+        sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
+        A \<notin> broken; B \<noteq> TTP; evs \<in> zg|]
+    ==> \<exists>C Y. Says A C Y \<in> set evs & sub_K \<in> parts {Y}"
+by (blast dest: con_K_authenticity Notes_TTP_imp_Says_A)
+
+
+subsection{*Proving fairness*}
+
+text{*Cannot prove that, if @{term B} has NRO, then  @{term A} has her NRR.
+It would appear that @{term B} has a small advantage, though it is
+useless to win disputes: @{term B} needs to present @{term con_K} as well.*}
+
+text{*Strange: unicity of the label protects @{term A}?*}
+lemma A_unicity: 
+     "[|NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, Crypt K M|};
+        NRO \<in> parts (spies evs);
+        Says A B {|Number f_nro, Agent B, Nonce L, Crypt K M', NRO'|}
+          \<in> set evs;
+        A \<notin> bad; evs \<in> zg |]
+     ==> M'=M"
+apply clarify
+apply (erule rev_mp)
+apply (erule rev_mp)
+apply (erule zg.induct)
+apply (frule_tac [5] ZG2_msg_in_parts_spies, auto) 
+txt{*ZG1: freshness*}
+apply (blast dest: parts.Body) 
+done
+
+
+text{*Fairness lemma: if @{term sub_K} exists, then @{term A} holds 
+NRR.  Relies on unicity of labels.*}
+lemma sub_K_implies_NRR:
+     "[| sub_K \<in> parts (spies evs);
+         NRO \<in> parts (spies evs);
+         sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
+         NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, Crypt K M|};
+         NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, Crypt K M|};
+         A \<notin> bad;  evs \<in> zg |]
+     ==> Gets A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs"
+apply clarify
+apply (erule rev_mp)
+apply (erule rev_mp)
+apply (erule zg.induct)
+apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
+txt{*Fake*}
+apply blast 
+txt{*ZG1: freshness*}
+apply (blast dest: parts.Body) 
+txt{*ZG3*}
+apply (blast dest: A_unicity [OF refl]) 
+done
+
+
+lemma Crypt_used_imp_L_used:
+     "[| Crypt (priK TTP) {|F, A, B, L, K|} \<in> used evs; evs \<in> zg |]
+      ==> L \<in> used evs"
+apply (erule rev_mp)
+apply (erule zg.induct, auto)
+txt{*Fake*}
+apply (blast dest!: Fake_parts_sing_imp_Un)
+txt{*ZG2: freshness*}
+apply (blast dest: parts.Body) 
+done
+
+
+text{*Fairness for @{term A}: if @{term con_K} and @{term NRO} exist, 
+then @{term A} holds NRR.  @{term A} must be uncompromised, but there is no
+assumption about @{term B}.*}
+theorem A_fairness_NRO:
+     "[|con_K \<in> used evs;
+        NRO \<in> parts (spies evs);
+        con_K = Crypt (priK TTP)
+                      {|Number f_con, Agent A, Agent B, Nonce L, Key K|};
+        NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, Crypt K M|};
+        NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, Crypt K M|};
+        A \<notin> bad;  evs \<in> zg |]
+    ==> Gets A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs"
+apply clarify
+apply (erule rev_mp)
+apply (erule rev_mp)
+apply (erule zg.induct)
+apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
+   txt{*Fake*}
+   apply (simp add: parts_insert_knows_A) 
+   apply (blast dest: Fake_parts_sing_imp_Un) 
+  txt{*ZG1*}
+  apply (blast dest: Crypt_used_imp_L_used) 
+ txt{*ZG2*}
+ apply (blast dest: parts_cut)
+txt{*ZG4*}
+apply (blast intro: sub_K_implies_NRR [OF _ _ refl] 
+             dest: Gets_imp_knows_Spy [THEN parts.Inj])
+done
+
+text{*Fairness for @{term B}: NRR exists at all, then @{term B} holds NRO.
+@{term B} must be uncompromised, but there is no assumption about @{term
+A}. *}
+theorem B_fairness_NRR:
+     "[|NRR \<in> used evs;
+        NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
+        NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
+        B \<notin> bad; evs \<in> zg |]
+    ==> Gets B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs"
+apply clarify
+apply (erule rev_mp)
+apply (erule zg.induct)
+apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
+txt{*Fake*}
+apply (blast dest!: Fake_parts_sing_imp_Un)
+txt{*ZG2*}
+apply (blast dest: parts_cut)
+done
+
+
+text{*If @{term con_K} exists at all, then @{term B} can get it, by @{text
+con_K_authenticity}.  Cannot conclude that also NRO is available to @{term B},
+because if @{term A} were unfair, @{term A} could build message 3 without
+building message 1, which contains NRO. *}
+
+end
diff -r 7195c9b0423f -r 2e31b8cc8788 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Aug 08 15:05:11 2003 +0200
+++ b/src/HOL/IsaMakefile	Tue Aug 12 13:35:03 2003 +0200
@@ -361,9 +361,9 @@
   Auth/OtwayRees_Bad.thy Auth/Public.thy Auth/ROOT.ML \
   Auth/Recur.thy Auth/Shared.thy \
   Auth/TLS.thy Auth/WooLam.thy \
-  Auth/Kerberos_BAN.thy \
-  Auth/KerberosIV.ML Auth/KerberosIV.thy \
+  Auth/Kerberos_BAN.thy Auth/KerberosIV.ML Auth/KerberosIV.thy \
   Auth/Yahalom.thy Auth/Yahalom2.thy Auth/Yahalom_Bad.thy \
+  Auth/ZhouGollmann.thy \
   Auth/Guard/Analz.thy Auth/Guard/Extensions.thy Auth/Guard/GuardK.thy \
   Auth/Guard/Guard_Public.thy Auth/Guard/Guard_Shared.thy \
   Auth/Guard/Guard.thy Auth/Guard/List_Msg.thy \