Addition of the Hash constructor
authorpaulson
Fri Dec 13 10:17:35 1996 +0100 (1996-12-13)
changeset 2373490ffa16952e
parent 2372 a2999e19703b
child 2374 4148aa5b00a2
Addition of the Hash constructor
Strengthening spy_analz_tac
src/HOL/Auth/Message.ML
src/HOL/Auth/Message.thy
     1.1 --- a/src/HOL/Auth/Message.ML	Tue Dec 10 15:13:53 1996 +0100
     1.2 +++ b/src/HOL/Auth/Message.ML	Fri Dec 13 10:17:35 1996 +0100
     1.3 @@ -30,6 +30,7 @@
     1.4  
     1.5  open Message;
     1.6  
     1.7 +AddIffs (msg.inject);
     1.8  
     1.9  (** Inverse of keys **)
    1.10  
    1.11 @@ -74,6 +75,10 @@
    1.12  by (fast_tac (!claset addss (!simpset)) 1);
    1.13  qed "keysFor_insert_Key";
    1.14  
    1.15 +goalw thy [keysFor_def] "keysFor (insert (Hash X) H) = keysFor H";
    1.16 +by (fast_tac (!claset addss (!simpset)) 1);
    1.17 +qed "keysFor_insert_Hash";
    1.18 +
    1.19  goalw thy [keysFor_def] "keysFor (insert {|X,Y|} H) = keysFor H";
    1.20  by (fast_tac (!claset addss (!simpset)) 1);
    1.21  qed "keysFor_insert_MPair";
    1.22 @@ -84,9 +89,8 @@
    1.23  qed "keysFor_insert_Crypt";
    1.24  
    1.25  Addsimps [keysFor_empty, keysFor_Un, keysFor_UN, 
    1.26 -          keysFor_insert_Agent, keysFor_insert_Nonce,
    1.27 -          keysFor_insert_Key, keysFor_insert_MPair,
    1.28 -          keysFor_insert_Crypt];
    1.29 +          keysFor_insert_Agent, keysFor_insert_Nonce, keysFor_insert_Key, 
    1.30 +	  keysFor_insert_Hash, keysFor_insert_MPair, keysFor_insert_Crypt];
    1.31  
    1.32  goalw thy [keysFor_def] "!!H. Crypt K X : H ==> invKey K : keysFor H";
    1.33  by (Fast_tac 1);
    1.34 @@ -123,6 +127,8 @@
    1.35  by (REPEAT (ares_tac basic_monos 1));
    1.36  qed "parts_mono";
    1.37  
    1.38 +val parts_insertI = impOfSubs (subset_insertI RS parts_mono);
    1.39 +
    1.40  goal thy "parts{} = {}";
    1.41  by (Step_tac 1);
    1.42  by (etac parts.induct 1);
    1.43 @@ -214,16 +220,16 @@
    1.44  qed "parts_trans";
    1.45  
    1.46  (*Cut*)
    1.47 -goal thy "!!H. [| Y: parts (insert X H);  X: parts H |] ==> Y: parts H";
    1.48 +goal thy "!!H. [| Y: parts (insert X G);  X: parts H |] \
    1.49 +\              ==> Y: parts (G Un H)";
    1.50  by (etac parts_trans 1);
    1.51 -by (Fast_tac 1);
    1.52 +by (Auto_tac());
    1.53  qed "parts_cut";
    1.54  
    1.55 -val parts_insertI = impOfSubs (subset_insertI RS parts_mono);
    1.56 -
    1.57  goal thy "!!H. X: parts H ==> parts (insert X H) = parts H";
    1.58 -by (fast_tac (!claset addSEs [parts_cut]
    1.59 -                      addIs  [parts_insertI]) 1);
    1.60 +by (fast_tac (!claset addSDs [parts_cut]
    1.61 +                      addIs  [parts_insertI] 
    1.62 +                      addss (!simpset)) 1);
    1.63  qed "parts_cut_eq";
    1.64  
    1.65  Addsimps [parts_cut_eq];
    1.66 @@ -231,29 +237,27 @@
    1.67  
    1.68  (** Rewrite rules for pulling out atomic messages **)
    1.69  
    1.70 +fun parts_tac i =
    1.71 +  EVERY [rtac ([subsetI, parts_insert_subset] MRS equalityI) i,
    1.72 +	 etac parts.induct i,
    1.73 +	 REPEAT (fast_tac (!claset addss (!simpset)) i)];
    1.74 +
    1.75  goal thy "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)";
    1.76 -by (rtac (parts_insert_subset RSN (2, equalityI)) 1);
    1.77 -by (rtac subsetI 1);
    1.78 -by (etac parts.induct 1);
    1.79 -(*Simplification breaks up equalities between messages;
    1.80 -  how to make it work for fast_tac??*)
    1.81 -by (ALLGOALS (fast_tac (!claset addss (!simpset))));
    1.82 +by (parts_tac 1);
    1.83  qed "parts_insert_Agent";
    1.84  
    1.85  goal thy "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)";
    1.86 -by (rtac (parts_insert_subset RSN (2, equalityI)) 1);
    1.87 -by (rtac subsetI 1);
    1.88 -by (etac parts.induct 1);
    1.89 -by (ALLGOALS (fast_tac (!claset addss (!simpset))));
    1.90 +by (parts_tac 1);
    1.91  qed "parts_insert_Nonce";
    1.92  
    1.93  goal thy "parts (insert (Key K) H) = insert (Key K) (parts H)";
    1.94 -by (rtac (parts_insert_subset RSN (2, equalityI)) 1);
    1.95 -by (rtac subsetI 1);
    1.96 -by (etac parts.induct 1);
    1.97 -by (ALLGOALS (fast_tac (!claset addss (!simpset))));
    1.98 +by (parts_tac 1);
    1.99  qed "parts_insert_Key";
   1.100  
   1.101 +goal thy "parts (insert (Hash X) H) = insert (Hash X) (parts H)";
   1.102 +by (parts_tac 1);
   1.103 +qed "parts_insert_Hash";
   1.104 +
   1.105  goal thy "parts (insert (Crypt K X) H) = \
   1.106  \         insert (Crypt K X) (parts (insert X H))";
   1.107  by (rtac equalityI 1);
   1.108 @@ -274,8 +278,8 @@
   1.109  by (ALLGOALS (best_tac (!claset addIs [parts.Fst, parts.Snd])));
   1.110  qed "parts_insert_MPair";
   1.111  
   1.112 -Addsimps [parts_insert_Agent, parts_insert_Nonce, 
   1.113 -          parts_insert_Key, parts_insert_Crypt, parts_insert_MPair];
   1.114 +Addsimps [parts_insert_Agent, parts_insert_Nonce, parts_insert_Key, 
   1.115 +          parts_insert_Hash, parts_insert_Crypt, parts_insert_MPair];
   1.116  
   1.117  
   1.118  goal thy "parts (Key``N) = Key``N";
   1.119 @@ -338,6 +342,8 @@
   1.120  by (REPEAT (ares_tac basic_monos 1));
   1.121  qed "analz_mono";
   1.122  
   1.123 +val analz_insertI = impOfSubs (subset_insertI RS analz_mono);
   1.124 +
   1.125  (** General equational properties **)
   1.126  
   1.127  goal thy "analz{} = {}";
   1.128 @@ -359,30 +365,28 @@
   1.129  
   1.130  (** Rewrite rules for pulling out atomic messages **)
   1.131  
   1.132 +fun analz_tac i =
   1.133 +  EVERY [rtac ([subsetI, analz_insert] MRS equalityI) i,
   1.134 +	 etac analz.induct i,
   1.135 +	 REPEAT (fast_tac (!claset addss (!simpset)) i)];
   1.136 +
   1.137  goal thy "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)";
   1.138 -by (rtac (analz_insert RSN (2, equalityI)) 1);
   1.139 -by (rtac subsetI 1);
   1.140 -by (etac analz.induct 1);
   1.141 -(*Simplification breaks up equalities between messages;
   1.142 -  how to make it work for fast_tac??*)
   1.143 -by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   1.144 +by (analz_tac 1);
   1.145  qed "analz_insert_Agent";
   1.146  
   1.147  goal thy "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)";
   1.148 -by (rtac (analz_insert RSN (2, equalityI)) 1);
   1.149 -by (rtac subsetI 1);
   1.150 -by (etac analz.induct 1);
   1.151 -by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   1.152 +by (analz_tac 1);
   1.153  qed "analz_insert_Nonce";
   1.154  
   1.155 +goal thy "analz (insert (Hash X) H) = insert (Hash X) (analz H)";
   1.156 +by (analz_tac 1);
   1.157 +qed "analz_insert_Hash";
   1.158 +
   1.159  (*Can only pull out Keys if they are not needed to decrypt the rest*)
   1.160  goalw thy [keysFor_def]
   1.161      "!!K. K ~: keysFor (analz H) ==>  \
   1.162  \         analz (insert (Key K) H) = insert (Key K) (analz H)";
   1.163 -by (rtac (analz_insert RSN (2, equalityI)) 1);
   1.164 -by (rtac subsetI 1);
   1.165 -by (etac analz.induct 1);
   1.166 -by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   1.167 +by (analz_tac 1);
   1.168  qed "analz_insert_Key";
   1.169  
   1.170  goal thy "analz (insert {|X,Y|} H) = \
   1.171 @@ -400,10 +404,7 @@
   1.172  goal thy "!!H. Key (invKey K) ~: analz H ==>  \
   1.173  \              analz (insert (Crypt K X) H) = \
   1.174  \              insert (Crypt K X) (analz H)";
   1.175 -by (rtac (analz_insert RSN (2, equalityI)) 1);
   1.176 -by (rtac subsetI 1);
   1.177 -by (etac analz.induct 1);
   1.178 -by (ALLGOALS (fast_tac (!claset addss (!simpset))));
   1.179 +by (analz_tac 1);
   1.180  qed "analz_insert_Crypt";
   1.181  
   1.182  goal thy "!!H. Key (invKey K) : analz H ==>  \
   1.183 @@ -443,9 +444,8 @@
   1.184                                                 analz_insert_Decrypt])));
   1.185  qed "analz_Crypt_if";
   1.186  
   1.187 -Addsimps [analz_insert_Agent, analz_insert_Nonce, 
   1.188 -          analz_insert_Key, analz_insert_MPair, 
   1.189 -          analz_Crypt_if];
   1.190 +Addsimps [analz_insert_Agent, analz_insert_Nonce, analz_insert_Key, 
   1.191 +	  analz_insert_Hash, analz_insert_MPair, analz_Crypt_if];
   1.192  
   1.193  (*This rule supposes "for the sake of argument" that we have the key.*)
   1.194  goal thy  "analz (insert (Crypt K X) H) <=  \
   1.195 @@ -547,10 +547,11 @@
   1.196  (*NO Agent_synth, as any Agent name can be synthd*)
   1.197  val Nonce_synth = mk_cases "Nonce n : synth H";
   1.198  val Key_synth   = mk_cases "Key K : synth H";
   1.199 +val Hash_synth  = mk_cases "Hash X : synth H";
   1.200  val MPair_synth = mk_cases "{|X,Y|} : synth H";
   1.201  val Crypt_synth = mk_cases "Crypt K X : synth H";
   1.202  
   1.203 -AddSEs [Nonce_synth, Key_synth, MPair_synth, Crypt_synth];
   1.204 +AddSEs [Nonce_synth, Key_synth, Hash_synth, MPair_synth, Crypt_synth];
   1.205  
   1.206  goal thy "H <= synth(H)";
   1.207  by (Fast_tac 1);
   1.208 @@ -609,7 +610,7 @@
   1.209  by (Fast_tac 1);
   1.210  qed "Key_synth_eq";
   1.211  
   1.212 -goal thy "!!K. Key K ~: H ==> (Crypt K X : synth H) = (Crypt K X: H)";
   1.213 +goal thy "!!K. Key K ~: H ==> (Crypt K X : synth H) = (Crypt K X : H)";
   1.214  by (Fast_tac 1);
   1.215  qed "Crypt_synth_eq";
   1.216  
   1.217 @@ -635,16 +636,25 @@
   1.218  qed "parts_synth";
   1.219  Addsimps [parts_synth];
   1.220  
   1.221 -goal thy "analz (synth H) = analz H Un synth H";
   1.222 +goal thy "analz (analz G Un H) = analz (G Un H)";
   1.223 +by (REPEAT_FIRST (resolve_tac [equalityI, analz_subset_cong]));
   1.224 +by (ALLGOALS Simp_tac);
   1.225 +qed "analz_analz_Un";
   1.226 +
   1.227 +goal thy "analz (synth G Un H) = analz (G Un H) Un synth G";
   1.228  by (rtac equalityI 1);
   1.229  by (rtac subsetI 1);
   1.230  by (etac analz.induct 1);
   1.231 -by (best_tac
   1.232 -    (!claset addIs [synth_increasing RS analz_mono RS subsetD]) 5);
   1.233 +by (deepen_tac (!claset addIs [impOfSubs analz_mono]) 0 5);
   1.234  (*Strange that best_tac just can't hack this one...*)
   1.235  by (ALLGOALS (deepen_tac (!claset addIs analz.intrs) 0));
   1.236 +qed "analz_synth_Un";
   1.237 +
   1.238 +goal thy "analz (synth H) = analz H Un synth H";
   1.239 +by (cut_inst_tac [("H","{}")] analz_synth_Un 1);
   1.240 +by (Full_simp_tac 1);
   1.241  qed "analz_synth";
   1.242 -Addsimps [analz_synth];
   1.243 +Addsimps [analz_analz_Un, analz_synth_Un, analz_synth];
   1.244  
   1.245  (*Hard to prove; still needed now that there's only one Spy?*)
   1.246  goal thy "analz (UN i. synth (H i)) = \
   1.247 @@ -689,6 +699,17 @@
   1.248                        addss (!simpset)) 1);
   1.249  qed "Crypt_Fake_parts_insert";
   1.250  
   1.251 +goal thy "!!H. X: synth (analz G) ==> \
   1.252 +\              analz (insert X H) <= synth (analz G) Un analz (G Un H)";
   1.253 +by (rtac subsetI 1);
   1.254 +by (subgoal_tac "x : analz (synth (analz G) Un H)" 1);
   1.255 +by (best_tac (!claset addIs [impOfSubs (analz_mono RS synth_mono)]
   1.256 +                      addSEs [impOfSubs analz_mono]) 2);
   1.257 +by (Full_simp_tac 1);
   1.258 +by (Fast_tac 1);
   1.259 +qed "Fake_analz_insert";
   1.260 +
   1.261 +(*Needed????????????????*)
   1.262  goal thy "!!H. [| X: synth (analz G); G <= H |] ==> \
   1.263  \              analz (insert X H) <= synth (analz H) Un analz H";
   1.264  by (rtac subsetI 1);
   1.265 @@ -697,7 +718,7 @@
   1.266                        addSEs [impOfSubs analz_mono]) 2);
   1.267  by (Full_simp_tac 1);
   1.268  by (Fast_tac 1);
   1.269 -qed "Fake_analz_insert";
   1.270 +qed "Fake_analz_insert_old";
   1.271  
   1.272  goal thy "(X: analz H & X: parts H) = (X: analz H)";
   1.273  by (fast_tac (!claset addDs [impOfSubs analz_subset_parts]) 1);
   1.274 @@ -724,6 +745,13 @@
   1.275  qed "Crypt_synth_analz";
   1.276  
   1.277  
   1.278 +goal thy "!!K. Key K ~: analz H \
   1.279 +\   ==> (Hash{|Key K,X|} : synth (analz H)) = (Hash{|Key K,X|} : analz H)";
   1.280 +by (Fast_tac 1);
   1.281 +qed "Hash_synth_analz";
   1.282 +Addsimps [Hash_synth_analz];
   1.283 +
   1.284 +
   1.285  (*We do NOT want Crypt... messages broken up in protocols!!*)
   1.286  Delrules partsEs;
   1.287  
   1.288 @@ -735,10 +763,11 @@
   1.289                            insert_commute;
   1.290  
   1.291  val pushKeys = map (insComm thy "Key ?K") 
   1.292 -                  ["Agent ?C", "Nonce ?N", "MPair ?X ?Y", "Crypt ?X ?K'"];
   1.293 +                   ["Agent ?C", "Nonce ?N", "Hash ?X", 
   1.294 +		    "MPair ?X ?Y", "Crypt ?X ?K'"];
   1.295  
   1.296  val pushCrypts = map (insComm thy "Crypt ?X ?K") 
   1.297 -                    ["Agent ?C", "Nonce ?N", "MPair ?X' ?Y"];
   1.298 +                     ["Agent ?C", "Nonce ?N", "Hash ?X'", "MPair ?X' ?Y"];
   1.299  
   1.300  (*Cannot be added with Addsimps -- we don't always want to re-order messages*)
   1.301  val pushes = pushKeys@pushCrypts;
   1.302 @@ -749,26 +778,38 @@
   1.303      match_tac (TrueI::refl::prems) ORELSE' eq_assume_tac
   1.304      ORELSE' etac FalseE;
   1.305  
   1.306 -(*Analysis of Fake cases and of messages that forward unknown parts
   1.307 +val Fake_insert_tac = 
   1.308 +    dresolve_tac [impOfSubs Fake_analz_insert,
   1.309 +		  impOfSubs Fake_parts_insert] THEN'
   1.310 +    eresolve_tac [asm_rl, synth.Inj];
   1.311 +
   1.312 +(*Analysis of Fake cases and of messages that forward unknown parts.
   1.313    Abstraction over i is ESSENTIAL: it delays the dereferencing of claset
   1.314    DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *)
   1.315  fun spy_analz_tac i =
   1.316 -  SELECT_GOAL 
   1.317 -   (EVERY [  (*push in occurrences of X...*)
   1.318 -           (REPEAT o CHANGED)
   1.319 -             (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1),
   1.320 -             (*...allowing further simplifications*)
   1.321 -           simp_tac (!simpset setloop split_tac [expand_if]) 1,
   1.322 -           REPEAT (resolve_tac [allI,impI,notI] 1),
   1.323 -           dtac (impOfSubs Fake_analz_insert) 1,
   1.324 -           eresolve_tac [asm_rl, synth.Inj] 1,
   1.325 -           Fast_tac 1,
   1.326 -           Asm_full_simp_tac 1,
   1.327 -           IF_UNSOLVED (depth_tac (!claset addIs [impOfSubs analz_mono]) 2 1)
   1.328 -           ]) i;
   1.329 -
   1.330 +  DETERM
   1.331 +   (SELECT_GOAL
   1.332 +     (EVERY 
   1.333 +      [  (*push in occurrences of X...*)
   1.334 +       (REPEAT o CHANGED)
   1.335 +           (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1),
   1.336 +       (*...allowing further simplifications*)
   1.337 +       simp_tac (!simpset setloop split_tac [expand_if]) 1,
   1.338 +       REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI])),
   1.339 +       DEPTH_SOLVE 
   1.340 +         (REPEAT (Fake_insert_tac 1) THEN Asm_full_simp_tac 1
   1.341 +	  THEN
   1.342 +	  IF_UNSOLVED (depth_tac (!claset addIs [impOfSubs analz_mono,
   1.343 +						 impOfSubs analz_subset_parts]) 2 1))
   1.344 +       ]) i);
   1.345  
   1.346  (*Useful in many uniqueness proofs*)
   1.347  fun ex_strip_tac i = REPEAT (swap_res_tac [exI, conjI] i) THEN 
   1.348                       assume_tac (i+1);
   1.349  
   1.350 +
   1.351 +(*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
   1.352 +goal Set.thy "A Un (B Un A) = B Un A";
   1.353 +by (Fast_tac 1);
   1.354 +val Un_absorb3 = result();
   1.355 +Addsimps [Un_absorb3];
     2.1 --- a/src/HOL/Auth/Message.thy	Tue Dec 10 15:13:53 1996 +0100
     2.2 +++ b/src/HOL/Auth/Message.thy	Fri Dec 13 10:17:35 1996 +0100
     2.3 @@ -28,13 +28,6 @@
     2.4    isSymKey :: key=>bool
     2.5    "isSymKey K == (invKey K = K)"
     2.6  
     2.7 -  (*We do not assume  Crypt (invKey K) (Crypt K X) = X
     2.8 -    because Crypt a is constructor!  We assume that encryption is injective,
     2.9 -    which is not true in the real world.  The alternative is to take
    2.10 -    Crypt an as uninterpreted function symbol satisfying the equation
    2.11 -    above.  This seems to require moving to ZF and regarding msg as an
    2.12 -    inductive definition instead of a datatype.*) 
    2.13 -
    2.14  datatype  (*We allow any number of friendly agents*)
    2.15    agent = Server | Friend nat | Spy
    2.16  
    2.17 @@ -42,6 +35,7 @@
    2.18    msg = Agent agent
    2.19        | Nonce nat
    2.20        | Key   key
    2.21 +      | Hash  msg
    2.22        | MPair msg msg
    2.23        | Crypt key msg
    2.24  
    2.25 @@ -63,9 +57,9 @@
    2.26  consts  parts   :: msg set => msg set
    2.27  inductive "parts H"
    2.28    intrs 
    2.29 -    Inj     "X: H ==> X: parts H"
    2.30 -    Fst     "{|X,Y|} : parts H ==> X : parts H"
    2.31 -    Snd     "{|X,Y|} : parts H ==> Y : parts H"
    2.32 +    Inj     "X: H  ==>  X: parts H"
    2.33 +    Fst     "{|X,Y|}   : parts H ==> X : parts H"
    2.34 +    Snd     "{|X,Y|}   : parts H ==> Y : parts H"
    2.35      Body    "Crypt K X : parts H ==> X : parts H"
    2.36  
    2.37  
    2.38 @@ -91,7 +85,8 @@
    2.39    intrs 
    2.40      Inj     "X: H ==> X: synth H"
    2.41      Agent   "Agent agt : synth H"
    2.42 +    Hash    "X: synth H ==> Hash X : synth H"
    2.43      MPair   "[| X: synth H;  Y: synth H |] ==> {|X,Y|} : synth H"
    2.44 -    Crypt   "[| X: synth H; Key(K): H |] ==> Crypt K X : synth H"
    2.45 +    Crypt   "[| X: synth H;  Key(K) : H |] ==> Crypt K X : synth H"
    2.46  
    2.47  end