src/HOL/Auth/Message.ML

 Inductive relations "parts", "analz" and "synth"
 *)
 
 open Message;
 
-AddIffs (msg.inject);
+AddIffs atomic.inject;
+AddIffs msg.inject;
 
 (*Holds because Friend is injective: thus cannot prove for all f*)
 goal thy "(Friend x : Friend``A) = (x:A)";
 by (Auto_tac());
 qed "Friend_image_eq";

 
 goalw thy [keysFor_def] "keysFor (insert (Nonce N) H) = keysFor H";
 by (Blast_tac 1);
 qed "keysFor_insert_Nonce";
 
+goalw thy [keysFor_def] "keysFor (insert (Number N) H) = keysFor H";
+by (Blast_tac 1);
+qed "keysFor_insert_Number";
+
 goalw thy [keysFor_def] "keysFor (insert (Key K) H) = keysFor H";
 by (Blast_tac 1);
 qed "keysFor_insert_Key";
 
 goalw thy [keysFor_def] "keysFor (insert (Hash X) H) = keysFor H";

     "keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)";
 by (Auto_tac());
 qed "keysFor_insert_Crypt";
 
 Addsimps [keysFor_empty, keysFor_Un, keysFor_UN1, 
-          keysFor_insert_Agent, keysFor_insert_Nonce, keysFor_insert_Key, 
+          keysFor_insert_Agent, keysFor_insert_Nonce, 
+	  keysFor_insert_Number, keysFor_insert_Key, 
           keysFor_insert_Hash, keysFor_insert_MPair, keysFor_insert_Crypt];
 AddSEs [keysFor_Un RS equalityD1 RS subsetD RS UnE,
 	keysFor_UN1 RS equalityD1 RS subsetD RS UN1_E];
 
 goalw thy [keysFor_def] "keysFor (Key``E) = {}";

 
 goal thy "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)";
 by (parts_tac 1);
 qed "parts_insert_Nonce";
 
+goal thy "parts (insert (Number N) H) = insert (Number N) (parts H)";
+by (parts_tac 1);
+qed "parts_insert_Number";
+
 goal thy "parts (insert (Key K) H) = insert (Key K) (parts H)";
 by (parts_tac 1);
 qed "parts_insert_Key";
 
 goal thy "parts (insert (Hash X) H) = insert (Hash X) (parts H)";

 by (Auto_tac());
 by (etac parts.induct 1);
 by (ALLGOALS (blast_tac (!claset addIs [parts.Fst, parts.Snd])));
 qed "parts_insert_MPair";
 
-Addsimps [parts_insert_Agent, parts_insert_Nonce, parts_insert_Key, 
+Addsimps [parts_insert_Agent, parts_insert_Nonce, 
+	  parts_insert_Number, parts_insert_Key, 
           parts_insert_Hash, parts_insert_Crypt, parts_insert_MPair];
 
 
 goal thy "parts (Key``N) = Key``N";
 by (Auto_tac());

 Addsimps [parts_image_Key];
 
 
 (*In any message, there is an upper bound N on its greatest nonce.*)
 goal thy "EX N. ALL n. N<=n --> Nonce n ~: parts {msg}";
-by (msg.induct_tac "msg" 1);
+by (induct_tac "msg" 1);
+by (induct_tac "atomic" 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [exI, parts_insert2])));
 (*MPair case: blast_tac works out the necessary sum itself!*)
 by (blast_tac (!claset addSEs [add_leE]) 2);
 (*Nonce case*)
 by (res_inst_tac [("x","N + Suc nat")] exI 1);

 qed "analz_insert_Agent";
 
 goal thy "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)";
 by (analz_tac 1);
 qed "analz_insert_Nonce";
+
+goal thy "analz (insert (Number N) H) = insert (Number N) (analz H)";
+by (analz_tac 1);
+qed "analz_insert_Number";
 
 goal thy "analz (insert (Hash X) H) = insert (Hash X) (analz H)";
 by (analz_tac 1);
 qed "analz_insert_Hash";
 

 by (case_tac "Key (invKey K)  : analz H " 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [analz_insert_Crypt, 
                                                analz_insert_Decrypt])));
 qed "analz_Crypt_if";
 
