# HG changeset patch
# User paulson
# Date 1065085024 -7200
# Node ID db95d1c2f51b33107a48c026eeba70afeac35e0e
# Parent  9f5679e97eac2e1da74b726e05766f8d43440cea
removal of junk and improvement of the document

diff -r 9f5679e97eac -r db95d1c2f51b src/HOL/SET-Protocol/Cardholder_Registration.thy
--- a/src/HOL/SET-Protocol/Cardholder_Registration.thy	Wed Oct 01 11:02:36 2003 +0200
+++ b/src/HOL/SET-Protocol/Cardholder_Registration.thy	Thu Oct 02 10:57:04 2003 +0200
@@ -348,11 +348,8 @@
 apply (erule set_cr.induct)
 apply (frule_tac [8] Gets_certificate_valid)
 apply (frule_tac [6] Gets_certificate_valid, simp_all)
-txt{*Fake*}
-apply (force dest!: usedI keysFor_parts_insert)
-txt{*Others*}
-apply blast
-apply auto
+apply (force dest!: usedI keysFor_parts_insert) --{*Fake*}
+apply (blast,auto)  --{*Others*}
 done
 
 
@@ -389,6 +386,7 @@
 by (blast intro: Crypt_parts_imp_used)
 
 
+(*<*) 
 subsection{*Messages signed by CA*}
 
 text{*Message @{text SET_CR2}: C can check CA's signature if he has received
@@ -459,7 +457,7 @@
       ==> \<exists>Y K. Says (CA i) C (Crypt K {|sign (priSK (CA i))
                     {|Agent C, Nonce NC3, Agent (CA i), Nonce NonceCCA|}, Y|}) \<in> set evs"
 by (blast dest!: certificate_valid_pubSK intro!: CA_Says_6_lemma)
-
+(*>*)
 
 
 subsection{*Useful lemmas *}
@@ -574,10 +572,8 @@
               analz_image_priEK disj_simps)
   --{*46 seconds on a 1.8GHz machine*}
 apply spy_analz
-txt{*3*}
-apply blast
-txt{*5*}
-apply blast
+apply blast  --{*3*}
+apply blast  --{*5*}
 done
 
 text{*The remaining quantifiers seem to be essential.
@@ -601,8 +597,7 @@
               DK_fresh_not_KeyCryptKey
               analz_image_priEK)
   --{*13 seconds on a 1.8GHz machine*}
-txt{*Fake*}
-apply spy_analz
+apply spy_analz  --{*Fake*}
 apply (auto intro: analz_into_parts [THEN usedI] in_parts_Says_imp_used)
 done
 
@@ -691,8 +686,7 @@
      "[|cardSK \<notin> symKeys;  \<forall>C. cardSK \<noteq> priEK C;  evs \<in> set_cr|] ==>
       Key cardSK \<notin> analz (knows Spy evs) --> ~ KeyCryptNonce cardSK N evs"
 apply (erule set_cr.induct, analz_mono_contra, simp_all)
-txt{*6*}
-apply (blast dest: not_KeyCryptKey_cardSK)
+apply (blast dest: not_KeyCryptKey_cardSK)  --{*6*}
 done
 
 subsubsection{*Lemmas for message 5 and 6:
@@ -746,20 +740,18 @@
               DK_fresh_not_KeyCryptNonce K_fresh_not_KeyCryptKey
               ball_conj_distrib analz_image_priEK)
   --{*71 seconds on a 1.8GHz machine*}
-txt{*Fake*}
-apply spy_analz
-txt{*3*}
-apply blast
-txt{*5*}
-apply blast
-txt{*6*}
-txt{*cardSK compromised?*}
+apply spy_analz  --{*Fake*}
+apply blast  --{*3*}
+apply blast  --{*5*}
+txt{*Message 6*}
 apply (force del: allE ballE impCE simp add: symKey_compromise)
+  --{*cardSK compromised*}
 txt{*Simplify again--necessary because the previous simplification introduces
   some logical connectives*}
