# HG changeset patch # User paulson # Date 844678551 -7200 # Node ID 5a5e508e2a2ba0547b6a4cef929946f0a2c737f3 # Parent 2395bc55b3e690b3af476e7f63ef58b4c54d7e59 Simple tidying diff -r 2395bc55b3e6 -r 5a5e508e2a2b src/HOL/Auth/OtwayRees.ML --- a/src/HOL/Auth/OtwayRees.ML Mon Oct 07 10:47:01 1996 +0200 +++ b/src/HOL/Auth/OtwayRees.ML Mon Oct 07 10:55:51 1996 +0200 @@ -12,7 +12,6 @@ Proc. Royal Soc. 426 (1989) *) - open OtwayRees; proof_timing:=true; @@ -89,20 +88,26 @@ tac Reveal_parts_sees_Spy 7 end; +(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *) +fun parts_induct_tac i = SELECT_GOAL + (DETERM (etac otway.induct 1 THEN parts_Fake_tac THEN + (*Fake message*) + TRY (best_tac (!claset addDs [impOfSubs analz_subset_parts, + impOfSubs Fake_parts_insert] + addss (!simpset)) 2)) THEN + (*Base case*) + fast_tac (!claset addss (!simpset)) 1 THEN + ALLGOALS Asm_simp_tac) i; (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY sends messages containing X! **) -(*Spy never sees lost another agent's shared key! (unless it is leaked at start)*) +(*Spy never sees another agent's shared key! (unless it's lost at start)*) goal thy "!!evs. [| evs : otway lost; A ~: lost |] \ \ ==> Key (shrK A) ~: parts (sees lost Spy evs)"; -by (etac otway.induct 1); -by parts_Fake_tac; +by (parts_induct_tac 1); by (Auto_tac()); -(*Deals with Fake message*) -by (best_tac (!claset addDs [impOfSubs analz_subset_parts, - impOfSubs Fake_parts_insert]) 1); qed "Spy_not_see_shrK"; bind_thm ("Spy_not_analz_shrK", @@ -139,10 +144,7 @@ goal thy "!!evs. evs : otway lost ==> \ \ length evs <= length evs' --> \ \ Key (newK evs') ~: (UN C. parts (sees lost C evs))"; -by (etac otway.induct 1); -by parts_Fake_tac; -(*auto_tac does not work here, as it performs safe_tac first*) -by (ALLGOALS Asm_simp_tac); +by (parts_induct_tac 1); by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts, impOfSubs parts_insert_subset_Un, Suc_leD] @@ -214,9 +216,7 @@ goal thy "!!evs. evs : otway lost ==> \ \ length evs <= length evs' --> \ \ newK evs' ~: keysFor (UN C. parts (sees lost C evs))"; -by (etac otway.induct 1); -by parts_Fake_tac; -by (ALLGOALS Asm_simp_tac); +by (parts_induct_tac 1); (*OR1 and OR3*) by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,2])); (*Fake, OR2, OR4: these messages send unknown (X) components*) @@ -248,7 +248,43 @@ Addsimps [new_keys_not_used, new_keys_not_analzd]; -(** Lemmas concerning the form of items passed in messages **) + +(*** Proofs involving analz ***) + +(*Describes the form of Key K when the following message is sent. The use of + "parts" strengthens the induction hyp for proving the Fake case. The + assumption A ~: lost prevents its being a Faked message. (Based + on NS_Shared/Says_S_message_form) *) +goal thy + "!!evs. evs: otway lost ==> \ +\ Crypt {|N, Key K|} (shrK A) : parts (sees lost Spy evs) & \ +\ A ~: lost --> \ +\ (EX evt: otway lost. K = newK evt)"; +by (parts_induct_tac 1); +by (Auto_tac()); +qed_spec_mp "Reveal_message_lemma"; + +(*EITHER describes the form of Key K when the following message is sent, + OR reduces it to the Fake case.*) + +goal thy + "!!evs. [| Says B' A {|N, Crypt {|N, Key K|} (shrK A)|} : set_of_list evs; \ +\ evs : otway lost |] \ +\ ==> (EX evt: otway lost. K = newK evt) \ +\ | Key K : analz (sees lost Spy evs)"; +br (Reveal_message_lemma RS disjCI) 1; +ba 1; +by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj] + addDs [impOfSubs analz_subset_parts] + addss (!simpset)) 1); +qed "Reveal_message_form"; + + +(*For proofs involving analz. We again instantiate the variable to "lost".*) +val analz_Fake_tac = + dres_inst_tac [("lost","lost")] OR2_analz_sees_Spy 4 THEN + dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6 THEN + forw_inst_tac [("lost","lost")] Reveal_message_form 7; (**** @@ -283,51 +319,13 @@ (** Session keys are not used to encrypt other session keys **) -(*Describes the form of Key K when the following message is sent. The use of - "parts" strengthens the induction hyp for proving the Fake case. The - assumptions on A are needed to prevent its being a Faked message. (Based - on NS_Shared/Says_S_message_form) *) -goal thy - "!!evs. evs: otway lost ==> \ -\ Crypt {|N, Key K|} (shrK A) : parts (sees lost Spy evs) & \ -\ A ~: lost --> \ -\ (EX evt: otway lost. K = newK evt)"; -by (etac otway.induct 1); -by parts_Fake_tac; -by (ALLGOALS Asm_simp_tac); -(*Deals with Fake message*) -by (best_tac (!claset addDs [impOfSubs analz_subset_parts, - impOfSubs Fake_parts_insert]) 2); -by (Auto_tac()); -val lemma = result() RS mp; - - -(*EITHER describes the form of Key K when the following message is sent, - OR reduces it to the Fake case.*) -goal thy - "!!evs. [| Says B' A {|N, Crypt {|N, Key K|} (shrK A)|} : set_of_list evs; \ -\ evs : otway lost |] \ -\ ==> (EX evt: otway lost. K = newK evt) \ -\ | Key K : analz (sees lost Spy evs)"; -by (excluded_middle_tac "A : lost" 1); -by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj] - addss (!simpset)) 2); -by (forward_tac [lemma] 1); -by (fast_tac (!claset addEs partsEs - addSDs [Says_imp_sees_Spy RS parts.Inj]) 1); -by (Fast_tac 1); -qed "Reveal_message_form"; - - (*The equality makes the induction hypothesis easier to apply*) goal thy "!!evs. evs : otway lost ==> \ \ ALL K E. (Key K : analz (Key``(newK``E) Un (sees lost Spy evs))) = \ \ (K : newK``E | Key K : analz (sees lost Spy evs))"; by (etac otway.induct 1); -by (dtac OR2_analz_sees_Spy 4); -by (dtac OR4_analz_sees_Spy 6); -by (dtac Reveal_message_form 7); +by analz_Fake_tac; by (REPEAT_FIRST (ares_tac [allI, analz_image_newK_lemma])); by (REPEAT ((eresolve_tac [bexE, disjE] ORELSE' hyp_subst_tac) 7)); by (ALLGOALS (*Takes 28 secs*) @@ -339,7 +337,7 @@ (*Reveal case 2, OR4, OR2, Fake*) by (EVERY (map spy_analz_tac [7,5,3,2])); (*Reveal case 1, OR3, Base*) -by (Auto_tac()); +by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1)); qed_spec_mp "analz_image_newK"; @@ -370,9 +368,8 @@ (*Remaining cases: OR3 and OR4*) by (ex_strip_tac 2); by (Fast_tac 2); -by (excluded_middle_tac "K = Key(newK evsa)" 1); -by (Asm_simp_tac 1); -by (REPEAT (ares_tac [refl,exI,impI,conjI] 1)); +by (expand_case_tac "K = ?y" 1); +by (REPEAT (ares_tac [refl,exI,impI,conjI] 2)); (*...we assume X is a very new message, and handle this case by contradiction*) by (fast_tac (!claset addEs [Says_imp_old_keys RS less_irrefl] delrules [conjI] (*prevent split-up into 4 subgoals*) @@ -403,42 +400,27 @@ (*Only OR1 can have caused such a part of a message to appear.*) goal thy - "!!evs. [| A ~: lost; evs : otway lost |] \ -\ ==> Crypt {|NA, Agent A, Agent B|} (shrK A) \ -\ : parts (sees lost Spy evs) --> \ -\ Says A B {|NA, Agent A, Agent B, \ + "!!evs. [| A ~: lost; evs : otway lost |] \ +\ ==> Crypt {|NA, Agent A, Agent B|} (shrK A) \ +\ : parts (sees lost Spy evs) --> \ +\ Says A B {|NA, Agent A, Agent B, \ \ Crypt {|NA, Agent A, Agent B|} (shrK A)|} \ \ : set_of_list evs"; -by (etac otway.induct 1); -by parts_Fake_tac; -by (ALLGOALS Asm_simp_tac); -(*Fake*) -by (best_tac (!claset addSDs [impOfSubs analz_subset_parts, - impOfSubs Fake_parts_insert]) 2); -by (Auto_tac()); +by (parts_induct_tac 1); qed_spec_mp "Crypt_imp_OR1"; -(** The Nonce NA uniquely identifies A's message. **) +(** The Nonce NA uniquely identifies A's message. **) goal thy "!!evs. [| evs : otway lost; A ~: lost |] \ \ ==> EX B'. ALL B. \ \ Crypt {|NA, Agent A, Agent B|} (shrK A) : parts (sees lost Spy evs) \ \ --> B = B'"; -by (etac otway.induct 1); -by parts_Fake_tac; -by (ALLGOALS Asm_simp_tac); -(*Fake*) -by (best_tac (!claset addSDs [impOfSubs analz_subset_parts, - impOfSubs Fake_parts_insert]) 2); -(*Base case*) -by (fast_tac (!claset addss (!simpset)) 1); -by (Step_tac 1); +by (parts_induct_tac 1); +by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); (*OR1: creation of new Nonce. Move assertion into global context*) -by (excluded_middle_tac "NA = Nonce (newN evsa)" 1); -by (Asm_simp_tac 1); -by (Fast_tac 1); +by (expand_case_tac "NA = ?y" 1); by (best_tac (!claset addSEs partsEs addEs [new_nonces_not_seen RSN(2,rev_notE)]) 1); val lemma = result(); @@ -497,26 +479,21 @@ \ Crypt {|NA, Key K|} (shrK A), \ \ Crypt {|NB, Key K|} (shrK B)|} \ \ : set_of_list evs)"; -by (etac otway.induct 1); -by parts_Fake_tac; -by (ALLGOALS Asm_simp_tac); -(*Fake*) -by (best_tac (!claset addSDs [impOfSubs analz_subset_parts, - impOfSubs Fake_parts_insert]) 1); +by (parts_induct_tac 1); (*OR1: it cannot be a new Nonce, contradiction.*) by (fast_tac (!claset addSIs [parts_insertI] addSEs partsEs addEs [Says_imp_old_nonces RS less_irrefl] addss (!simpset)) 1); -(*OR3 and OR4*) (** LEVEL 5 **) +(*OR3 and OR4*) (*OR4*) by (REPEAT (Safe_step_tac 2)); by (REPEAT (best_tac (!claset addSDs [parts_cut]) 3)); by (fast_tac (!claset addSIs [Crypt_imp_OR1] addEs partsEs addDs [Says_imp_sees_Spy RS parts.Inj]) 2); -(*OR3*) (** LEVEL 8 **) -by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib]))); +(*OR3*) (** LEVEL 5 **) +by (asm_simp_tac (!simpset addsimps [ex_disj_distrib]) 1); by (step_tac (!claset delrules [disjCI, impCE]) 1); by (fast_tac (!claset addSEs [MPair_parts] addSDs [Says_imp_sees_Spy RS parts.Inj] @@ -547,7 +524,7 @@ by (fast_tac (!claset addSIs [NA_Crypt_imp_Server_msg] addEs partsEs addDs [Says_imp_sees_Spy RS parts.Inj]) 1); -qed "A_can_trust"; +qed "A_trust_OR4"; (*Describes the form of K and NA when the Server sends this message.*) @@ -577,9 +554,7 @@ \ Says A Spy {|NA, Key K|} ~: set_of_list evs --> \ \ Key K ~: analz (sees lost Spy evs)"; by (etac otway.induct 1); -by (dtac OR2_analz_sees_Spy 4); -by (dtac OR4_analz_sees_Spy 6); -by (forward_tac [Reveal_message_form] 7); +by analz_Fake_tac; by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, disjE] ORELSE' hyp_subst_tac)); by (ALLGOALS (asm_full_simp_tac @@ -599,7 +574,7 @@ by (dtac (Says_imp_sees_Spy RS analz.Inj) 2); by (fast_tac (!claset addSDs [analz.Decrypt] addss (!simpset)) 2); (*So now we have Aa ~: lost *) -by (dtac A_can_trust 1); +by (dtac A_trust_OR4 1); by (REPEAT (assume_tac 1)); by (fast_tac (!claset addDs [unique_session_keys] addss (!simpset)) 1); val lemma = result() RS mp RS mp RSN(2,rev_notE); @@ -643,13 +618,8 @@ \ {|NA, Agent A, Agent B, X', \ \ Crypt {|NA, NB, Agent A, Agent B|} (shrK B)|} \ \ : set_of_list evs)"; -by (etac otway.induct 1); -by parts_Fake_tac; -by (ALLGOALS Asm_simp_tac); -(*Fake*) -by (best_tac (!claset addSDs [impOfSubs analz_subset_parts, - impOfSubs Fake_parts_insert]) 2); -by (Auto_tac()); +by (parts_induct_tac 1); +by (auto_tac (!claset, !simpset addcongs [conj_cong])); qed_spec_mp "Crypt_imp_OR2"; @@ -657,23 +627,13 @@ goal thy "!!evs. [| evs : otway lost; B ~: lost |] \ -\ ==> EX NA' A'. ALL NA A. \ +\ ==> EX NA' A'. ALL NA A. \ \ Crypt {|NA, NB, Agent A, Agent B|} (shrK B) : parts(sees lost Spy evs) \ \ --> NA = NA' & A = A'"; -by (etac otway.induct 1); -by parts_Fake_tac; -by (ALLGOALS Asm_simp_tac); -(*Fake*) -by (best_tac (!claset delrules [conjI,conjE] - addSDs [impOfSubs analz_subset_parts, - impOfSubs Fake_parts_insert]) 2); -(*Base case*) -by (fast_tac (!claset addss (!simpset)) 1); -by (Step_tac 1); +by (parts_induct_tac 1); +by (simp_tac (!simpset addsimps [all_conj_distrib]) 1); (*OR2: creation of new Nonce. Move assertion into global context*) -by (excluded_middle_tac "NB = Nonce (newN evsa)" 1); -by (Asm_simp_tac 1); -by (fast_tac (!claset addSIs [exI]) 1); +by (expand_case_tac "NB = ?y" 1); by (fast_tac (!claset addSEs (nonce_not_seen_now::partsEs)) 1); val lemma = result(); @@ -706,12 +666,7 @@ \ {|NA, Crypt {|NA, Key K|} (shrK A), \ \ Crypt {|NB, Key K|} (shrK B)|} \ \ : set_of_list evs)"; -by (etac otway.induct 1); -by parts_Fake_tac; -by (ALLGOALS (asm_simp_tac (!simpset addcongs [conj_cong]))); -(*Fake*) -by (best_tac (!claset addSDs [impOfSubs analz_subset_parts, - impOfSubs Fake_parts_insert]) 1); +by (parts_induct_tac 1); (*OR1: it cannot be a new Nonce, contradiction.*) by (fast_tac (!claset addSIs [parts_insertI] addSEs partsEs @@ -753,10 +708,10 @@ by (fast_tac (!claset addSIs [NB_Crypt_imp_Server_msg] addEs partsEs addDs [Says_imp_sees_Spy RS parts.Inj]) 1); -qed "B_can_trust"; +qed "B_trust_OR3"; -B_can_trust RS Spy_not_see_encrypted_key; +B_trust_OR3 RS Spy_not_see_encrypted_key; (** A session key uniquely identifies a pair of senders in the message @@ -769,8 +724,7 @@ \ C=A | C=B"; by (Simp_tac 1); (*Miniscoping*) by (etac otway.induct 1); -by (dres_inst_tac [("lost","lost")] OR2_analz_sees_Spy 4); -by (dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6); +by analz_Fake_tac; (*spy_analz_tac just does not work here: it is an entirely different proof!*) by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib, ex_disj_distrib, @@ -778,9 +732,8 @@ parts_insert2]))); by (REPEAT_FIRST (etac exE)); (*OR3: extraction of K = newK evsa to global context...*) (** LEVEL 6 **) -by (excluded_middle_tac "K = newK evsa" 4); -by (Asm_simp_tac 4); -by (REPEAT (ares_tac [exI] 4)); +by (expand_case_tac "K = ?y" 4); +by (REPEAT (ares_tac [exI] 5)); (*...we prove this case by contradiction: the key is too new!*) by (fast_tac (!claset addSEs partsEs addEs [Says_imp_old_keys RS less_irrefl] diff -r 2395bc55b3e6 -r 5a5e508e2a2b src/HOL/Auth/OtwayRees.thy --- a/src/HOL/Auth/OtwayRees.thy Mon Oct 07 10:47:01 1996 +0200 +++ b/src/HOL/Auth/OtwayRees.thy Mon Oct 07 10:55:51 1996 +0200 @@ -73,12 +73,12 @@ (*This message models possible leaks of session keys. Alice's Nonce identifies the protocol run.*) - Reveal "[| evs: otway lost; A ~= Spy; - Says B' A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|} - : set_of_list evs; - Says A B {|Nonce NA, Agent A, Agent B, - Crypt {|Nonce NA, Agent A, Agent B|} (shrK A)|} - : set_of_list evs |] - ==> Says A Spy {|Nonce NA, Key K|} # evs : otway lost" + Revl "[| evs: otway lost; A ~= Spy; + Says B' A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|} + : set_of_list evs; + Says A B {|Nonce NA, Agent A, Agent B, + Crypt {|Nonce NA, Agent A, Agent B|} (shrK A)|} + : set_of_list evs |] + ==> Says A Spy {|Nonce NA, Key K|} # evs : otway lost" end diff -r 2395bc55b3e6 -r 5a5e508e2a2b src/HOL/Auth/Shared.ML --- a/src/HOL/Auth/Shared.ML Mon Oct 07 10:47:01 1996 +0200 +++ b/src/HOL/Auth/Shared.ML Mon Oct 07 10:55:51 1996 +0200 @@ -9,6 +9,18 @@ *) +val prems = goal HOL.thy "[| P ==> Q(True); ~P ==> Q(False) |] ==> Q(P)"; +by (excluded_middle_tac "P" 1); +by (asm_simp_tac (!simpset addsimps prems) 1); +by (asm_simp_tac (!simpset addsimps prems) 1); +val expand_case = result(); + +fun expand_case_tac P i = + res_inst_tac [("P",P)] expand_case i THEN + Simp_tac (i+1) THEN + Simp_tac i; + + (*GOALS.ML??*) fun prlim n = (goals_limit:=n; pr()); @@ -107,7 +119,6 @@ AddSIs [sees_own_shrK, Spy_sees_lost]; - (** Specialized rewrite rules for (sees lost A (Says...#evs)) **) goal thy "sees lost A (Says A B X # evs) = insert X (sees lost A evs)"; @@ -156,6 +167,14 @@ Addsimps [Says_imp_sees_Spy]; AddIs [Says_imp_sees_Spy]; +goal thy + "!!evs. [| Says A B (Crypt X (shrK C)) : set_of_list evs; \ +\ C : lost |] \ +\ ==> X : analz (sees lost Spy evs)"; +by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj] + addss (!simpset)) 1); +qed "Says_Crypt_lost"; + goal thy "initState lost C <= Key `` range shrK"; by (agent.induct_tac "C" 1); by (Auto_tac ()); diff -r 2395bc55b3e6 -r 5a5e508e2a2b src/HOL/Auth/Shared.thy --- a/src/HOL/Auth/Shared.thy Mon Oct 07 10:47:01 1996 +0200 +++ b/src/HOL/Auth/Shared.thy Mon Oct 07 10:55:51 1996 +0200 @@ -23,7 +23,7 @@ (*Server knows all keys; other agents know only their own*) initState_Server "initState lost Server = Key `` range shrK" initState_Friend "initState lost (Friend i) = {Key (shrK (Friend i))}" - initState_Spy "initState lost Spy = Key``shrK``lost" + initState_Spy "initState lost Spy = Key``shrK``lost" datatype (*Messages, and components of agent stores*)