# HG changeset patch
# User paulson
# Date 873973468 -7200
# Node ID a39baf59ea47aa4908e52607f895e8c47eec69e4
# Parent  42a726e008ce590cce9fab3b1a0584af8aedee07
Split base cases from "msg" to "atomic" in order
to reduce the number of freeness theorems

diff -r 42a726e008ce -r a39baf59ea47 src/HOL/Auth/Message.ML
--- a/src/HOL/Auth/Message.ML	Thu Sep 11 12:22:31 1997 +0200
+++ b/src/HOL/Auth/Message.ML	Thu Sep 11 12:24:28 1997 +0200
@@ -9,7 +9,8 @@
 
 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)";
@@ -57,6 +58,10 @@
 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";
@@ -75,7 +80,8 @@
 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];
@@ -247,6 +253,10 @@
 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";
@@ -275,7 +285,8 @@
 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];
 
 
@@ -289,7 +300,8 @@
 
 (*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);
@@ -386,6 +398,10 @@
 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";
@@ -450,7 +466,8 @@
                                                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.*)
@@ -554,9 +571,9 @@
 
 (*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;
+val mk_cases = synth.mk_cases (atomic.simps @ msg.simps);
 
-(*NO Agent_synth, as any Agent name can be synthesized*)
+(*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";
@@ -614,6 +631,10 @@
 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";
@@ -626,7 +647,8 @@
 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]
@@ -762,6 +784,10 @@
 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";
@@ -774,7 +800,7 @@
 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;
@@ -835,11 +861,12 @@
                           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;
@@ -885,7 +912,7 @@
           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 **)
diff -r 42a726e008ce -r a39baf59ea47 src/HOL/Auth/Message.thy
--- a/src/HOL/Auth/Message.thy	Thu Sep 11 12:22:31 1997 +0200
+++ b/src/HOL/Auth/Message.thy	Thu Sep 11 12:24:28 1997 +0200
@@ -31,19 +31,33 @@
 datatype  (*We allow any number of friendly agents*)
   agent = Server | Friend nat | Spy
 
-datatype  (*Messages are agent names, nonces, keys, pairs and encryptions*)
-  msg = Agent agent
-      | Nonce nat
-      | Key   key
-      | Hash  msg
-      | MPair msg msg
-      | Crypt key msg
+datatype  
+  atomic = AGENT  agent	(*Agent names*)
+         | NUMBER nat   (*Ordinary integers, timestamps, ...*)
+         | NONCE  nat   (*Unguessable nonces*)
+         | KEY    key   (*Crypto keys*)
+
+datatype
+  msg = Atomic atomic
+      | Hash   msg       (*Hashing*)
+      | MPair  msg msg   (*Compound messages*)
+      | Crypt  key msg   (*Encryption, public- or shared-key*)
 
 (*Allows messages of the form {|A,B,NA|}, etc...*)
 syntax
+  Agent          :: agent => msg
+  Number         :: nat   => msg
+  Nonce          :: nat   => msg
+  Key            :: key   => msg
   "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")
 
 translations
+  "Agent x"       == "Atomic (AGENT x)"
+  "Number x"	  == "Atomic (NUMBER x)"
+  "Nonce x"	  == "Atomic (NONCE x)"
+  "Key x"	  == "Atomic (KEY x)"
+  "Key``x"	  == "Atomic `` (KEY `` x)"
+
   "{|x, y, z|}"   == "{|x, {|y, z|}|}"
   "{|x, y|}"      == "MPair x y"
 
@@ -83,13 +97,15 @@
 
 (** Inductive definition of "synth" -- what can be built up from a set of
     messages.  A form of upward closure.  Pairs can be built, messages
-    encrypted with known keys.  Agent names may be quoted.  **)
+    encrypted with known keys.  Agent names are public domain.
+    Numbers can be guessed, but Nonces cannot be.  **)
 
 consts  synth   :: msg set => msg set
 inductive "synth H"
   intrs 
     Inj     "X: H ==> X: synth H"
     Agent   "Agent agt : synth H"
+    Number  "Number n  : 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"