Addition of the Hash constructor
Strengthening spy_analz_tac

--- a/src/HOL/Auth/Message.ML	Tue Dec 10 15:13:53 1996 +0100
+++ b/src/HOL/Auth/Message.ML	Fri Dec 13 10:17:35 1996 +0100
@@ -30,6 +30,7 @@
 
 open Message;
 
+AddIffs (msg.inject);
 
 (** Inverse of keys **)
 
@@ -74,6 +75,10 @@
 by (fast_tac (!claset addss (!simpset)) 1);
 qed "keysFor_insert_Key";
 
+goalw thy [keysFor_def] "keysFor (insert (Hash X) H) = keysFor H";
+by (fast_tac (!claset addss (!simpset)) 1);
+qed "keysFor_insert_Hash";
+
 goalw thy [keysFor_def] "keysFor (insert {|X,Y|} H) = keysFor H";
 by (fast_tac (!claset addss (!simpset)) 1);
 qed "keysFor_insert_MPair";
@@ -84,9 +89,8 @@
 qed "keysFor_insert_Crypt";
 
 Addsimps [keysFor_empty, keysFor_Un, keysFor_UN, 
-          keysFor_insert_Agent, keysFor_insert_Nonce,
-          keysFor_insert_Key, keysFor_insert_MPair,
-          keysFor_insert_Crypt];
+          keysFor_insert_Agent, keysFor_insert_Nonce, keysFor_insert_Key, 
+	  keysFor_insert_Hash, keysFor_insert_MPair, keysFor_insert_Crypt];
 
 goalw thy [keysFor_def] "!!H. Crypt K X : H ==> invKey K : keysFor H";
 by (Fast_tac 1);
@@ -123,6 +127,8 @@
 by (REPEAT (ares_tac basic_monos 1));
 qed "parts_mono";
 
+val parts_insertI = impOfSubs (subset_insertI RS parts_mono);
+
 goal thy "parts{} = {}";
 by (Step_tac 1);
 by (etac parts.induct 1);
@@ -214,16 +220,16 @@
 qed "parts_trans";
 
 (*Cut*)
-goal thy "!!H. [| Y: parts (insert X H);  X: parts H |] ==> Y: parts H";
+goal thy "!!H. [| Y: parts (insert X G);  X: parts H |] \
+\              ==> Y: parts (G Un H)";
 by (etac parts_trans 1);
-by (Fast_tac 1);
+by (Auto_tac());
 qed "parts_cut";
 
-val parts_insertI = impOfSubs (subset_insertI RS parts_mono);
-
 goal thy "!!H. X: parts H ==> parts (insert X H) = parts H";
-by (fast_tac (!claset addSEs [parts_cut]
-                      addIs  [parts_insertI]) 1);
+by (fast_tac (!claset addSDs [parts_cut]
+                      addIs  [parts_insertI] 
+                      addss (!simpset)) 1);
 qed "parts_cut_eq";
 
 Addsimps [parts_cut_eq];
@@ -231,29 +237,27 @@
 
 (** Rewrite rules for pulling out atomic messages **)
 
+fun parts_tac i =
+  EVERY [rtac ([subsetI, parts_insert_subset] MRS equalityI) i,
+	 etac parts.induct i,
+	 REPEAT (fast_tac (!claset addss (!simpset)) i)];
+
 goal thy "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)";
-by (rtac (parts_insert_subset RSN (2, equalityI)) 1);
-by (rtac subsetI 1);
-by (etac parts.induct 1);
-(*Simplification breaks up equalities between messages;
-  how to make it work for fast_tac??*)
-by (ALLGOALS (fast_tac (!claset addss (!simpset))));
+by (parts_tac 1);
 qed "parts_insert_Agent";
 
 goal thy "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)";
-by (rtac (parts_insert_subset RSN (2, equalityI)) 1);
-by (rtac subsetI 1);
-by (etac parts.induct 1);
-by (ALLGOALS (fast_tac (!claset addss (!simpset))));
+by (parts_tac 1);
 qed "parts_insert_Nonce";
 
 goal thy "parts (insert (Key K) H) = insert (Key K) (parts H)";
-by (rtac (parts_insert_subset RSN (2, equalityI)) 1);
-by (rtac subsetI 1);
-by (etac parts.induct 1);
-by (ALLGOALS (fast_tac (!claset addss (!simpset))));
+by (parts_tac 1);
 qed "parts_insert_Key";
 