-by (force del: allE ballE impCE
+apply (force del: allE ballE impCE
           simp del: image_insert image_Un imp_disjL
           simp add: analz_image_keys_simps symKey_compromise)
+done
 
 
 subsection{*Secrecy of CardSecret: the Cardholder's secret*}
@@ -824,22 +816,14 @@
               ball_conj_distrib Nonce_compromise symKey_compromise
               analz_image_priEK)
   --{*12 seconds on a 1.8GHz machine*}
-txt{*Fake*}
-apply spy_analz
+apply spy_analz  --{*Fake*}
 apply (simp_all (no_asm_simp))
-txt{*1*}
-apply blast
-txt{*2*}
-apply (blast dest!: Gets_imp_knows_Spy [THEN analz.Inj])
-txt{*3*}
-apply blast
-txt{*4*}
-apply (blast dest: NC2_not_CardSecret Gets_imp_knows_Spy [THEN analz.Inj] analz_symKeys_Decrypt)
-txt{*5*}
-apply blast
-txt{*6*}
-apply (blast dest: KC2_secrecy)
-apply (blast dest: KC2_secrecy)
+apply blast  --{*1*}
+apply (blast dest!: Gets_imp_knows_Spy [THEN analz.Inj])  --{*2*}
+apply blast  --{*3*}
+apply (blast dest: NC2_not_CardSecret Gets_imp_knows_Spy [THEN analz.Inj] analz_symKeys_Decrypt)  --{*4*}
+apply blast  --{*5*}
+apply (blast dest: KC2_secrecy)+  --{*Message 6: two cases*}
 done
 
 
@@ -898,21 +882,13 @@
               ball_conj_distrib Nonce_compromise symKey_compromise
               analz_image_priEK)
   --{*15 seconds on a 1.8GHz machine*}
-txt{*Fake*}
-apply spy_analz
-txt{*1*}
-apply blast
-txt{*2*}
-apply (blast dest!: Gets_imp_knows_Spy [THEN analz.Inj])
-txt{*3*}
-apply blast
-txt{*4*}
-apply (blast dest: NC2_not_NonceCCA)
-txt{*5*}
-apply blast
-txt{*6*}
-apply (blast dest: KC2_secrecy)
-apply (blast dest: KC2_secrecy)
+apply spy_analz  --{*Fake*}
+apply blast  --{*1*}
+apply (blast dest!: Gets_imp_knows_Spy [THEN analz.Inj])  --{*2*}
+apply blast  --{*3*}
+apply (blast dest: NC2_not_NonceCCA)  --{*4*}
+apply blast  --{*5*}
+apply (blast dest: KC2_secrecy)+  --{*Message 6: two cases*}
 done
 
 
@@ -974,8 +950,7 @@
               notin_image_iff analz_image_priEK)
   --{*33 seconds on a 1.8GHz machine*}
 apply spy_analz
-txt{*6*}
-apply (simp add: insert_absorb)
+apply (simp add: insert_absorb)  --{*6*}
 done
 
 lemma analz_insert_pan:
@@ -1005,14 +980,10 @@
          add: analz_image_keys_simps analz_insert_pan analz_image_pan
               notin_image_iff analz_image_priEK)
   --{*18 seconds on a 1.8GHz machine*}
-txt{*fake*}
-apply spy_analz
-txt{*3*}
-apply blast
-txt{*5*}
-apply blast
-txt{*6*}
-apply (simp (no_asm_simp) add: insert_absorb)
+apply spy_analz  --{*fake*}
+apply blast  --{*3*}
+apply blast  --{*5*}
+apply (simp (no_asm_simp) add: insert_absorb)  --{*6*}
 done
 
 
@@ -1052,6 +1023,7 @@
 done
 
 
+(*<*)
 text{*UNUSED unicity result*}
 lemma unique_KC1:
      "[|Says C B {|Crypt KC1 X, Crypt EK {|Key KC1, Y|}|}
@@ -1073,6 +1045,8 @@
 apply (erule rev_mp)
 apply (erule set_cr.induct, auto)
 done
+(*>*)
+
 
 text{*Cannot show cardSK to be secret because it isn't assumed to be fresh
   it could be a previously compromised cardSK [e.g. involving a bad CA]*}
diff -r 9f5679e97eac -r db95d1c2f51b src/HOL/SET-Protocol/EventSET.thy
--- a/src/HOL/SET-Protocol/EventSET.thy	Wed Oct 01 11:02:36 2003 +0200
+++ b/src/HOL/SET-Protocol/EventSET.thy	Thu Oct 02 10:57:04 2003 +0200
@@ -131,75 +131,6 @@
      parts.Body [THEN revcut_rl, standard]
 
 