-Addsimps [analz_insert_Agent, analz_insert_Nonce, analz_insert_Key, 
+Addsimps [analz_insert_Agent, analz_insert_Nonce, 
+	  analz_insert_Number, 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) <=  \
 \          insert (Crypt K X) (analz (insert X H))";

 
 AddIs  synth.intrs;
 
 (*Can only produce a nonce or key if it is already known,
   but can synth a pair or encryption from its components...*)
-val mk_cases = synth.mk_cases msg.simps;
-
-(*NO Agent_synth, as any Agent name can be synthesized*)
+val mk_cases = synth.mk_cases (atomic.simps @ msg.simps);
+
+(*NO Agent_synth, as any Agent name can be synthesized.  Ditto for Number*)
 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";

 
 goal thy "Agent A : synth H";
 by (Blast_tac 1);
 qed "Agent_synth";
 
+goal thy "Number n : synth H";
+by (Blast_tac 1);
+qed "Number_synth";
+
 goal thy "(Nonce N : synth H) = (Nonce N : H)";
 by (Blast_tac 1);
 qed "Nonce_synth_eq";
 
 goal thy "(Key K : synth H) = (Key K : H)";

 
 goal thy "!!K. Key K ~: H ==> (Crypt K X : synth H) = (Crypt K X : H)";
 by (Blast_tac 1);
 qed "Crypt_synth_eq";
 
-Addsimps [Agent_synth, Nonce_synth_eq, Key_synth_eq, Crypt_synth_eq];
+Addsimps [Agent_synth, Number_synth, 
+	  Nonce_synth_eq, Key_synth_eq, Crypt_synth_eq];
 
 
 goalw thy [keysFor_def]
     "keysFor (synth H) = keysFor H Un invKey``{K. Key K : H}";
 by (Blast_tac 1);

 
 goalw thy [HPair_def] "Nonce N ~= Hash[X] Y";
 by (Simp_tac 1);
 qed "Nonce_neq_HPair";
 
+goalw thy [HPair_def] "Number N ~= Hash[X] Y";
+by (Simp_tac 1);
+qed "Number_neq_HPair";
+
 goalw thy [HPair_def] "Key K ~= Hash[X] Y";
 by (Simp_tac 1);
 qed "Key_neq_HPair";
 
 goalw thy [HPair_def] "Hash Z ~= Hash[X] Y";

 
 goalw thy [HPair_def] "Crypt K X' ~= Hash[X] Y";
 by (Simp_tac 1);
 qed "Crypt_neq_HPair";
 
-val HPair_neqs = [Agent_neq_HPair, Nonce_neq_HPair, 
+val HPair_neqs = [Agent_neq_HPair, Nonce_neq_HPair, Number_neq_HPair, 
                   Key_neq_HPair, Hash_neq_HPair, Crypt_neq_HPair];
 
 AddIffs HPair_neqs;
 AddIffs (HPair_neqs RL [not_sym]);
 

 
 fun insComm thy x y = read_instantiate_sg (sign_of thy) [("x",x), ("y",y)] 
                           insert_commute;
 
 val pushKeys = map (insComm thy "Key ?K") 
-                   ["Agent ?C", "Nonce ?N", "Hash ?X", 
-                    "MPair ?X ?Y", "Crypt ?X ?K'"];
+                   ["Agent ?C", "Nonce ?N", "Number ?N", 
+		    "Hash ?X", "MPair ?X ?Y", "Crypt ?X ?K'"];
 
 val pushCrypts = map (insComm thy "Crypt ?X ?K") 
-                     ["Agent ?C", "Nonce ?N", "Hash ?X'", "MPair ?X' ?Y"];
+                     ["Agent ?C", "Nonce ?N", "Number ?N", 
+		      "Hash ?X'", "MPair ?X' ?Y"];
 
 (*Cannot be added with Addsimps -- we don't always want to re-order messages*)
 val pushes = pushKeys@pushCrypts;
 
 

        DEPTH_SOLVE 
          (REPEAT (Fake_insert_tac 1) THEN Asm_full_simp_tac 1
           THEN
           IF_UNSOLVED (Blast.depth_tac
 		       (!claset addIs [analz_insertI,
-				       impOfSubs analz_subset_parts]) 2 1))
+				       impOfSubs analz_subset_parts]) 4 1))
        ]) i);
 
 (** Useful in many uniqueness proofs **)
 fun ex_strip_tac i = REPEAT (swap_res_tac [exI, conjI] i) THEN 
                      assume_tac (i+1);