+goal thy "parts (insert (Hash X) H) = insert (Hash X) (parts H)";
+by (parts_tac 1);
+qed "parts_insert_Hash";
+
 goal thy "parts (insert (Crypt K X) H) = \
 \         insert (Crypt K X) (parts (insert X H))";
 by (rtac equalityI 1);
@@ -274,8 +278,8 @@
 by (ALLGOALS (best_tac (!claset addIs [parts.Fst, parts.Snd])));
 qed "parts_insert_MPair";
 
-Addsimps [parts_insert_Agent, parts_insert_Nonce, 
-          parts_insert_Key, parts_insert_Crypt, parts_insert_MPair];
+Addsimps [parts_insert_Agent, parts_insert_Nonce, parts_insert_Key, 
+          parts_insert_Hash, parts_insert_Crypt, parts_insert_MPair];
 
 
 goal thy "parts (Key``N) = Key``N";
@@ -338,6 +342,8 @@
 by (REPEAT (ares_tac basic_monos 1));
 qed "analz_mono";
 
+val analz_insertI = impOfSubs (subset_insertI RS analz_mono);
+
 (** General equational properties **)
 
 goal thy "analz{} = {}";
@@ -359,30 +365,28 @@
 
 (** Rewrite rules for pulling out atomic messages **)
 
+fun analz_tac i =
+  EVERY [rtac ([subsetI, analz_insert] MRS equalityI) i,
+	 etac analz.induct i,
+	 REPEAT (fast_tac (!claset addss (!simpset)) i)];
+
 goal thy "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)";
-by (rtac (analz_insert RSN (2, equalityI)) 1);
-by (rtac subsetI 1);
-by (etac analz.induct 1);
-(*Simplification breaks up equalities between messages;
-  how to make it work for fast_tac??*)
-by (ALLGOALS (fast_tac (!claset addss (!simpset))));
+by (analz_tac 1);
 qed "analz_insert_Agent";
 
 goal thy "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)";
-by (rtac (analz_insert RSN (2, equalityI)) 1);
-by (rtac subsetI 1);
-by (etac analz.induct 1);
-by (ALLGOALS (fast_tac (!claset addss (!simpset))));
+by (analz_tac 1);
 qed "analz_insert_Nonce";
 
+goal thy "analz (insert (Hash X) H) = insert (Hash X) (analz H)";
+by (analz_tac 1);
+qed "analz_insert_Hash";
+
 (*Can only pull out Keys if they are not needed to decrypt the rest*)
 goalw thy [keysFor_def]
     "!!K. K ~: keysFor (analz H) ==>  \
 \         analz (insert (Key K) H) = insert (Key K) (analz H)";
-by (rtac (analz_insert RSN (2, equalityI)) 1);
-by (rtac subsetI 1);
-by (etac analz.induct 1);
-by (ALLGOALS (fast_tac (!claset addss (!simpset))));
+by (analz_tac 1);
 qed "analz_insert_Key";
 
 goal thy "analz (insert {|X,Y|} H) = \
@@ -400,10 +404,7 @@
 goal thy "!!H. Key (invKey K) ~: analz H ==>  \
 \              analz (insert (Crypt K X) H) = \
 \              insert (Crypt K X) (analz H)";
-by (rtac (analz_insert RSN (2, equalityI)) 1);
-by (rtac subsetI 1);
-by (etac analz.induct 1);
-by (ALLGOALS (fast_tac (!claset addss (!simpset))));
+by (analz_tac 1);
 qed "analz_insert_Crypt";
 
 goal thy "!!H. Key (invKey K) : analz H ==>  \
@@ -443,9 +444,8 @@
                                                analz_insert_Decrypt])));
 qed "analz_Crypt_if";
 
-Addsimps [analz_insert_Agent, analz_insert_Nonce, 
-          analz_insert_Key, analz_insert_MPair, 
-          analz_Crypt_if];
+Addsimps [analz_insert_Agent, analz_insert_Nonce, analz_insert_Key, 
+	  analz_insert_Hash, analz_insert_MPair, analz_Crypt_if];
 
 (*This rule supposes "for the sake of argument" that we have the key.*)
 goal thy  "analz (insert (Crypt K X) H) <=  \
@@ -547,10 +547,11 @@
 (*NO Agent_synth, as any Agent name can be synthd*)
 val Nonce_synth = mk_cases "Nonce n : synth H";
 val Key_synth   = mk_cases "Key K : synth H";
+val Hash_synth  = mk_cases "Hash X : synth H";
 val MPair_synth = mk_cases "{|X,Y|} : synth H";
 val Crypt_synth = mk_cases "Crypt K X : synth H";
 