-subsection{*Lemmas About Agents' Knowledge*}
-
-lemma knows_Says: "knows A (Says A B X # evs) = insert X (knows A evs)"
-by auto
-
-lemma knows_Notes: "knows A (Notes A X # evs) = insert X (knows A evs)"
-by auto
-
-lemma knows_Gets:
-     "A \<noteq> Spy --> knows A (Gets A X # evs) = insert X (knows A evs)"
-by auto
-
-lemma knows_subset_knows_Says: "knows A evs <= knows A (Says A B X # evs)"
-by auto
-
-lemma knows_subset_knows_Notes: "knows A evs <= knows A (Notes A X # evs)"
-by auto
-
-lemma knows_subset_knows_Gets: "knows A evs <= knows A (Gets A X # evs)"
-by auto
-
-(*Agents know what they say*)
-lemma Says_imp_knows [rule_format]:
-     "Says A B X \<in> set evs --> X \<in> knows A evs"
-apply (induct_tac "evs")
-apply (auto split: event.split) 
-done
-
-(*Agents know what they note*)
-lemma Notes_imp_knows [rule_format]:
-     "Notes A X \<in> set evs --> X \<in> knows A evs"
-apply (induct_tac "evs")
-apply (auto split: event.split) 
-done
-
-(*Agents know what they receive*)
-lemma Gets_imp_knows_agents [rule_format]:
-     "A \<noteq> Spy --> Gets A X \<in> set evs --> X \<in> knows A evs"
-apply (induct_tac "evs")
-apply (auto split: event.split) 
-done
-
-
-(*What agents DIFFERENT FROM Spy know
-  was either said, or noted, or got, or known initially*)
-lemma knows_imp_Says_Gets_Notes_initState [rule_format]:
-     "[| X \<in> knows A evs; A \<noteq> Spy |] ==>
-  \<exists>B. Says A B X \<in> set evs |
-               Gets A X \<in> set evs |
-               Notes A X \<in> set evs |
-               X \<in> initState A"
-apply (erule rev_mp) 
-apply (induct_tac "evs")
-apply (auto split: event.split) 
-done
-
-(*What the Spy knows -- for the time being --
-  was either said or noted, or known initially*)
-lemma knows_Spy_imp_Says_Notes_initState [rule_format]:
-     "[| X \<in> knows Spy evs |] ==>
-   \<exists>A B. Says A B X \<in> set evs |
-                  Notes A X \<in> set evs |
-                  X \<in> initState Spy"
-apply (erule rev_mp) 
-apply (induct_tac "evs")
-apply (auto split: event.split) 
-done
-
-
 subsection{*The Function @{term used}*}
 
 lemma parts_knows_Spy_subset_used: "parts (knows Spy evs) <= used evs"
@@ -225,11 +156,6 @@
 lemma used_Gets [simp]: "used (Gets A X # evs) = used evs"
 by auto
 
-lemma used_nil_subset: "used [] <= used evs"
-apply auto
-apply (rule initState_into_used, auto)
-done
-
 
 lemma Notes_imp_parts_subset_used [rule_format]:
      "Notes A X \<in> set evs --> parts {X} <= used evs"
@@ -255,11 +181,9 @@
 {*
 val analz_mono_contra_tac = 
   let val analz_impI = inst "P" "?Y \<notin> analz (knows Spy ?evs)" impI
-  in
-    rtac analz_impI THEN' 
-    REPEAT1 o 
-      (dresolve_tac (thms"analz_mono_contra"))
-    THEN' mp_tac
+  in rtac analz_impI THEN' 
+     REPEAT1 o (dresolve_tac (thms"analz_mono_contra")) THEN'
+     mp_tac
   end
 *}
 
diff -r 9f5679e97eac -r db95d1c2f51b src/HOL/SET-Protocol/Merchant_Registration.thy
--- a/src/HOL/SET-Protocol/Merchant_Registration.thy	Wed Oct 01 11:02:36 2003 +0200
+++ b/src/HOL/SET-Protocol/Merchant_Registration.thy	Thu Oct 02 10:57:04 2003 +0200
@@ -189,14 +189,10 @@
       ==> Key K \<notin> used evs --> K \<in> symKeys -->
           K \<notin> keysFor (parts (knows Spy evs))"
 apply (erule set_mr.induct, simp_all)
-txt{*Fake*}
-apply (force dest!: usedI keysFor_parts_insert)
-txt{*Message 2*}
-apply force
-txt{*Message 3*}
-apply (blast dest: Gets_certificate_valid)
-txt{*Message 4*}
-apply force
+apply (force dest!: usedI keysFor_parts_insert)  --{*Fake*}
+apply force  --{*Message 2*}
+apply (blast dest: Gets_certificate_valid)  --{*Message 3*}
+apply force  --{*Message 4*}
 done
 
 
@@ -294,10 +290,8 @@
               analz_knows_absorb2 analz_Key_image_insert_eq notin_image_iff
               Spy_analz_private_Key analz_image_priEK)
   --{*23 seconds on a 1.8GHz machine*}
