# HG changeset patch
# User paulson
# Date 1084351241 -7200
# Node ID 36582c356db7a00e2cd714e81ccc84ce95456bd0
# Parent  c8e1937110c2fc58397c2bde203e15d2682a22a3
simpilified and strengthened proofs

diff -r c8e1937110c2 -r 36582c356db7 src/HOL/Auth/ZhouGollmann.thy
--- a/src/HOL/Auth/ZhouGollmann.thy	Wed May 12 10:00:56 2004 +0200
+++ b/src/HOL/Auth/ZhouGollmann.thy	Wed May 12 10:40:41 2004 +0200
@@ -16,7 +16,7 @@
   TTP :: agent
 
 translations
-  "TTP" == "Server "
+  "TTP" == " Server "
 
 syntax
   f_sub :: nat
@@ -25,10 +25,10 @@
   f_con :: nat
 
 translations
-  "f_sub" == "5"
-  "f_nro" == "2"
-  "f_nrr" == "3"
-  "f_con" == "4"
+  "f_sub" == " 5 "
+  "f_nro" == " 2 "
+  "f_nrr" == " 3 "
+  "f_con" == " 4 "
 
 
 constdefs
@@ -172,16 +172,16 @@
 by auto 
 
 
-subsection{*About NRO*}
+subsection{*About NRO: Validity for @{term B}*}
 
 text{*Below we prove that if @{term NRO} exists then @{term A} definitely
-sent it, provided @{term A} is not broken.  *}
+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 |]
+     "[|NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
+        NRO \<in> parts (spies evs);
+        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)
@@ -189,85 +189,62 @@
 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 (force intro!: exI)
-txt{*ZG4*}
-apply (auto ); 
+lemma NRO_sender:
+     "[|Says A' B {|n, b, l, C, Crypt (priK A) X|} \<in> set evs; evs \<in> zg|]
+    ==> A' \<in> {A,Spy}"
+apply (erule rev_mp)  
+apply (erule zg.induct, simp_all)
 done
 
+text{*Holds also for @{term "A = Spy"}!*}
 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)
+     "[|Says A' B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs;
+        NRO = Crypt (priK A) {|Number f_nro, Agent B, Nonce L, C|};
+        A \<notin> broken;  evs \<in> zg |]
+     ==> Says A B {|Number f_nro, Agent B, Nonce L, C, NRO|} \<in> set evs"
+apply clarify 
+apply (frule NRO_sender, auto)
+txt{*We are left with the case where @{term "A' = Spy"} and  @{term "A' \<noteq> A"},
+  i.e. @{term "A \<notin> bad"}, when we can apply @{text NRO_authenticity_good}.*}
+ apply (blast dest: NRO_authenticity_good [OF refl])
 done
 
 
-subsection{*About NRR*}
+subsection{*About NRR: Validity for @{term A}*}
 
 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 |]
+     "[|NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
+        NRR \<in> parts (spies evs);
+        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 (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)
+lemma NRR_sender:
+     "[|Says B' A {|n, a, l, Crypt (priK B) X|} \<in> set evs; evs \<in> zg|]
+    ==> B' \<in> {B,Spy}"
+apply (erule rev_mp)  
+apply (erule zg.induct, simp_all)
 done
 
+text{*Holds also for @{term "B = Spy"}!*}
 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)
+     "[|Says B' A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs;
+        NRR = Crypt (priK B) {|Number f_nrr, Agent A, Nonce L, C|};
+        B \<notin> broken; evs \<in> zg|]
+    ==> Says B A {|Number f_nrr, Agent A, Nonce L, NRR|} \<in> set evs"
+apply clarify 
+apply (frule NRR_sender, auto)
+txt{*We are left with the case where @{term "B' = Spy"} and  @{term "B' \<noteq> B"},
+  i.e. @{term "B \<notin> bad"}, when we can apply @{text NRR_authenticity_good}.*}
+ apply (blast dest: NRR_authenticity_good [OF refl])
 done
 
 
@@ -278,10 +255,11 @@
 
 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 |]
+     "[|sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
+        sub_K \<in> parts (spies evs);
+        A \<notin> bad;  evs \<in> zg |]
      ==> Says A TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_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)
@@ -289,37 +267,28 @@
 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)
+lemma sub_K_sender:
+     "[|Says A' TTP {|n, b, l, k, Crypt (priK A) X|} \<in> set evs;  evs \<in> zg|]
+    ==> A' \<in> {A,Spy}"
+apply (erule rev_mp)  
+apply (erule zg.induct, simp_all)
 done
 
+text{*Holds also for @{term "A = Spy"}!*}
 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)
+     "[|Says A' TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs;
+        sub_K = Crypt (priK A) {|Number f_sub, Agent B, Nonce L, Key K|};
+        A \<notin> broken;  evs \<in> zg |]
+     ==> Says A TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs"
+apply clarify 
+apply (frule sub_K_sender, auto)
+txt{*We are left with the case where @{term "A' = Spy"} and  @{term "A' \<noteq> A"},
+  i.e. @{term "A \<notin> bad"}, when we can apply @{text sub_K_authenticity_good}.*}
+ apply (blast dest: sub_K_authenticity_good [OF refl])
 done
 
 
+
 subsection{*Proofs About @{term con_K}*}
 
 text{*Below we prove that if @{term con_K} exists, then @{term TTP} has it,
@@ -339,7 +308,7 @@
 apply (frule_tac [5] ZG2_msg_in_parts_spies, simp_all)
 txt{*Fake*}
 apply (blast dest!: Fake_parts_sing_imp_Un)
-txt{*ZG2*}
+txt{*ZG2*} 
 apply (blast dest: parts_cut)
 done
 
@@ -351,8 +320,15 @@
            \<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)
+     ==> Says A TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_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{*ZG4*}
+apply (clarify dest!: Gets_imp_Says) 
+apply (rule sub_K_authenticity, auto) 
+done
 
 text{*If @{term con_K} exists, then @{term A} sent @{term sub_K}.  We again
    assume that @{term A} is not broken. *}
@@ -361,8 +337,8 @@
         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}"
+        A \<notin> broken; evs \<in> zg|]
+     ==> Says A TTP {|Number f_sub, Agent B, Nonce L, Key K, sub_K|} \<in> set evs"
 by (blast dest: con_K_authenticity Notes_TTP_imp_Says_A)
 
 
@@ -393,11 +369,11 @@
 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 = 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|};
+         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
@@ -409,7 +385,7 @@
 apply blast 
 txt{*ZG1: freshness*}
 apply (blast dest: parts.Body) 
-txt{*ZG3*}
+txt{*ZG3*} 
 apply (blast dest: A_unicity [OF refl]) 
 done
 
@@ -450,8 +426,8 @@
   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] 
+txt{*ZG4*} 
+apply (blast intro: sub_K_implies_NRR [OF refl] 
              dest: Gets_imp_knows_Spy [THEN parts.Inj])
 done