-AddSEs [Nonce_synth, Key_synth, MPair_synth, Crypt_synth];
+AddSEs [Nonce_synth, Key_synth, Hash_synth, MPair_synth, Crypt_synth];
 
 goal thy "H <= synth(H)";
 by (Fast_tac 1);
@@ -609,7 +610,7 @@
 by (Fast_tac 1);
 qed "Key_synth_eq";
 
-goal thy "!!K. Key K ~: H ==> (Crypt K X : synth H) = (Crypt K X: H)";
+goal thy "!!K. Key K ~: H ==> (Crypt K X : synth H) = (Crypt K X : H)";
 by (Fast_tac 1);
 qed "Crypt_synth_eq";
 
@@ -635,16 +636,25 @@
 qed "parts_synth";
 Addsimps [parts_synth];
 
-goal thy "analz (synth H) = analz H Un synth H";
+goal thy "analz (analz G Un H) = analz (G Un H)";
+by (REPEAT_FIRST (resolve_tac [equalityI, analz_subset_cong]));
+by (ALLGOALS Simp_tac);
+qed "analz_analz_Un";
+
+goal thy "analz (synth G Un H) = analz (G Un H) Un synth G";
 by (rtac equalityI 1);
 by (rtac subsetI 1);
 by (etac analz.induct 1);
-by (best_tac
-    (!claset addIs [synth_increasing RS analz_mono RS subsetD]) 5);
+by (deepen_tac (!claset addIs [impOfSubs analz_mono]) 0 5);
 (*Strange that best_tac just can't hack this one...*)
 by (ALLGOALS (deepen_tac (!claset addIs analz.intrs) 0));
+qed "analz_synth_Un";
+
+goal thy "analz (synth H) = analz H Un synth H";
+by (cut_inst_tac [("H","{}")] analz_synth_Un 1);
+by (Full_simp_tac 1);
 qed "analz_synth";
-Addsimps [analz_synth];
+Addsimps [analz_analz_Un, analz_synth_Un, analz_synth];
 
 (*Hard to prove; still needed now that there's only one Spy?*)
 goal thy "analz (UN i. synth (H i)) = \
@@ -689,6 +699,17 @@
                       addss (!simpset)) 1);
 qed "Crypt_Fake_parts_insert";
 
+goal thy "!!H. X: synth (analz G) ==> \
+\              analz (insert X H) <= synth (analz G) Un analz (G Un H)";
+by (rtac subsetI 1);
+by (subgoal_tac "x : analz (synth (analz G) Un H)" 1);
+by (best_tac (!claset addIs [impOfSubs (analz_mono RS synth_mono)]
+                      addSEs [impOfSubs analz_mono]) 2);
+by (Full_simp_tac 1);
+by (Fast_tac 1);
+qed "Fake_analz_insert";
+
+(*Needed????????????????*)
 goal thy "!!H. [| X: synth (analz G); G <= H |] ==> \
 \              analz (insert X H) <= synth (analz H) Un analz H";
 by (rtac subsetI 1);
@@ -697,7 +718,7 @@
                       addSEs [impOfSubs analz_mono]) 2);
 by (Full_simp_tac 1);
 by (Fast_tac 1);
-qed "Fake_analz_insert";
+qed "Fake_analz_insert_old";
 
 goal thy "(X: analz H & X: parts H) = (X: analz H)";
 by (fast_tac (!claset addDs [impOfSubs analz_subset_parts]) 1);
@@ -724,6 +745,13 @@
 qed "Crypt_synth_analz";
 
 
+goal thy "!!K. Key K ~: analz H \
+\   ==> (Hash{|Key K,X|} : synth (analz H)) = (Hash{|Key K,X|} : analz H)";
+by (Fast_tac 1);
+qed "Hash_synth_analz";
+Addsimps [Hash_synth_analz];
+
+
 (*We do NOT want Crypt... messages broken up in protocols!!*)
 Delrules partsEs;
 
@@ -735,10 +763,11 @@
                           insert_commute;
 
 val pushKeys = map (insComm thy "Key ?K") 
-                  ["Agent ?C", "Nonce ?N", "MPair ?X ?Y", "Crypt ?X ?K'"];
+                   ["Agent ?C", "Nonce ?N", "Hash ?X", 
+		    "MPair ?X ?Y", "Crypt ?X ?K'"];
 
 val pushCrypts = map (insComm thy "Crypt ?X ?K") 
