# HG changeset patch # User paulson # Date 842283264 -7200 # Node ID d551e68b7a36b98a7daeacc24385c8472378bc2a # Parent a4abf41134e29d1bd8e963c26b476f45f3d77a8b Stronger proofs; work for Otway-Rees diff -r a4abf41134e2 -r d551e68b7a36 src/HOL/Auth/Message.ML --- a/src/HOL/Auth/Message.ML Mon Sep 09 17:33:23 1996 +0200 +++ b/src/HOL/Auth/Message.ML Mon Sep 09 17:34:24 1996 +0200 @@ -60,6 +60,7 @@ goalw thy [keysFor_def] "keysFor (insert (Crypt X K) H) = insert (invKey K) (keysFor H)"; by (Auto_tac()); +by (Fast_tac 1); qed "keysFor_insert_Crypt"; Addsimps [keysFor_empty, keysFor_Un, keysFor_UN, diff -r a4abf41134e2 -r d551e68b7a36 src/HOL/Auth/OtwayRees.ML --- a/src/HOL/Auth/OtwayRees.ML Mon Sep 09 17:33:23 1996 +0200 +++ b/src/HOL/Auth/OtwayRees.ML Mon Sep 09 17:34:24 1996 +0200 @@ -62,7 +62,10 @@ qed "OR5_parts_sees_Enemy"; (*OR2_analz... and OR4_analz... let us treat those cases using the same - argument as for the Fake case.*) + argument as for the Fake case. This is possible for most, but not all, + proofs: Fake does not invent new nonces (as in OR2), and of course Fake + messages originate from the Enemy. *) + val OR2_OR4_tac = dtac (OR2_analz_sees_Enemy RS (impOfSubs analz_subset_parts)) 4 THEN dtac (OR4_analz_sees_Enemy RS (impOfSubs analz_subset_parts)) 6; @@ -70,9 +73,9 @@ (*** Shared keys are not betrayed ***) -(*Enemy never sees another agent's shared key!*) +(*Enemy never sees another agent's shared key! (unless it is leaked at start)*) goal thy - "!!evs. [| evs : otway; A ~= Enemy |] ==> \ + "!!evs. [| evs : otway; A ~= Enemy; A ~: Friend``leaked |] ==> \ \ Key (shrK A) ~: parts (sees Enemy evs)"; be otway.induct 1; by OR2_OR4_tac; @@ -90,16 +93,20 @@ Enemy_not_analz_shrK, not_sym RSN (2, Enemy_not_analz_shrK)]; -(*We go to some trouble to preserve R in the 3rd subgoal*) +(*We go to some trouble to preserve R in the 3rd and 4th subgoals + As usual fast_tac cannot be used because it uses the equalities too soon*) val major::prems = -goal thy "[| Key (shrK A) : parts (sees Enemy evs); \ -\ evs : otway; \ -\ A=Enemy ==> R \ +goal thy "[| Key (shrK A) : parts (sees Enemy evs); \ +\ evs : otway; \ +\ A=Enemy ==> R; \ +\ !!i. [| A = Friend i; i: leaked |] ==> R \ \ |] ==> R"; br ccontr 1; br ([major, Enemy_not_see_shrK] MRS rev_notE) 1; +br notI 3; +be imageE 3; by (swap_res_tac prems 2); -by (ALLGOALS (fast_tac (!claset addIs prems))); +by (swap_res_tac prems 3 THEN ALLGOALS (fast_tac (!claset addIs prems))); qed "Enemy_see_shrK_E"; bind_thm ("Enemy_analz_shrK_E", @@ -109,28 +116,6 @@ AddSEs [Enemy_see_shrK_E, Enemy_analz_shrK_E]; -(*No Friend will ever see another agent's shared key - (excluding the Enemy, who might transmit his). - The Server, of course, knows all shared keys.*) -goal thy - "!!evs. [| evs : otway; A ~= Enemy; A ~= Friend j |] ==> \ -\ Key (shrK A) ~: parts (sees (Friend j) evs)"; -br (sees_agent_subset_sees_Enemy RS parts_mono RS contra_subsetD) 1; -by (ALLGOALS Asm_simp_tac); -qed "Friend_not_see_shrK"; - - -(*Not for Addsimps -- it can cause goals to blow up!*) -goal thy - "!!evs. evs : otway ==> \ -\ (Key (shrK A) : analz (insert (Key (shrK B)) (sees Enemy evs))) = \ -\ (A=B | A=Enemy)"; -by (best_tac (!claset addDs [impOfSubs analz_subset_parts] - addIs [impOfSubs (subset_insertI RS analz_mono)] - addss (!simpset)) 1); -qed "shrK_mem_analz"; - - (*** Future keys can't be seen or used! ***) (*Nobody can have SEEN keys that will be generated in the future. @@ -220,9 +205,8 @@ (**** The following is to prove theorems of the form - Key K : analz (insert (Key (newK evt)) - (insert (Key (shrK C)) (sees Enemy evs))) ==> - Key K : analz (insert (Key (shrK C)) (sees Enemy evs)) + Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) ==> + Key K : analz (sees Enemy evs) A more general formula must be proved inductively. @@ -243,9 +227,9 @@ by (best_tac (!claset addSEs partsEs addDs [impOfSubs analz_subset_parts, impOfSubs parts_insert_subset_Un] - addss (!simpset)) 1); -(*OR5*) -by (fast_tac (!claset addss (!simpset)) 1); + addss (!simpset)) 2); +(*Base case and OR5*) +by (Auto_tac()); result(); @@ -254,6 +238,9 @@ Delsimps [image_insert]; Addsimps [image_insert RS sym]; +Delsimps [image_Un]; +Addsimps [image_Un RS sym]; + goal thy "insert (Key (newK x)) (sees A evs) = \ \ Key `` (newK``{x}) Un (sees A evs)"; by (Fast_tac 1); @@ -294,25 +281,22 @@ (*Lemma for the trivial direction of the if-and-only-if*) goal thy - "!!evs. (Key K : analz (insert KsC (Key``nE Un sEe))) --> \ -\ (K : nE | Key K : analz (insert KsC sEe)) ==> \ -\ (Key K : analz (insert KsC (Key``nE Un sEe))) = \ -\ (K : nE | Key K : analz (insert KsC sEe))"; + "!!evs. (Key K : analz (Key``nE Un sEe)) --> \ +\ (K : nE | Key K : analz sEe) ==> \ +\ (Key K : analz (Key``nE Un sEe)) = (K : nE | Key K : analz sEe)"; by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1); val lemma = result(); + goal thy "!!evs. evs : otway ==> \ -\ ALL K E. (Key K : analz (insert (Key (shrK C)) \ -\ (Key``(newK``E) Un (sees Enemy evs)))) = \ -\ (K : newK``E | \ -\ Key K : analz (insert (Key (shrK C)) \ -\ (sees Enemy evs)))"; +\ ALL K E. (Key K : analz (Key``(newK``E) Un (sees Enemy evs))) = \ +\ (K : newK``E | Key K : analz (sees Enemy evs))"; be otway.induct 1; bd OR2_analz_sees_Enemy 4; bd OR4_analz_sees_Enemy 6; by (REPEAT_FIRST (resolve_tac [allI, lemma])); -by (ALLGOALS (*Takes 40 secs*) +by (ALLGOALS (*Takes 35 secs*) (asm_simp_tac (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK] @ pushes) @@ -321,14 +305,14 @@ by (enemy_analz_tac 5); (*OR3*) by (Fast_tac 4); -(*OR2*) (** LEVEL 11 **) +(*OR2*) (** LEVEL 7 **) by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")] (insert_commute RS ssubst) 3); by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")] (insert_commute RS ssubst) 3); by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 3); by (enemy_analz_tac 3); -(*Fake case*) (** LEVEL 6 **) +(*Fake case*) (** LEVEL 11 **) by (res_inst_tac [("y1","X"), ("A1", "?G Un (?H::msg set)")] (insert_commute RS ssubst) 2); by (enemy_analz_tac 2); @@ -339,12 +323,8 @@ goal thy "!!evs. evs : otway ==> \ -\ Key K : analz (insert (Key (newK evt)) \ -\ (insert (Key (shrK C)) \ -\ (sees Enemy evs))) = \ -\ (K = newK evt | \ -\ Key K : analz (insert (Key (shrK C)) \ -\ (sees Enemy evs)))"; +\ Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) = \ +\ (K = newK evt | Key K : analz (sees Enemy evs))"; by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, insert_Key_singleton]) 1); by (Fast_tac 1); @@ -371,9 +351,8 @@ "!!evs. [| Says Server (Friend j) \ \ {|Ni, Crypt {|Ni, K|} (shrK (Friend i)), \ \ Crypt {|Nj, K|} (shrK (Friend j))|} : set_of_list evs; \ -\ evs : otway; Friend i ~= C; Friend j ~= C \ -\ |] ==> \ -\ K ~: analz (insert (Key (shrK C)) (sees Enemy evs))"; +\ i ~: leaked; j ~: leaked; evs : otway |] ==> \ +\ K ~: analz (sees Enemy evs)"; be rev_mp 1; be otway.induct 1; bd OR2_analz_sees_Enemy 4; @@ -383,14 +362,14 @@ by (REPEAT_FIRST (resolve_tac [conjI, impI])); by (TRYALL (forward_tac [Says_Server_message_form] THEN' assume_tac)); by (REPEAT_FIRST (eresolve_tac [bexE, exE, conjE] ORELSE' hyp_subst_tac)); -by (ALLGOALS +by (ALLGOALS (asm_full_simp_tac (!simpset addsimps ([analz_subset_parts RS contra_subsetD, analz_insert_Key_newK] @ pushes) setloop split_tac [expand_if]))); (*OR3*) by (fast_tac (!claset addSEs [less_irrefl]) 3); -(*Fake*) (** LEVEL 8 **) +(*Fake*) (** LEVEL 10 **) by (res_inst_tac [("y1","X"), ("x1", "Key ?K")] (insert_commute RS ssubst) 1); by (enemy_analz_tac 1); (*OR4*) @@ -411,9 +390,9 @@ (** First, two lemmas for the Fake, OR2 and OR4 cases **) goal thy - "!!evs. [| X : synth (analz (sees Enemy evs)); \ -\ Crypt X' (shrK C) : parts{X}; \ -\ C ~= Enemy; evs : otway |] \ + "!!evs. [| X : synth (analz (sees Enemy evs)); \ +\ Crypt X' (shrK C) : parts{X}; \ +\ C ~= Enemy; C ~: Friend``leaked; evs : otway |] \ \ ==> Crypt X' (shrK C) : parts (sees Enemy evs)"; by (best_tac (!claset addSEs [impOfSubs analz_subset_parts] addDs [impOfSubs parts_insert_subset_Un] @@ -433,9 +412,9 @@ (*The Key K uniquely identifies a pair of senders in the message encrypted by C, but if C=Enemy then he could send all sorts of nonsense.*) goal thy - "!!evs. evs : otway ==> \ -\ EX A B. ALL C. \ -\ C ~= Enemy --> \ + "!!evs. evs : otway ==> \ +\ EX A B. ALL C. \ +\ C ~= Enemy & C ~: Friend``leaked --> \ \ (ALL S S' X. Says S S' X : set_of_list evs --> \ \ (EX NA. Crypt {|NA, Key K|} (shrK C) : parts{X}) --> C=A | C=B)"; by (Simp_tac 1); diff -r a4abf41134e2 -r d551e68b7a36 src/HOL/Auth/Shared.ML --- a/src/HOL/Auth/Shared.ML Mon Sep 09 17:33:23 1996 +0200 +++ b/src/HOL/Auth/Shared.ML Mon Sep 09 17:34:24 1996 +0200 @@ -20,6 +20,12 @@ open Shared; +(*Holds because Friend is injective: thus cannot prove for all f*) +goal thy "(Friend x : Friend``A) = (x:A)"; +by (Auto_tac()); +qed "Friend_image_eq"; +Addsimps [Friend_image_eq]; + Addsimps [Un_insert_left, Un_insert_right]; (*By default only o_apply is built-in. But in the presence of eta-expansion @@ -96,19 +102,20 @@ Addsimps [shrK_notin_image_newK]; -(*Agents see their own shrKs!*) -goal thy "Key (shrK A) : analz (sees A evs)"; +(*Agents see their own shared keys!*) +goal thy "Key (shrK A) : sees A evs"; by (list.induct_tac "evs" 1); -by (asm_simp_tac (!simpset addsimps [impOfSubs(Un_upper2 RS analz_mono)]) 2); by (agent.induct_tac "A" 1); -by (auto_tac (!claset addIs [range_eqI], !simpset)); -qed "analz_own_shrK"; +by (Auto_tac ()); +qed "sees_own_shrK"; -bind_thm ("parts_own_shrK", - [analz_subset_parts, analz_own_shrK] MRS subsetD); +(*Enemy sees leaked shrKs!*) +goal thy "!!i. i: leaked ==> Key (shrK (Friend i)) : sees Enemy evs"; +by (list.induct_tac "evs" 1); +by (Auto_tac ()); +qed "Enemy_sees_leaked"; -Addsimps [analz_own_shrK, parts_own_shrK]; - +AddSIs [sees_own_shrK, Enemy_sees_leaked]; (** Specialized rewrite rules for (sees A (Says...#evs)) **)