-txt{*Fake*}
-apply spy_analz
-txt{*Message 3*}
-apply auto
+apply spy_analz  --{*Fake*}
+apply auto  --{*Message 3*}
 done
 
 lemma symKey_secrecy [rule_format]:
@@ -315,12 +309,9 @@
               analz_knows_absorb2 analz_Key_image_insert_eq
               symKey_compromise notin_image_iff Spy_analz_private_Key
               analz_image_priEK)
-txt{*Fake*}
-apply spy_analz
-txt{*Message 1*}
-apply force
-txt{*Message 3*}
-apply (auto intro: analz_into_parts [THEN usedI] in_parts_Says_imp_used)
+apply spy_analz  --{*Fake*}
+apply force  --{*Message 1*}
+apply (auto intro: analz_into_parts [THEN usedI] in_parts_Says_imp_used)  --{*Message 3*}
 done
 
 subsection{*Unicity *}
diff -r 9f5679e97eac -r db95d1c2f51b src/HOL/SET-Protocol/MessageSET.thy
--- a/src/HOL/SET-Protocol/MessageSET.thy	Wed Oct 01 11:02:36 2003 +0200
+++ b/src/HOL/SET-Protocol/MessageSET.thy	Thu Oct 02 10:57:04 2003 +0200
@@ -829,86 +829,16 @@
 
 
 subsection{*Tactics useful for many protocol proofs*}