-                    ["Agent ?C", "Nonce ?N", "MPair ?X' ?Y"];
+                     ["Agent ?C", "Nonce ?N", "Hash ?X'", "MPair ?X' ?Y"];
 
 (*Cannot be added with Addsimps -- we don't always want to re-order messages*)
 val pushes = pushKeys@pushCrypts;
@@ -749,26 +778,38 @@
     match_tac (TrueI::refl::prems) ORELSE' eq_assume_tac
     ORELSE' etac FalseE;
 
-(*Analysis of Fake cases and of messages that forward unknown parts
+val Fake_insert_tac = 
+    dresolve_tac [impOfSubs Fake_analz_insert,
+		  impOfSubs Fake_parts_insert] THEN'
+    eresolve_tac [asm_rl, synth.Inj];
+
+(*Analysis of Fake cases and of messages that forward unknown parts.
   Abstraction over i is ESSENTIAL: it delays the dereferencing of claset
   DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *)
 fun spy_analz_tac i =
-  SELECT_GOAL 
-   (EVERY [  (*push in occurrences of X...*)
-           (REPEAT o CHANGED)
-             (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1),
-             (*...allowing further simplifications*)
-           simp_tac (!simpset setloop split_tac [expand_if]) 1,
-           REPEAT (resolve_tac [allI,impI,notI] 1),
-           dtac (impOfSubs Fake_analz_insert) 1,
-           eresolve_tac [asm_rl, synth.Inj] 1,
-           Fast_tac 1,
-           Asm_full_simp_tac 1,
-           IF_UNSOLVED (depth_tac (!claset addIs [impOfSubs analz_mono]) 2 1)
-           ]) i;
-
+  DETERM
+   (SELECT_GOAL
+     (EVERY 
+      [  (*push in occurrences of X...*)
+       (REPEAT o CHANGED)
+           (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1),
+       (*...allowing further simplifications*)
+       simp_tac (!simpset setloop split_tac [expand_if]) 1,
+       REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI])),
+       DEPTH_SOLVE 
+         (REPEAT (Fake_insert_tac 1) THEN Asm_full_simp_tac 1
+	  THEN
+	  IF_UNSOLVED (depth_tac (!claset addIs [impOfSubs analz_mono,
+						 impOfSubs analz_subset_parts]) 2 1))
+       ]) i);
 
 (*Useful in many uniqueness proofs*)
 fun ex_strip_tac i = REPEAT (swap_res_tac [exI, conjI] i) THEN 
                      assume_tac (i+1);
 
+
+(*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
+goal Set.thy "A Un (B Un A) = B Un A";
+by (Fast_tac 1);
+val Un_absorb3 = result();
+Addsimps [Un_absorb3];

--- a/src/HOL/Auth/Message.thy	Tue Dec 10 15:13:53 1996 +0100
+++ b/src/HOL/Auth/Message.thy	Fri Dec 13 10:17:35 1996 +0100
@@ -28,13 +28,6 @@
   isSymKey :: key=>bool
   "isSymKey K == (invKey K = K)"
 
-  (*We do not assume  Crypt (invKey K) (Crypt K X) = X
-    because Crypt a is constructor!  We assume that encryption is injective,
-    which is not true in the real world.  The alternative is to take
-    Crypt an as uninterpreted function symbol satisfying the equation
-    above.  This seems to require moving to ZF and regarding msg as an
-    inductive definition instead of a datatype.*) 
-
 datatype  (*We allow any number of friendly agents*)
   agent = Server | Friend nat | Spy
 
@@ -42,6 +35,7 @@
   msg = Agent agent
       | Nonce nat
       | Key   key
+      | Hash  msg
       | MPair msg msg
       | Crypt key msg
 
@@ -63,9 +57,9 @@
 consts  parts   :: msg set => msg set
 inductive "parts H"
   intrs 
-    Inj     "X: H ==> X: parts H"
-    Fst     "{|X,Y|} : parts H ==> X : parts H"
-    Snd     "{|X,Y|} : parts H ==> Y : parts H"
+    Inj     "X: H  ==>  X: parts H"
+    Fst     "{|X,Y|}   : parts H ==> X : parts H"
+    Snd     "{|X,Y|}   : parts H ==> Y : parts H"
     Body    "Crypt K X : parts H ==> X : parts H"
 
 
@@ -91,7 +85,8 @@
   intrs 
     Inj     "X: H ==> X: synth H"
     Agent   "Agent agt : synth H"
+    Hash    "X: synth H ==> Hash X : synth H"
     MPair   "[| X: synth H;  Y: synth H |] ==> {|X,Y|} : synth H"
-    Crypt   "[| X: synth H; Key(K): H |] ==> Crypt K X : synth H"
+    Crypt   "[| X: synth H;  Key(K) : H |] ==> Crypt K X : synth H"
 
 end