Split base cases from "msg" to "atomic" in order
authorpaulson
Thu Sep 11 12:24:28 1997 +0200 (1997-09-11)
changeset 3668a39baf59ea47
parent 3667 42a726e008ce
child 3669 3384c6f1f095
Split base cases from "msg" to "atomic" in order
to reduce the number of freeness theorems
src/HOL/Auth/Message.ML
src/HOL/Auth/Message.thy
     1.1 --- a/src/HOL/Auth/Message.ML	Thu Sep 11 12:22:31 1997 +0200
     1.2 +++ b/src/HOL/Auth/Message.ML	Thu Sep 11 12:24:28 1997 +0200
     1.3 @@ -9,7 +9,8 @@
     1.4  
     1.5  open Message;
     1.6  
     1.7 -AddIffs (msg.inject);
     1.8 +AddIffs atomic.inject;
     1.9 +AddIffs msg.inject;
    1.10  
    1.11  (*Holds because Friend is injective: thus cannot prove for all f*)
    1.12  goal thy "(Friend x : Friend``A) = (x:A)";
    1.13 @@ -57,6 +58,10 @@
    1.14  by (Blast_tac 1);
    1.15  qed "keysFor_insert_Nonce";
    1.16  
    1.17 +goalw thy [keysFor_def] "keysFor (insert (Number N) H) = keysFor H";
    1.18 +by (Blast_tac 1);
    1.19 +qed "keysFor_insert_Number";
    1.20 +
    1.21  goalw thy [keysFor_def] "keysFor (insert (Key K) H) = keysFor H";
    1.22  by (Blast_tac 1);
    1.23  qed "keysFor_insert_Key";
    1.24 @@ -75,7 +80,8 @@
    1.25  qed "keysFor_insert_Crypt";
    1.26  
    1.27  Addsimps [keysFor_empty, keysFor_Un, keysFor_UN1, 
    1.28 -          keysFor_insert_Agent, keysFor_insert_Nonce, keysFor_insert_Key, 
    1.29 +          keysFor_insert_Agent, keysFor_insert_Nonce, 
    1.30 +	  keysFor_insert_Number, keysFor_insert_Key, 
    1.31            keysFor_insert_Hash, keysFor_insert_MPair, keysFor_insert_Crypt];
    1.32  AddSEs [keysFor_Un RS equalityD1 RS subsetD RS UnE,
    1.33  	keysFor_UN1 RS equalityD1 RS subsetD RS UN1_E];
    1.34 @@ -247,6 +253,10 @@
    1.35  by (parts_tac 1);
    1.36  qed "parts_insert_Nonce";
    1.37  
    1.38 +goal thy "parts (insert (Number N) H) = insert (Number N) (parts H)";
    1.39 +by (parts_tac 1);
    1.40 +qed "parts_insert_Number";
    1.41 +
    1.42  goal thy "parts (insert (Key K) H) = insert (Key K) (parts H)";
    1.43  by (parts_tac 1);
    1.44  qed "parts_insert_Key";
    1.45 @@ -275,7 +285,8 @@
    1.46  by (ALLGOALS (blast_tac (!claset addIs [parts.Fst, parts.Snd])));
    1.47  qed "parts_insert_MPair";
    1.48  
    1.49 -Addsimps [parts_insert_Agent, parts_insert_Nonce, parts_insert_Key, 
    1.50 +Addsimps [parts_insert_Agent, parts_insert_Nonce, 
    1.51 +	  parts_insert_Number, parts_insert_Key, 
    1.52            parts_insert_Hash, parts_insert_Crypt, parts_insert_MPair];
    1.53  
    1.54  
    1.55 @@ -289,7 +300,8 @@
    1.56  
    1.57  (*In any message, there is an upper bound N on its greatest nonce.*)
    1.58  goal thy "EX N. ALL n. N<=n --> Nonce n ~: parts {msg}";
    1.59 -by (msg.induct_tac "msg" 1);
    1.60 +by (induct_tac "msg" 1);
    1.61 +by (induct_tac "atomic" 1);
    1.62  by (ALLGOALS (asm_simp_tac (!simpset addsimps [exI, parts_insert2])));
    1.63  (*MPair case: blast_tac works out the necessary sum itself!*)
    1.64  by (blast_tac (!claset addSEs [add_leE]) 2);
    1.65 @@ -386,6 +398,10 @@
    1.66  by (analz_tac 1);
    1.67  qed "analz_insert_Nonce";
    1.68  
    1.69 +goal thy "analz (insert (Number N) H) = insert (Number N) (analz H)";
    1.70 +by (analz_tac 1);
    1.71 +qed "analz_insert_Number";
    1.72 +
    1.73  goal thy "analz (insert (Hash X) H) = insert (Hash X) (analz H)";
    1.74  by (analz_tac 1);
    1.75  qed "analz_insert_Hash";
    1.76 @@ -450,7 +466,8 @@
    1.77                                                 analz_insert_Decrypt])));
    1.78  qed "analz_Crypt_if";
    1.79  
    1.80 -Addsimps [analz_insert_Agent, analz_insert_Nonce, analz_insert_Key, 
    1.81 +Addsimps [analz_insert_Agent, analz_insert_Nonce, 
    1.82 +	  analz_insert_Number, analz_insert_Key, 
    1.83            analz_insert_Hash, analz_insert_MPair, analz_Crypt_if];
    1.84  
    1.85  (*This rule supposes "for the sake of argument" that we have the key.*)
    1.86 @@ -554,9 +571,9 @@
    1.87  
    1.88  (*Can only produce a nonce or key if it is already known,
    1.89    but can synth a pair or encryption from its components...*)
    1.90 -val mk_cases = synth.mk_cases msg.simps;
    1.91 +val mk_cases = synth.mk_cases (atomic.simps @ msg.simps);
    1.92  
    1.93 -(*NO Agent_synth, as any Agent name can be synthesized*)
    1.94 +(*NO Agent_synth, as any Agent name can be synthesized.  Ditto for Number*)
    1.95  val Nonce_synth = mk_cases "Nonce n : synth H";
    1.96  val Key_synth   = mk_cases "Key K : synth H";
    1.97  val Hash_synth  = mk_cases "Hash X : synth H";
    1.98 @@ -614,6 +631,10 @@
    1.99  by (Blast_tac 1);
   1.100  qed "Agent_synth";
   1.101  
   1.102 +goal thy "Number n : synth H";
   1.103 +by (Blast_tac 1);
   1.104 +qed "Number_synth";
   1.105 +
   1.106  goal thy "(Nonce N : synth H) = (Nonce N : H)";
   1.107  by (Blast_tac 1);
   1.108  qed "Nonce_synth_eq";
   1.109 @@ -626,7 +647,8 @@
   1.110  by (Blast_tac 1);
   1.111  qed "Crypt_synth_eq";
   1.112  
   1.113 -Addsimps [Agent_synth, Nonce_synth_eq, Key_synth_eq, Crypt_synth_eq];
   1.114 +Addsimps [Agent_synth, Number_synth, 
   1.115 +	  Nonce_synth_eq, Key_synth_eq, Crypt_synth_eq];
   1.116  
   1.117  
   1.118  goalw thy [keysFor_def]
   1.119 @@ -762,6 +784,10 @@
   1.120  by (Simp_tac 1);
   1.121  qed "Nonce_neq_HPair";
   1.122  
   1.123 +goalw thy [HPair_def] "Number N ~= Hash[X] Y";
   1.124 +by (Simp_tac 1);
   1.125 +qed "Number_neq_HPair";
   1.126 +
   1.127  goalw thy [HPair_def] "Key K ~= Hash[X] Y";
   1.128  by (Simp_tac 1);
   1.129  qed "Key_neq_HPair";
   1.130 @@ -774,7 +800,7 @@
   1.131  by (Simp_tac 1);
   1.132  qed "Crypt_neq_HPair";
   1.133  
   1.134 -val HPair_neqs = [Agent_neq_HPair, Nonce_neq_HPair, 
   1.135 +val HPair_neqs = [Agent_neq_HPair, Nonce_neq_HPair, Number_neq_HPair, 
   1.136                    Key_neq_HPair, Hash_neq_HPair, Crypt_neq_HPair];
   1.137  
   1.138  AddIffs HPair_neqs;
   1.139 @@ -835,11 +861,12 @@
   1.140                            insert_commute;
   1.141  
   1.142  val pushKeys = map (insComm thy "Key ?K") 
   1.143 -                   ["Agent ?C", "Nonce ?N", "Hash ?X", 
   1.144 -                    "MPair ?X ?Y", "Crypt ?X ?K'"];
   1.145 +                   ["Agent ?C", "Nonce ?N", "Number ?N", 
   1.146 +		    "Hash ?X", "MPair ?X ?Y", "Crypt ?X ?K'"];
   1.147  
   1.148  val pushCrypts = map (insComm thy "Crypt ?X ?K") 
   1.149 -                     ["Agent ?C", "Nonce ?N", "Hash ?X'", "MPair ?X' ?Y"];
   1.150 +                     ["Agent ?C", "Nonce ?N", "Number ?N", 
   1.151 +		      "Hash ?X'", "MPair ?X' ?Y"];
   1.152  
   1.153  (*Cannot be added with Addsimps -- we don't always want to re-order messages*)
   1.154  val pushes = pushKeys@pushCrypts;
   1.155 @@ -885,7 +912,7 @@
   1.156            THEN
   1.157            IF_UNSOLVED (Blast.depth_tac
   1.158  		       (!claset addIs [analz_insertI,
   1.159 -				       impOfSubs analz_subset_parts]) 2 1))
   1.160 +				       impOfSubs analz_subset_parts]) 4 1))
   1.161         ]) i);
   1.162  
   1.163  (** Useful in many uniqueness proofs **)
     2.1 --- a/src/HOL/Auth/Message.thy	Thu Sep 11 12:22:31 1997 +0200
     2.2 +++ b/src/HOL/Auth/Message.thy	Thu Sep 11 12:24:28 1997 +0200
     2.3 @@ -31,19 +31,33 @@
     2.4  datatype  (*We allow any number of friendly agents*)
     2.5    agent = Server | Friend nat | Spy
     2.6  
     2.7 -datatype  (*Messages are agent names, nonces, keys, pairs and encryptions*)
     2.8 -  msg = Agent agent
     2.9 -      | Nonce nat
    2.10 -      | Key   key
    2.11 -      | Hash  msg
    2.12 -      | MPair msg msg
    2.13 -      | Crypt key msg
    2.14 +datatype  
    2.15 +  atomic = AGENT  agent	(*Agent names*)
    2.16 +         | NUMBER nat   (*Ordinary integers, timestamps, ...*)
    2.17 +         | NONCE  nat   (*Unguessable nonces*)
    2.18 +         | KEY    key   (*Crypto keys*)
    2.19 +
    2.20 +datatype
    2.21 +  msg = Atomic atomic
    2.22 +      | Hash   msg       (*Hashing*)
    2.23 +      | MPair  msg msg   (*Compound messages*)
    2.24 +      | Crypt  key msg   (*Encryption, public- or shared-key*)
    2.25  
    2.26  (*Allows messages of the form {|A,B,NA|}, etc...*)
    2.27  syntax
    2.28 +  Agent          :: agent => msg
    2.29 +  Number         :: nat   => msg
    2.30 +  Nonce          :: nat   => msg
    2.31 +  Key            :: key   => msg
    2.32    "@MTuple"      :: "['a, args] => 'a * 'b"       ("(2{|_,/ _|})")
    2.33  
    2.34  translations
    2.35 +  "Agent x"       == "Atomic (AGENT x)"
    2.36 +  "Number x"	  == "Atomic (NUMBER x)"
    2.37 +  "Nonce x"	  == "Atomic (NONCE x)"
    2.38 +  "Key x"	  == "Atomic (KEY x)"
    2.39 +  "Key``x"	  == "Atomic `` (KEY `` x)"
    2.40 +
    2.41    "{|x, y, z|}"   == "{|x, {|y, z|}|}"
    2.42    "{|x, y|}"      == "MPair x y"
    2.43  
    2.44 @@ -83,13 +97,15 @@
    2.45  
    2.46  (** Inductive definition of "synth" -- what can be built up from a set of
    2.47      messages.  A form of upward closure.  Pairs can be built, messages
    2.48 -    encrypted with known keys.  Agent names may be quoted.  **)
    2.49 +    encrypted with known keys.  Agent names are public domain.
    2.50 +    Numbers can be guessed, but Nonces cannot be.  **)
    2.51  
    2.52  consts  synth   :: msg set => msg set
    2.53  inductive "synth H"
    2.54    intrs 
    2.55      Inj     "X: H ==> X: synth H"
    2.56      Agent   "Agent agt : synth H"
    2.57 +    Number  "Number n  : synth H"
    2.58      Hash    "X: synth H ==> Hash X : synth H"
    2.59      MPair   "[| X: synth H;  Y: synth H |] ==> {|X,Y|} : synth H"
    2.60      Crypt   "[| X: synth H;  Key(K) : H |] ==> Crypt K X : synth H"