+(*<*)
 ML
 {*
-val invKey = thm "invKey"
-val keysFor_def = thm "keysFor_def"
-val symKeys_def = thm "symKeys_def"
-val parts_mono = thm "parts_mono";
-val analz_mono = thm "analz_mono";
-val Key_image_eq = thm "Key_image_eq";
-val Nonce_Key_image_eq = thm "Nonce_Key_image_eq";
-val keysFor_Un = thm "keysFor_Un";
-val keysFor_mono = thm "keysFor_mono";
-val keysFor_image_Key = thm "keysFor_image_Key";
-val Crypt_imp_invKey_keysFor = thm "Crypt_imp_invKey_keysFor";
-val MPair_parts = thm "MPair_parts";
-val parts_increasing = thm "parts_increasing";
-val parts_insertI = thm "parts_insertI";
-val parts_empty = thm "parts_empty";
-val parts_emptyE = thm "parts_emptyE";
-val parts_singleton = thm "parts_singleton";
-val parts_Un_subset1 = thm "parts_Un_subset1";
-val parts_Un_subset2 = thm "parts_Un_subset2";
-val parts_insert = thm "parts_insert";
-val parts_insert2 = thm "parts_insert2";
-val parts_UN_subset1 = thm "parts_UN_subset1";
-val parts_UN_subset2 = thm "parts_UN_subset2";
-val parts_UN = thm "parts_UN";
-val parts_insert_subset = thm "parts_insert_subset";
-val parts_partsD = thm "parts_partsD";
-val parts_trans = thm "parts_trans";
-val parts_cut = thm "parts_cut";
-val parts_cut_eq = thm "parts_cut_eq";
-val parts_insert_eq_I = thm "parts_insert_eq_I";
-val parts_image_Key = thm "parts_image_Key";
-val MPair_analz = thm "MPair_analz";
 val analz_increasing = thm "analz_increasing";
 val analz_subset_parts = thm "analz_subset_parts";
-val not_parts_not_analz = thm "not_parts_not_analz";
 val parts_analz = thm "parts_analz";
 val analz_parts = thm "analz_parts";
 val analz_insertI = thm "analz_insertI";
-val analz_empty = thm "analz_empty";
-val analz_Un = thm "analz_Un";
-val analz_insert_Crypt_subset = thm "analz_insert_Crypt_subset";
-val analz_image_Key = thm "analz_image_Key";
-val analz_analzD = thm "analz_analzD";
-val analz_trans = thm "analz_trans";
-val analz_cut = thm "analz_cut";
-val analz_insert_eq = thm "analz_insert_eq";
-val analz_subset_cong = thm "analz_subset_cong";
-val analz_cong = thm "analz_cong";
-val analz_insert_cong = thm "analz_insert_cong";
-val analz_trivial = thm "analz_trivial";
-val analz_UN_analz = thm "analz_UN_analz";
-val synth_mono = thm "synth_mono";
-val synth_increasing = thm "synth_increasing";
-val synth_Un = thm "synth_Un";
-val synth_insert = thm "synth_insert";
-val synth_synthD = thm "synth_synthD";
-val synth_trans = thm "synth_trans";
-val synth_cut = thm "synth_cut";
-val Agent_synth = thm "Agent_synth";
-val Number_synth = thm "Number_synth";
-val Nonce_synth_eq = thm "Nonce_synth_eq";
-val Key_synth_eq = thm "Key_synth_eq";
-val Crypt_synth_eq = thm "Crypt_synth_eq";
-val keysFor_synth = thm "keysFor_synth";
-val parts_synth = thm "parts_synth";
-val analz_analz_Un = thm "analz_analz_Un";
-val analz_synth_Un = thm "analz_synth_Un";
-val analz_synth = thm "analz_synth";
-val parts_insert_subset_Un = thm "parts_insert_subset_Un";
 val Fake_parts_insert = thm "Fake_parts_insert";
 val Fake_analz_insert = thm "Fake_analz_insert";
-val analz_conj_parts = thm "analz_conj_parts";
-val analz_disj_parts = thm "analz_disj_parts";
-val MPair_synth_analz = thm "MPair_synth_analz";
-val Crypt_synth_analz = thm "Crypt_synth_analz";
-val Hash_synth_analz = thm "Hash_synth_analz";
-val pushes = thms "pushes";
-
 
 (*Prove base case (subgoal i) and simplify others.  A typical base case
   concerns  Crypt K X \<notin> Key`shrK`bad  and cannot be proved by rewriting
@@ -955,6 +885,8 @@
 
 fun spy_analz_tac i = gen_spy_analz_tac (claset(), simpset()) i
 *}
+(*>*)
+
 
 (*By default only o_apply is built-in.  But in the presence of eta-expansion
   this means that some terms displayed as (f o g) will be rewritten, and others
diff -r 9f5679e97eac -r db95d1c2f51b src/HOL/SET-Protocol/PublicSET.thy
--- a/src/HOL/SET-Protocol/PublicSET.thy	Wed Oct 01 11:02:36 2003 +0200
+++ b/src/HOL/SET-Protocol/PublicSET.thy	Thu Oct 02 10:57:04 2003 +0200
@@ -40,6 +40,7 @@
 specification (publicKey)
   injective_publicKey:
     "publicKey b A = publicKey c A' ==> b=c & A=A'"
+(*<*)
    apply (rule exI [of _ "%b A. 2 * nat_of_agent A + (if b then 1 else 0)"]) 
    apply (auto simp add: inj_on_def inj_nat_of_agent [THEN inj_eq] split: agent.split) 
    apply (drule_tac f="%x. x mod 2" in arg_cong, simp add: mod_Suc)+
@@ -47,7 +48,7 @@
    apply presburger+
 *)
    done                       
-
+(*>*)
 
 axioms
   (*No private key equals any public key (essential to ensure that private
@@ -68,7 +69,7 @@
    RCA (has already certified and therefore) knows all CAs public keys; 
    Spy knows all keys of all bad agents.*}
 primrec    
-
+(*<*)
   initState_CA:
     "initState (CA i)  =
        (if i=0 then Key ` ({priEK RCA, priSK RCA} Un
@@ -94,7 +95,7 @@
        {Key (priEK (PG i)), Key (priSK (PG i)),
 	Key (pubEK (PG i)), Key (pubSK (PG i)),
 	Key (pubEK RCA), Key (pubSK RCA)}"
-
+(*>*)
   initState_Spy:
     "initState Spy = Key ` (invKey ` pubEK ` bad Un
 			    invKey ` pubSK ` bad Un
@@ -108,9 +109,11 @@
 specification (pan)
   inj_pan: "inj pan"
   --{*No two agents have the same PAN*}
+(*<*)
    apply (rule exI [of _ "nat_of_agent"]) 
    apply (simp add: inj_on_def inj_nat_of_agent [THEN inj_eq]) 
    done
+(*>*)
 
 declare inj_pan [THEN inj_eq, iff]
 
@@ -274,11 +277,10 @@
 lemma keysFor_parts_insert:
      "[| K \<in> keysFor (parts (insert X H));  X \<in> synth (analz H) |]  
       ==> K \<in> keysFor (parts H) | Key (invKey K) \<in> parts H"
-apply (force dest!: 
+by (force dest!: 
          parts_insert_subset_Un [THEN keysFor_mono, THEN [2] rev_subsetD]
          analz_subset_parts [THEN keysFor_mono, THEN [2] rev_subsetD] 
             intro: analz_into_parts)
-done
 
 lemma Crypt_imp_keysFor [intro]:
      "[|K \<in> symKeys; Crypt K X \<in> H|] ==> K \<in> keysFor H"