1.1 --- a/src/HOL/Auth/Recur.ML Fri Jan 17 11:50:09 1997 +0100
1.2 +++ b/src/HOL/Auth/Recur.ML Fri Jan 17 12:49:31 1997 +0100
1.3 @@ -10,29 +10,26 @@
1.4
1.5 proof_timing:=true;
1.6 HOL_quantifiers := false;
1.7 -Pretty.setdepth 25;
1.8 +Pretty.setdepth 30;
1.9
1.10
1.11 (** Possibility properties: traces that reach the end
1.12 - ONE theorem would be more elegant and faster!
1.13 - By induction on a list of agents (no repetitions)
1.14 + ONE theorem would be more elegant and faster!
1.15 + By induction on a list of agents (no repetitions)
1.16 **)
1.17
1.18 +
1.19 (*Simplest case: Alice goes directly to the server*)
1.20 goal thy
1.21 "!!A. A ~= Server \
1.22 \ ==> EX K NA. EX evs: recur lost. \
1.23 -\ Says Server A {|Agent A, \
1.24 -\ Crypt (shrK A) {|Key K, Agent Server, Nonce NA|}, \
1.25 +\ Says Server A {|Crypt (shrK A) {|Key K, Agent Server, Nonce NA|}, \
1.26 \ Agent Server|} \
1.27 \ : set_of_list evs";
1.28 by (REPEAT (resolve_tac [exI,bexI] 1));
1.29 by (rtac (recur.Nil RS recur.RA1 RS
1.30 - (respond.One RSN (4,recur.RA3))) 2);
1.31 -by (REPEAT
1.32 - (ALLGOALS (asm_simp_tac (!simpset setsolver safe_solver))
1.33 - THEN
1.34 - REPEAT_FIRST (eq_assume_tac ORELSE' resolve_tac [refl, conjI])));
1.35 + (respond.One RSN (4,recur.RA3))) 2);
1.36 +by possibility_tac;
1.37 result();
1.38
1.39
1.40 @@ -40,44 +37,42 @@
1.41 goal thy
1.42 "!!A B. [| A ~= B; A ~= Server; B ~= Server |] \
1.43 \ ==> EX K. EX NA. EX evs: recur lost. \
1.44 -\ Says B A {|Agent A, Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
1.45 +\ Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
1.46 \ Agent Server|} \
1.47 \ : set_of_list evs";
1.48 +by (cut_facts_tac [Nonce_supply2, Key_supply2] 1);
1.49 +by (REPEAT (eresolve_tac [exE, conjE] 1));
1.50 by (REPEAT (resolve_tac [exI,bexI] 1));
1.51 by (rtac (recur.Nil RS recur.RA1 RS recur.RA2 RS
1.52 - (respond.One RS respond.Cons RSN (4,recur.RA3)) RS
1.53 - recur.RA4) 2);
1.54 -bw HPair_def;
1.55 -by (REPEAT
1.56 - (REPEAT_FIRST (eq_assume_tac ORELSE' resolve_tac [refl, conjI])
1.57 - THEN
1.58 - ALLGOALS (asm_simp_tac (!simpset setsolver safe_solver))));
1.59 + (respond.One RS respond.Cons RSN (4,recur.RA3)) RS
1.60 + recur.RA4) 2);
1.61 +by basic_possibility_tac;
1.62 +by (DEPTH_SOLVE (eresolve_tac [asm_rl, less_not_refl2,
1.63 + less_not_refl2 RS not_sym] 1));
1.64 result();
1.65
1.66
1.67 -(*Case three: Alice, Bob, Charlie and the server*)
1.68 +(*Case three: Alice, Bob, Charlie and the server
1.69 goal thy
1.70 - "!!A B. [| A ~= B; A ~= Server; B ~= Server |] \
1.71 + "!!A B. [| A ~= B; B ~= C; A ~= Server; B ~= Server; C ~= Server |] \
1.72 \ ==> EX K. EX NA. EX evs: recur lost. \
1.73 -\ Says B A {|Agent A, Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
1.74 +\ Says B A {|Crypt (shrK A) {|Key K, Agent B, Nonce NA|}, \
1.75 \ Agent Server|} \
1.76 \ : set_of_list evs";
1.77 +by (cut_facts_tac [Nonce_supply3, Key_supply3] 1);
1.78 +by (REPEAT (eresolve_tac [exE, conjE] 1));
1.79 by (REPEAT (resolve_tac [exI,bexI] 1));
1.80 by (rtac (recur.Nil RS recur.RA1 RS recur.RA2 RS recur.RA2 RS
1.81 - (respond.One RS respond.Cons RS respond.Cons RSN
1.82 - (4,recur.RA3)) RS recur.RA4 RS recur.RA4) 2);
1.83 -bw HPair_def;
1.84 -by (REPEAT (*SLOW: 37 seconds*)
1.85 - (REPEAT_FIRST (eq_assume_tac ORELSE' resolve_tac [refl, conjI])
1.86 - THEN
1.87 - ALLGOALS (asm_simp_tac (!simpset setsolver safe_solver))));
1.88 -by (ALLGOALS
1.89 - (SELECT_GOAL (DEPTH_SOLVE
1.90 - (swap_res_tac [refl, conjI, disjI1, disjI2] 1 APPEND
1.91 - etac not_sym 1))));
1.92 + (respond.One RS respond.Cons RS respond.Cons RSN
1.93 + (4,recur.RA3)) RS recur.RA4 RS recur.RA4) 2);
1.94 +(*SLOW: 70 seconds*)
1.95 +by basic_possibility_tac;
1.96 +by (DEPTH_SOLVE (swap_res_tac [refl, conjI, disjCI] 1
1.97 + ORELSE
1.98 + eresolve_tac [asm_rl, less_not_refl2,
1.99 + less_not_refl2 RS not_sym] 1));
1.100 result();
1.101 -
1.102 -
1.103 +****************)
1.104
1.105 (**** Inductive proofs about recur ****)
1.106
1.107 @@ -99,10 +94,30 @@
1.108 AddSEs [not_Says_to_self RSN (2, rev_notE)];
1.109
1.110
1.111 +
1.112 +goal thy "!!evs. (PA,RB,KAB) : respond evs ==> Key KAB : parts{RB}";
1.113 +by (etac respond.induct 1);
1.114 +by (ALLGOALS Simp_tac);
1.115 +qed "respond_Key_in_parts";
1.116 +
1.117 +goal thy "!!evs. (PA,RB,KAB) : respond evs ==> Key KAB ~: used evs";
1.118 +by (etac respond.induct 1);
1.119 +by (REPEAT (assume_tac 1));
1.120 +qed "respond_imp_not_used";
1.121 +
1.122 +goal thy
1.123 + "!!evs. [| Key K : parts {RB}; (PB,RB,K') : respond evs |] \
1.124 +\ ==> Key K ~: used evs";
1.125 +by (etac rev_mp 1);
1.126 +by (etac respond.induct 1);
1.127 +by (auto_tac(!claset addDs [Key_not_used, respond_imp_not_used],
1.128 + !simpset));
1.129 +qed_spec_mp "Key_in_parts_respond";
1.130 +
1.131 (*Simple inductive reasoning about responses*)
1.132 -goal thy "!!j. (j,PA,RB) : respond i ==> RB : responses i";
1.133 +goal thy "!!evs. (PA,RB,KAB) : respond evs ==> RB : responses evs";
1.134 by (etac respond.induct 1);
1.135 -by (REPEAT (ares_tac responses.intrs 1));
1.136 +by (REPEAT (ares_tac (respond_imp_not_used::responses.intrs) 1));
1.137 qed "respond_imp_responses";
1.138
1.139
1.140 @@ -110,7 +125,7 @@
1.141
1.142 val RA2_analz_sees_Spy = Says_imp_sees_Spy RS analz.Inj |> standard;
1.143
1.144 -goal thy "!!evs. Says C' B {|Agent B, X, Agent B, X', RA|} : set_of_list evs \
1.145 +goal thy "!!evs. Says C' B {|X, X', RA|} : set_of_list evs \
1.146 \ ==> RA : analz (sees lost Spy evs)";
1.147 by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1);
1.148 qed "RA4_analz_sees_Spy";
1.149 @@ -131,8 +146,8 @@
1.150 let val tac = forw_inst_tac [("lost","lost")]
1.151 in tac RA2_parts_sees_Spy 4 THEN
1.152 etac subst 4 (*RA2: DELETE needless definition of PA!*) THEN
1.153 - forward_tac [respond_imp_responses] 5 THEN
1.154 - tac RA4_parts_sees_Spy 6
1.155 + forward_tac [respond_imp_responses] 5 THEN
1.156 + tac RA4_parts_sees_Spy 6
1.157 end;
1.158
1.159 (*For proving the easier theorems about X ~: parts (sees lost Spy evs) *)
1.160 @@ -153,14 +168,6 @@
1.161 (** Spy never sees another agent's long-term key (unless initially lost) **)
1.162
1.163 goal thy
1.164 - "!!evs. (j,PB,RB) : respond i \
1.165 -\ ==> Key K : parts {RB} --> (EX j'. K = newK2(i,j') & j<=j')";
1.166 -be respond.induct 1;
1.167 -by (Auto_tac());
1.168 -by (best_tac (!claset addDs [Suc_leD]) 1);
1.169 -qed_spec_mp "Key_in_parts_respond";
1.170 -
1.171 -goal thy
1.172 "!!evs. evs : recur lost \
1.173 \ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)";
1.174 by (parts_induct_tac 1);
1.175 @@ -189,115 +196,30 @@
1.176 AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D];
1.177
1.178
1.179 -(*** Future keys can't be seen or used! ***)
1.180 +
1.181 +(** Nobody can have used non-existent keys! **)
1.182
1.183 -(*Nobody can have SEEN keys that will be generated in the future. *)
1.184 -goal thy "!!evs. evs : recur lost ==> \
1.185 -\ length evs <= i --> \
1.186 -\ Key (newK2(i,j)) ~: parts (sees lost Spy evs)";
1.187 -by (parts_induct_tac 1);
1.188 -(*RA2*)
1.189 -by (best_tac (!claset addSEs partsEs
1.190 - addSDs [parts_cut]
1.191 - addDs [Suc_leD]
1.192 - addss (!simpset)) 3);
1.193 -(*Fake*)
1.194 -by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
1.195 - impOfSubs parts_insert_subset_Un,
1.196 - Suc_leD]
1.197 - addss (!simpset)) 1);
1.198 -(*For RA3*)
1.199 -by (asm_simp_tac (!simpset addsimps [parts_insert_sees]) 2);
1.200 -(*RA1-RA4*)
1.201 -by (REPEAT (best_tac (!claset addDs [Key_in_parts_respond, Suc_leD]
1.202 - addss (!simpset)) 1));
1.203 -qed_spec_mp "new_keys_not_seen";
1.204 -Addsimps [new_keys_not_seen];
1.205 -
1.206 -(*Variant: old messages must contain old keys!*)
1.207 -goal thy
1.208 - "!!evs. [| Says A B X : set_of_list evs; \
1.209 -\ Key (newK2(i,j)) : parts {X}; \
1.210 -\ evs : recur lost \
1.211 -\ |] ==> i < length evs";
1.212 -by (rtac ccontr 1);
1.213 -by (dtac leI 1);
1.214 -by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Spy]
1.215 - addIs [impOfSubs parts_mono]) 1);
1.216 -qed "Says_imp_old_keys";
1.217 -
1.218 -
1.219 -(*** Future nonces can't be seen or used! ***)
1.220 -
1.221 -goal thy
1.222 - "!!evs. (j, PB, RB) : respond i \
1.223 -\ ==> Nonce N : parts {RB} --> Nonce N : parts {PB}";
1.224 -be respond.induct 1;
1.225 +goal thy
1.226 + "!!evs. [| K : keysFor (parts {RB}); (PB,RB,K') : respond evs |] \
1.227 +\ ==> K : range shrK";
1.228 +by (etac rev_mp 1);
1.229 +by (etac (respond_imp_responses RS responses.induct) 1);
1.230 by (Auto_tac());
1.231 -qed_spec_mp "Nonce_in_parts_respond";
1.232 +qed_spec_mp "Key_in_keysFor_parts";
1.233
1.234
1.235 -goal thy "!!i. evs : recur lost ==> \
1.236 -\ length evs <= i --> Nonce(newN i) ~: parts (sees lost Spy evs)";
1.237 -by (parts_induct_tac 1);
1.238 -(*For RA3*)
1.239 -by (asm_simp_tac (!simpset addsimps [parts_insert_sees]) 4);
1.240 -by (deepen_tac (!claset addSDs [Says_imp_sees_Spy RS parts.Inj]
1.241 - addDs [Nonce_in_parts_respond, parts_cut, Suc_leD]
1.242 - addss (!simpset)) 0 4);
1.243 -(*Fake*)
1.244 -by (fast_tac (!claset addDs [impOfSubs analz_subset_parts,
1.245 - impOfSubs parts_insert_subset_Un,
1.246 - Suc_leD]
1.247 - addss (!simpset)) 1);
1.248 -(*RA1, RA2, RA4*)
1.249 -by (REPEAT_FIRST (fast_tac (!claset
1.250 - addSEs partsEs
1.251 - addEs [leD RS notE]
1.252 - addDs [Suc_leD]
1.253 - addss (!simpset))));
1.254 -qed_spec_mp "new_nonces_not_seen";
1.255 -Addsimps [new_nonces_not_seen];
1.256 -
1.257 -(*Variant: old messages must contain old nonces!*)
1.258 -goal thy "!!evs. [| Says A B X : set_of_list evs; \
1.259 -\ Nonce (newN i) : parts {X}; \
1.260 -\ evs : recur lost \
1.261 -\ |] ==> i < length evs";
1.262 -by (rtac ccontr 1);
1.263 -by (dtac leI 1);
1.264 -by (fast_tac (!claset addSDs [new_nonces_not_seen, Says_imp_sees_Spy]
1.265 - addIs [impOfSubs parts_mono]) 1);
1.266 -qed "Says_imp_old_nonces";
1.267 -
1.268 -
1.269 -(** Nobody can have USED keys that will be generated in the future. **)
1.270 -
1.271 -goal thy
1.272 - "!!evs. (j,PB,RB) : respond i \
1.273 -\ ==> K : keysFor (parts {RB}) --> (EX A. K = shrK A)";
1.274 -be (respond_imp_responses RS responses.induct) 1;
1.275 -by (Auto_tac());
1.276 -qed_spec_mp "Key_in_keysFor_parts_respond";
1.277 -
1.278 -
1.279 -goal thy "!!i. evs : recur lost ==> \
1.280 -\ length evs <= i --> newK2(i,j) ~: keysFor (parts (sees lost Spy evs))";
1.281 +goal thy "!!evs. evs : recur lost ==> \
1.282 +\ Key K ~: used evs --> K ~: keysFor (parts (sees lost Spy evs))";
1.283 by (parts_induct_tac 1);
1.284 (*RA3*)
1.285 -by (fast_tac (!claset addDs [Key_in_keysFor_parts_respond, Suc_leD]
1.286 - addss (!simpset addsimps [parts_insert_sees])) 4);
1.287 -(*RA2*)
1.288 -by (fast_tac (!claset addSEs partsEs
1.289 - addDs [Suc_leD] addss (!simpset)) 3);
1.290 -(*Fake, RA1, RA4*)
1.291 -by (REPEAT
1.292 - (best_tac
1.293 - (!claset addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
1.294 - impOfSubs (parts_insert_subset_Un RS keysFor_mono),
1.295 - Suc_leD]
1.296 - addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)]
1.297 - addss (!simpset)) 1));
1.298 +by (best_tac (!claset addDs [Key_in_keysFor_parts]
1.299 + addss (!simpset addsimps [parts_insert_sees])) 2);
1.300 +(*Fake*)
1.301 +by (best_tac
1.302 + (!claset addIs [impOfSubs analz_subset_parts]
1.303 + addDs [impOfSubs (analz_subset_parts RS keysFor_mono),
1.304 + impOfSubs (parts_insert_subset_Un RS keysFor_mono)]
1.305 + addss (!simpset)) 1);
1.306 qed_spec_mp "new_keys_not_used";
1.307
1.308
1.309 @@ -319,86 +241,82 @@
1.310 dres_inst_tac [("lost","lost")] RA4_analz_sees_Spy 6;
1.311
1.312
1.313 -Delsimps [image_insert];
1.314 -
1.315 (** Session keys are not used to encrypt other session keys **)
1.316
1.317 (*Version for "responses" relation. Handles case RA3 in the theorem below.
1.318 Note that it holds for *any* set H (not just "sees lost Spy evs")
1.319 satisfying the inductive hypothesis.*)
1.320 goal thy
1.321 - "!!evs. [| RB : responses i; \
1.322 -\ ALL K I. (Key K : analz (Key``(newK``I) Un H)) = \
1.323 -\ (K : newK``I | Key K : analz H) |] \
1.324 -\ ==> ALL K I. (Key K : analz (insert RB (Key``(newK``I) Un H))) = \
1.325 -\ (K : newK``I | Key K : analz (insert RB H))";
1.326 -be responses.induct 1;
1.327 -by (ALLGOALS
1.328 - (asm_simp_tac
1.329 - (!simpset addsimps [insert_Key_singleton, insert_Key_image,
1.330 - Un_assoc RS sym, pushKey_newK]
1.331 - setloop split_tac [expand_if])));
1.332 -by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
1.333 -qed "resp_analz_image_newK_lemma";
1.334 + "!!evs. [| RB : responses evs; \
1.335 +\ ALL K KK. KK <= Compl (range shrK) --> \
1.336 +\ (Key K : analz (Key``KK Un H)) = \
1.337 +\ (K : KK | Key K : analz H) |] \
1.338 +\ ==> ALL K KK. KK <= Compl (range shrK) --> \
1.339 +\ (Key K : analz (insert RB (Key``KK Un H))) = \
1.340 +\ (K : KK | Key K : analz (insert RB H))";
1.341 +by (etac responses.induct 1);
1.342 +by (ALLGOALS (asm_simp_tac analz_image_freshK_ss));
1.343 +qed "resp_analz_image_freshK_lemma";
1.344
1.345 (*Version for the protocol. Proof is almost trivial, thanks to the lemma.*)
1.346 goal thy
1.347 - "!!evs. evs : recur lost ==> \
1.348 -\ ALL K I. (Key K : analz (Key``(newK``I) Un (sees lost Spy evs))) = \
1.349 -\ (K : newK``I | Key K : analz (sees lost Spy evs))";
1.350 + "!!evs. evs : recur lost ==> \
1.351 +\ ALL K KK. KK <= Compl (range shrK) --> \
1.352 +\ (Key K : analz (Key``KK Un (sees lost Spy evs))) = \
1.353 +\ (K : KK | Key K : analz (sees lost Spy evs))";
1.354 by (etac recur.induct 1);
1.355 by analz_Fake_tac;
1.356 -by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma]));
1.357 -by (ALLGOALS (asm_simp_tac (!simpset addsimps [resp_analz_image_newK_lemma])));
1.358 +by (REPEAT_FIRST (resolve_tac [allI, impI]));
1.359 +by (REPEAT_FIRST (rtac analz_image_freshK_lemma ));
1.360 +by (ALLGOALS
1.361 + (asm_simp_tac
1.362 + (analz_image_freshK_ss addsimps [resp_analz_image_freshK_lemma])));
1.363 (*Base*)
1.364 by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1);
1.365 (*RA4, RA2, Fake*)
1.366 by (REPEAT (spy_analz_tac 1));
1.367 -val raw_analz_image_newK = result();
1.368 -qed_spec_mp "analz_image_newK";
1.369 +val raw_analz_image_freshK = result();
1.370 +qed_spec_mp "analz_image_freshK";
1.371
1.372
1.373 (*Instance of the lemma with H replaced by (sees lost Spy evs):
1.374 - [| RB : responses i; evs : recur lost |]
1.375 - ==> Key xa : analz (insert RB (Key``newK``x Un sees lost Spy evs)) =
1.376 - (xa : newK``x | Key xa : analz (insert RB (sees lost Spy evs)))
1.377 + [| RB : responses evs; evs : recur lost; |]
1.378 + ==> KK <= Compl (range shrK) -->
1.379 + Key K : analz (insert RB (Key``KK Un sees lost Spy evs)) =
1.380 + (K : KK | Key K : analz (insert RB (sees lost Spy evs)))
1.381 *)
1.382 -bind_thm ("resp_analz_image_newK",
1.383 - raw_analz_image_newK RSN
1.384 - (2, resp_analz_image_newK_lemma) RS spec RS spec);
1.385 +bind_thm ("resp_analz_image_freshK",
1.386 + raw_analz_image_freshK RSN
1.387 + (2, resp_analz_image_freshK_lemma) RS spec RS spec);
1.388
1.389 goal thy
1.390 - "!!evs. evs : recur lost ==> \
1.391 -\ Key K : analz (insert (Key (newK x)) (sees lost Spy evs)) = \
1.392 -\ (K = newK x | Key K : analz (sees lost Spy evs))";
1.393 -by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK,
1.394 - insert_Key_singleton]) 1);
1.395 -by (Fast_tac 1);
1.396 -qed "analz_insert_Key_newK";
1.397 + "!!evs. [| evs : recur lost; KAB ~: range shrK |] ==> \
1.398 +\ Key K : analz (insert (Key KAB) (sees lost Spy evs)) = \
1.399 +\ (K = KAB | Key K : analz (sees lost Spy evs))";
1.400 +by (asm_simp_tac (analz_image_freshK_ss addsimps [analz_image_freshK]) 1);
1.401 +qed "analz_insert_freshK";
1.402
1.403
1.404 -(*This is more general than proving Hash_new_nonces_not_seen: we don't prove
1.405 - that "future nonces" can't be hashed, but that everything that's hashed is
1.406 - already in past traffic. *)
1.407 +(*Everything that's hashed is already in past traffic. *)
1.408 goal thy "!!i. [| evs : recur lost; A ~: lost |] ==> \
1.409 \ Hash {|Key(shrK A), X|} : parts (sees lost Spy evs) --> \
1.410 \ X : parts (sees lost Spy evs)";
1.411 -be recur.induct 1;
1.412 +by (etac recur.induct 1);
1.413 by parts_Fake_tac;
1.414 (*RA3 requires a further induction*)
1.415 -be responses.induct 5;
1.416 +by (etac responses.induct 5);
1.417 by (ALLGOALS Asm_simp_tac);
1.418 (*Fake*)
1.419 by (best_tac (!claset addDs [impOfSubs analz_subset_parts,
1.420 - impOfSubs Fake_parts_insert]
1.421 - addss (!simpset addsimps [parts_insert_sees])) 2);
1.422 + impOfSubs Fake_parts_insert]
1.423 + addss (!simpset addsimps [parts_insert_sees])) 2);
1.424 (*Two others*)
1.425 by (REPEAT (fast_tac (!claset addss (!simpset)) 1));
1.426 bind_thm ("Hash_imp_body", result() RSN (2, rev_mp));
1.427
1.428
1.429 (** The Nonce NA uniquely identifies A's message.
1.430 - This theorem applies to rounds RA1 and RA2!
1.431 + This theorem applies to steps RA1 and RA2!
1.432
1.433 Unicity is not used in other proofs but is desirable in its own right.
1.434 **)
1.435 @@ -409,29 +327,20 @@
1.436 \ Hash {|Key(shrK A), Agent A, Agent B, Nonce NA, P|} \
1.437 \ : parts (sees lost Spy evs) --> B=B' & P=P'";
1.438 by (parts_induct_tac 1);
1.439 -be responses.induct 3;
1.440 +by (etac responses.induct 3);
1.441 by (ALLGOALS (simp_tac (!simpset addsimps [all_conj_distrib])));
1.442 by (step_tac (!claset addSEs partsEs) 1);
1.443 -(*RA1: creation of new Nonce. Move assertion into global context*)
1.444 -by (expand_case_tac "NA = ?y" 1);
1.445 -by (best_tac (!claset addSIs [exI]
1.446 - addSDs [Hash_imp_body]
1.447 - addSEs (new_nonces_not_seen::partsEs)
1.448 - addss (!simpset)) 1);
1.449 -by (best_tac (!claset addss (!simpset)) 1);
1.450 -(*RA2: creation of new Nonce*)
1.451 -by (expand_case_tac "NA = ?y" 1);
1.452 -by (best_tac (!claset addSIs [exI]
1.453 - addSDs [Hash_imp_body]
1.454 - addSEs (new_nonces_not_seen::partsEs)
1.455 - addss (!simpset)) 1);
1.456 -by (best_tac (!claset addss (!simpset)) 1);
1.457 +(*RA1,2: creation of new Nonce. Move assertion into global context*)
1.458 +by (ALLGOALS (expand_case_tac "NA = ?y"));
1.459 +by (REPEAT_FIRST (ares_tac [exI]));
1.460 +by (REPEAT (best_tac (!claset addSDs [Hash_imp_body]
1.461 + addSEs sees_Spy_partsEs) 1));
1.462 val lemma = result();
1.463
1.464 goalw thy [HPair_def]
1.465 - "!!evs.[| HPair (Key(shrK A)) {|Agent A, Agent B, Nonce NA, P|} \
1.466 + "!!evs.[| Hash[Key(shrK A)] {|Agent A, Agent B, Nonce NA, P|} \
1.467 \ : parts (sees lost Spy evs); \
1.468 -\ HPair (Key(shrK A)) {|Agent A, Agent B', Nonce NA, P'|} \
1.469 +\ Hash[Key(shrK A)] {|Agent A, Agent B', Nonce NA, P'|} \
1.470 \ : parts (sees lost Spy evs); \
1.471 \ evs : recur lost; A ~: lost |] \
1.472 \ ==> B=B' & P=P'";
1.473 @@ -445,39 +354,36 @@
1.474 ***)
1.475
1.476 goal thy
1.477 - "!!evs. [| RB : responses i; evs : recur lost |] \
1.478 + "!!evs. [| RB : responses evs; evs : recur lost |] \
1.479 \ ==> (Key (shrK B) : analz (insert RB (sees lost Spy evs))) = (B:lost)";
1.480 -be responses.induct 1;
1.481 +by (etac responses.induct 1);
1.482 by (ALLGOALS
1.483 (asm_simp_tac
1.484 - (!simpset addsimps [resp_analz_image_newK, insert_Key_singleton]
1.485 - setloop split_tac [expand_if])));
1.486 + (analz_image_freshK_ss addsimps [Spy_analz_shrK,
1.487 + resp_analz_image_freshK])));
1.488 qed "shrK_in_analz_respond";
1.489 Addsimps [shrK_in_analz_respond];
1.490
1.491
1.492 goal thy
1.493 - "!!evs. [| RB : responses i; \
1.494 -\ ALL K I. (Key K : analz (Key``(newK``I) Un H)) = \
1.495 -\ (K : newK``I | Key K : analz H) |] \
1.496 + "!!evs. [| RB : responses evs; \
1.497 +\ ALL K KK. KK <= Compl (range shrK) --> \
1.498 +\ (Key K : analz (Key``KK Un H)) = \
1.499 +\ (K : KK | Key K : analz H) |] \
1.500 \ ==> (Key K : analz (insert RB H)) --> \
1.501 -\ (Key K : parts{RB} | Key K : analz H)";
1.502 -be responses.induct 1;
1.503 +\ (Key K : parts{RB} | Key K : analz H)";
1.504 +by (etac responses.induct 1);
1.505 by (ALLGOALS
1.506 (asm_simp_tac
1.507 - (!simpset addsimps [read_instantiate [("H", "?ff``?xx")] parts_insert,
1.508 - resp_analz_image_newK_lemma,
1.509 - insert_Key_singleton, insert_Key_image,
1.510 - Un_assoc RS sym, pushKey_newK]
1.511 - setloop split_tac [expand_if])));
1.512 -(*The "Message" simpset gives the standard treatment of "image"*)
1.513 -by (simp_tac (simpset_of "Message") 1);
1.514 + (analz_image_freshK_ss addsimps [resp_analz_image_freshK_lemma])));
1.515 +(*Simplification using two distinct treatments of "image"*)
1.516 +by (simp_tac (!simpset addsimps [parts_insert2]) 1);
1.517 by (fast_tac (!claset delrules [allE]) 1);
1.518 qed "resp_analz_insert_lemma";
1.519
1.520 bind_thm ("resp_analz_insert",
1.521 - raw_analz_image_newK RSN
1.522 - (2, resp_analz_insert_lemma) RSN(2, rev_mp));
1.523 + raw_analz_image_freshK RSN
1.524 + (2, resp_analz_insert_lemma) RSN(2, rev_mp));
1.525
1.526
1.527 (*The Server does not send such messages. This theorem lets us avoid
1.528 @@ -487,44 +393,51 @@
1.529 \ ==> ALL C X Y P. Says Server C {|X, Agent Server, Agent C, Y, P|} \
1.530 \ ~: set_of_list evs";
1.531 by (etac recur.induct 1);
1.532 -be (respond.induct) 5;
1.533 +by (etac (respond.induct) 5);
1.534 by (Auto_tac());
1.535 qed_spec_mp "Says_Server_not";
1.536 AddSEs [Says_Server_not RSN (2,rev_notE)];
1.537
1.538
1.539 +(*The last key returned by respond indeed appears in a certificate*)
1.540 goal thy
1.541 - "!!i. (j,PB,RB) : respond i \
1.542 -\ ==> EX A' B'. ALL A B N. \
1.543 + "!!K. (Hash[Key(shrK A)] {|Agent A, B, NA, P|}, RA, K) : respond evs \
1.544 +\ ==> Crypt (shrK A) {|Key K, B, NA|} : parts {RA}";
1.545 +by (etac respond.elim 1);
1.546 +by (ALLGOALS Asm_full_simp_tac);
1.547 +qed "respond_certificate";
1.548 +
1.549 +
1.550 +goal thy
1.551 + "!!K'. (PB,RB,KXY) : respond evs \
1.552 +\ ==> EX A' B'. ALL A B N. \
1.553 \ Crypt (shrK A) {|Key K, Agent B, N|} : parts {RB} \
1.554 \ --> (A'=A & B'=B) | (A'=B & B'=A)";
1.555 -be respond.induct 1;
1.556 +by (etac respond.induct 1);
1.557 by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [all_conj_distrib])));
1.558 (*Base case*)
1.559 by (Fast_tac 1);
1.560 by (Step_tac 1);
1.561 +(*Case analysis on K=KBC*)
1.562 by (expand_case_tac "K = ?y" 1);
1.563 +by (dtac respond_Key_in_parts 1);
1.564 by (best_tac (!claset addSIs [exI]
1.565 addSEs partsEs
1.566 - addDs [Key_in_parts_respond]
1.567 - addss (!simpset)) 1);
1.568 + addDs [Key_in_parts_respond]) 1);
1.569 +(*Case analysis on K=KAB*)
1.570 by (expand_case_tac "K = ?y" 1);
1.571 by (REPEAT (ares_tac [exI] 2));
1.572 by (ex_strip_tac 1);
1.573 -be respond.elim 1;
1.574 -by (REPEAT_FIRST (etac Pair_inject ORELSE' hyp_subst_tac));
1.575 -by (ALLGOALS (asm_full_simp_tac
1.576 - (!simpset addsimps [all_conj_distrib, ex_disj_distrib])));
1.577 -by (Fast_tac 1);
1.578 +by (dtac respond_certificate 1);
1.579 by (Fast_tac 1);
1.580 val lemma = result();
1.581
1.582 goal thy
1.583 "!!RB. [| Crypt (shrK A) {|Key K, Agent B, N|} : parts {RB}; \
1.584 \ Crypt (shrK A') {|Key K, Agent B', N'|} : parts {RB}; \
1.585 -\ (j,PB,RB) : respond i |] \
1.586 +\ (PB,RB,KXY) : respond evs |] \
1.587 \ ==> (A'=A & B'=B) | (A'=B & B'=A)";
1.588 -by (prove_unique_tac lemma 1); (*50 seconds??, due to the disjunctions*)
1.589 +by (prove_unique_tac lemma 1); (*50 seconds??, due to the disjunctions*)
1.590 qed "unique_session_keys";
1.591
1.592
1.593 @@ -533,47 +446,34 @@
1.594 the premises, e.g. by having A=Spy **)
1.595
1.596 goal thy
1.597 - "!!j. (j, HPair (Key(shrK A)) {|Agent A, B, NA, P|}, RA) : respond i \
1.598 -\ ==> Crypt (shrK A) {|Key (newK2 (i,j)), B, NA|} : parts {RA}";
1.599 -be respond.elim 1;
1.600 -by (ALLGOALS Asm_full_simp_tac);
1.601 -qed "newK2_respond_lemma";
1.602 -
1.603 -
1.604 -goal thy
1.605 - "!!evs. [| (j,PB,RB) : respond (length evs); evs : recur lost |] \
1.606 + "!!evs. [| (PB,RB,KAB) : respond evs; evs : recur lost |] \
1.607 \ ==> ALL A A' N. A ~: lost & A' ~: lost --> \
1.608 \ Crypt (shrK A) {|Key K, Agent A', N|} : parts{RB} --> \
1.609 \ Key K ~: analz (insert RB (sees lost Spy evs))";
1.610 -be respond.induct 1;
1.611 +by (etac respond.induct 1);
1.612 by (forward_tac [respond_imp_responses] 2);
1.613 -by (ALLGOALS (*4 MINUTES???*)
1.614 +by (forward_tac [respond_imp_not_used] 2);
1.615 +by (ALLGOALS (*43 seconds*)
1.616 (asm_simp_tac
1.617 - (!simpset addsimps
1.618 - ([analz_image_newK, not_parts_not_analz,
1.619 - read_instantiate [("H", "?ff``?xx")] parts_insert,
1.620 - Un_assoc RS sym, resp_analz_image_newK,
1.621 - insert_Key_singleton, analz_insert_Key_newK])
1.622 - setloop split_tac [expand_if])));
1.623 -by (ALLGOALS (simp_tac (simpset_of "Message")));
1.624 -by (Fast_tac 1);
1.625 + (analz_image_freshK_ss addsimps
1.626 + [analz_image_freshK, not_parts_not_analz,
1.627 + shrK_in_analz_respond,
1.628 + read_instantiate [("H", "?ff``?xx")] parts_insert,
1.629 + resp_analz_image_freshK, analz_insert_freshK])));
1.630 +by (ALLGOALS Simp_tac);
1.631 +by (fast_tac (!claset addIs [impOfSubs analz_subset_parts]) 1);
1.632 by (step_tac (!claset addSEs [MPair_parts]) 1);
1.633 -(** LEVEL 6 **)
1.634 -by (fast_tac (!claset addDs [resp_analz_insert, Key_in_parts_respond]
1.635 - addSEs [new_keys_not_seen RS not_parts_not_analz
1.636 - RSN(2,rev_notE)]
1.637 - addss (!simpset)) 4);
1.638 -by (fast_tac (!claset addSDs [newK2_respond_lemma]) 3);
1.639 +(** LEVEL 7 **)
1.640 +by (fast_tac (!claset addSDs [resp_analz_insert, Key_in_parts_respond]
1.641 + addDs [impOfSubs analz_subset_parts]) 4);
1.642 +by (fast_tac (!claset addSDs [respond_certificate]) 3);
1.643 by (best_tac (!claset addSEs partsEs
1.644 addDs [Key_in_parts_respond]
1.645 addss (!simpset)) 2);
1.646 -by (thin_tac "ALL x.?P(x)" 1);
1.647 -be respond.elim 1;
1.648 -by (fast_tac (!claset addss (!simpset)) 1);
1.649 -by (step_tac (!claset addss (!simpset)) 1);
1.650 -by (best_tac (!claset addSEs partsEs
1.651 - addDs [Key_in_parts_respond]
1.652 - addss (!simpset)) 1);
1.653 +by (dtac unique_session_keys 1);
1.654 +by (etac respond_certificate 1);
1.655 +by (assume_tac 1);
1.656 +by (Fast_tac 1);
1.657 qed_spec_mp "respond_Spy_not_see_encrypted_key";
1.658
1.659
1.660 @@ -586,7 +486,7 @@
1.661 by analz_Fake_tac;
1.662 by (ALLGOALS
1.663 (asm_simp_tac
1.664 - (!simpset addsimps [not_parts_not_analz, analz_insert_Key_newK]
1.665 + (!simpset addsimps [not_parts_not_analz, analz_insert_freshK]
1.666 setloop split_tac [expand_if])));
1.667 (*RA4*)
1.668 by (spy_analz_tac 4);
1.669 @@ -596,13 +496,14 @@
1.670 (*RA2*)
1.671 by (spy_analz_tac 1);
1.672 (*RA3, case 2: K is an old key*)
1.673 -by (fast_tac (!claset addSDs [resp_analz_insert]
1.674 - addSEs partsEs
1.675 - addDs [Key_in_parts_respond]
1.676 - addEs [Says_imp_old_keys RS less_irrefl]) 2);
1.677 +by (best_tac (!claset addSDs [resp_analz_insert]
1.678 + addSEs partsEs
1.679 + addDs [Key_in_parts_respond,
1.680 + Says_imp_sees_Spy RS parts.Inj RSN (2, parts_cut)]
1.681 + addss (!simpset)) 2);
1.682 (*RA3, case 1: use lemma previously proved by induction*)
1.683 by (fast_tac (!claset addSEs [respond_Spy_not_see_encrypted_key RSN
1.684 - (2,rev_notE)]) 1);
1.685 + (2,rev_notE)]) 1);
1.686 bind_thm ("Spy_not_see_encrypted_key", result() RS mp RSN (2, rev_mp));
1.687
1.688
1.689 @@ -622,34 +523,29 @@
1.690 (**** Authenticity properties for Agents ****)
1.691
1.692 (*The response never contains Hashes*)
1.693 -(*NEEDED????????????????*)
1.694 goal thy
1.695 - "!!evs. (j,PB,RB) : respond i \
1.696 + "!!evs. (PB,RB,K) : respond evs \
1.697 \ ==> Hash {|Key (shrK B), M|} : parts (insert RB H) --> \
1.698 \ Hash {|Key (shrK B), M|} : parts H";
1.699 -be (respond_imp_responses RS responses.induct) 1;
1.700 +by (etac (respond_imp_responses RS responses.induct) 1);
1.701 by (Auto_tac());
1.702 bind_thm ("Hash_in_parts_respond", result() RSN (2, rev_mp));
1.703
1.704 -(*NEEDED????????????????*)
1.705 (*Only RA1 or RA2 can have caused such a part of a message to appear.*)
1.706 goalw thy [HPair_def]
1.707 "!!evs. [| Hash {|Key(shrK A), Agent A, Agent B, NA, P|} \
1.708 \ : parts (sees lost Spy evs); \
1.709 \ A ~: lost; evs : recur lost |] \
1.710 -\ ==> Says A B (HPair (Key(shrK A)) {|Agent A, Agent B, NA, P|}) \
1.711 +\ ==> Says A B (Hash[Key(shrK A)] {|Agent A, Agent B, NA, P|}) \
1.712 \ : set_of_list evs";
1.713 -be rev_mp 1;
1.714 +by (etac rev_mp 1);
1.715 by (parts_induct_tac 1);
1.716 (*RA3*)
1.717 by (fast_tac (!claset addSDs [Hash_in_parts_respond]) 1);
1.718 qed_spec_mp "Hash_auth_sender";
1.719
1.720
1.721 -val nonce_not_seen_now = le_refl RSN (2, new_nonces_not_seen) RSN (2,rev_notE);
1.722 -
1.723 -
1.724 -(** These two results should subsume (for all agents) the guarantees proved
1.725 +(** These two results subsume (for all agents) the guarantees proved
1.726 separately for A and B in the Otway-Rees protocol.
1.727 **)
1.728