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