# HG changeset patch # User paulson # Date 846503724 -3600 # Node ID 3106a99d30a515b9705ec0310d2a22281d807765 # Parent 53b6e0bc8ccfdce5b36ab74d4addd48541427d10 Changing from the Reveal to the Oops rule diff -r 53b6e0bc8ccf -r 3106a99d30a5 src/HOL/Auth/NS_Shared.ML --- a/src/HOL/Auth/NS_Shared.ML Sun Oct 27 13:47:02 1996 +0100 +++ b/src/HOL/Auth/NS_Shared.ML Mon Oct 28 12:55:24 1996 +0100 @@ -50,22 +50,22 @@ AddSEs [not_Says_to_self RSN (2, rev_notE)]; (*For reasoning about the encrypted portion of message NS3*) -goal thy "!!evs. (Says S A (Crypt {|N, B, K, X|} KA)) : set_of_list evs ==> \ -\ X : parts (sees lost Spy evs)"; +goal thy "!!evs. Says S A (Crypt {|N, B, K, X|} KA) : set_of_list evs \ +\ ==> X : parts (sees lost Spy evs)"; by (fast_tac (!claset addSEs partsEs addSDs [Says_imp_sees_Spy RS parts.Inj]) 1); qed "NS3_msg_in_parts_sees_Spy"; goal thy - "!!evs. Says S A (Crypt {|NA, B, K, X|} (shrK A)) : set_of_list evs ==> \ -\ K : parts (sees lost Spy evs)"; + "!!evs. Says Server A (Crypt {|NA, B, K, X|} (shrK A)) : set_of_list evs \ +\ ==> K : parts (sees lost Spy evs)"; by (fast_tac (!claset addSEs partsEs addSDs [Says_imp_sees_Spy RS parts.Inj]) 1); -qed "Reveal_parts_sees_Spy"; +qed "Oops_parts_sees_Spy"; val parts_Fake_tac = dres_inst_tac [("lost","lost")] NS3_msg_in_parts_sees_Spy 5 THEN - forw_inst_tac [("lost","lost")] Reveal_parts_sees_Spy 8; + forw_inst_tac [("lost","lost")] Oops_parts_sees_Spy 8; (*For proving the easier theorems about X ~: parts (sees lost Spy evs) *) fun parts_induct_tac i = SELECT_GOAL @@ -82,47 +82,29 @@ (** Theorems of the form X ~: parts (sees lost Spy evs) imply that NOBODY sends messages containing X! **) -(*Spy never sees another agent's shared key!*) +(*Spy never sees another agent's shared key! (unless it's lost at start)*) goal thy - "!!evs. [| evs : ns_shared lost; A ~: lost |] \ -\ ==> Key (shrK A) ~: parts (sees lost Spy evs)"; + "!!evs. evs : ns_shared lost \ +\ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)"; by (parts_induct_tac 1); by (Auto_tac()); -qed "Spy_not_see_shrK"; - -bind_thm ("Spy_not_analz_shrK", - [analz_subset_parts, Spy_not_see_shrK] MRS contra_subsetD); - -Addsimps [Spy_not_see_shrK, Spy_not_analz_shrK]; +qed "Spy_see_shrK"; +Addsimps [Spy_see_shrK]; -(*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 lost Spy evs); \ -\ evs : ns_shared lost; \ -\ A:lost ==> R \ -\ |] ==> R"; -by (rtac ccontr 1); -by (rtac ([major, Spy_not_see_shrK] MRS rev_notE) 1); -by (swap_res_tac prems 2); -by (ALLGOALS (fast_tac (!claset addIs prems))); -qed "Spy_see_shrK_E"; +goal thy + "!!evs. evs : ns_shared lost \ +\ ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)"; +by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset)); +qed "Spy_analz_shrK"; +Addsimps [Spy_analz_shrK]; -bind_thm ("Spy_analz_shrK_E", - analz_subset_parts RS subsetD RS Spy_see_shrK_E); - -AddSEs [Spy_see_shrK_E, Spy_analz_shrK_E]; - +goal thy "!!A. [| Key (shrK A) : parts (sees lost Spy evs); \ +\ evs : ns_shared lost |] ==> A:lost"; +by (fast_tac (!claset addDs [Spy_see_shrK]) 1); +qed "Spy_see_shrK_D"; -goal thy - "!!evs. evs : ns_shared lost ==> \ -\ (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)"; -by (best_tac (!claset addIs [impOfSubs (subset_insertI RS analz_mono)] - addss (!simpset)) 1); -qed "shrK_mem_analz"; - -Addsimps [shrK_mem_analz]; - +bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D); +AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; (*** Future keys can't be seen or used! ***) @@ -256,12 +238,7 @@ \ Crypt {|Key K, Agent A|} (shrK B)|} (shrK A)) \ \ : set_of_list evs"; by (etac rev_mp 1); -by (etac ns_shared.induct 1); -by parts_Fake_tac; -(*Fake case*) -by (best_tac (!claset addSDs [impOfSubs Fake_parts_insert] - addDs [impOfSubs analz_subset_parts] - addss (!simpset)) 2); +by (parts_induct_tac 1); by (Auto_tac()); qed "A_trust_NS2"; @@ -287,6 +264,13 @@ qed "Says_S_message_form"; +(*For proofs involving analz. We again instantiate the variable to "lost".*) +val analz_Fake_tac = + forw_inst_tac [("lost","lost")] Says_Server_message_form 8 THEN + forw_inst_tac [("lost","lost")] Says_S_message_form 5 THEN + Full_simp_tac 7 THEN + REPEAT_FIRST (eresolve_tac [asm_rl, bexE, disjE] ORELSE' hyp_subst_tac); + (**** The following is to prove theorems of the form @@ -320,45 +304,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 - assumption A ~: lost prevents its being a Faked message. *) -goal thy - "!!evs. evs: ns_shared lost ==> \ -\ Crypt {|NA, Agent B, Key K, X|} (shrK A) \ -\ : parts (sees lost Spy evs) & A ~: lost \ -\ --> (EX evt: ns_shared lost. K = newK evt)"; -by (parts_induct_tac 1); -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 S A (Crypt {|NA, Agent B, Key K, X|} (shrK A)) \ -\ : set_of_list evs; \ -\ evs : ns_shared lost |] \ -\ ==> (EX evt: ns_shared lost. K = newK evt) \ -\ | Key K : analz (sees lost Spy evs)"; -by (case_tac "A : lost" 1); -by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj] - addss (!simpset)) 1); -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 : ns_shared 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 ns_shared.induct 1); -by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5); -by (dtac Reveal_message_form 8); -by (REPEAT_FIRST (eresolve_tac [bexE, conjE, disjE] ORELSE' hyp_subst_tac)); +by analz_Fake_tac; by (REPEAT_FIRST (resolve_tac [allI, analz_image_newK_lemma])); by (ALLGOALS (asm_simp_tac @@ -366,8 +318,8 @@ @ pushes) setloop split_tac [expand_if]))); (** LEVEL 6 **) -(*Reveal case 2, NS3, Fake*) -by (EVERY (map spy_analz_tac [7,5,2])); +(*NS3, Fake*) +by (EVERY (map spy_analz_tac [5,2])); by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1)); (*NS3, NS2, Base*) by (REPEAT (Fast_tac 3)); @@ -393,10 +345,8 @@ \ Says Server A (Crypt {|NA, Agent B, Key K, X|} (shrK A)) \ \ : set_of_list evs --> A=A' & NA=NA' & B=B' & X=X'"; by (etac ns_shared.induct 1); -by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5); -by (REPEAT_FIRST (eresolve_tac [conjE, bexE, disjE] ORELSE' hyp_subst_tac)); by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib]))); -by (step_tac (!claset delrules [conjI]) 1); +by (Step_tac 1); (*NS3*) by (ex_strip_tac 2); by (Fast_tac 2); @@ -438,9 +388,7 @@ \ (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set_of_list evs) --> \ \ Key K ~: analz (sees lost Spy evs)"; by (etac ns_shared.induct 1); -by (forward_tac [Reveal_message_form] 8); -by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5); -by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, disjE] ORELSE' hyp_subst_tac)); +by analz_Fake_tac; by (ALLGOALS (asm_simp_tac (!simpset addsimps ([analz_subset_parts RS contra_subsetD, @@ -450,9 +398,9 @@ by (fast_tac (!claset addIs [parts_insertI] addEs [Says_imp_old_keys RS less_irrefl] addss (!simpset)) 2); -(*Revl case 2, OR4, OR2, Fake*) +(*OR4, OR2, Fake*) by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac)); -(*NS3 and Revl subcases*) (**LEVEL 7 **) +(*NS3 and Oops subcases*) (**LEVEL 7 **) by (step_tac (!claset delrules [impCE]) 1); by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 2); be conjE 2; @@ -555,11 +503,11 @@ val lemma = result(); goal thy - "!!evs. [| Crypt (Nonce NB) K : parts (sees lost Spy evs); \ + "!!evs. [| Crypt (Nonce NB) K : parts (sees lost Spy evs); \ \ Says Server A (Crypt {|NA, Agent B, Key K, X|} (shrK A)) \ -\ : set_of_list evs; \ +\ : set_of_list evs; \ \ ALL NB. Says A Spy {|NA, NB, Key K|} ~: set_of_list evs; \ -\ A ~: lost; B ~: lost; evs : ns_shared lost |] \ +\ A ~: lost; B ~: lost; evs : ns_shared lost |] \ \ ==> Says B A (Crypt (Nonce NB) K) : set_of_list evs"; by (fast_tac (!claset addSIs [lemma RS mp RS mp RS mp] addSEs [Spy_not_see_encrypted_key RSN (2, rev_notE)]) 1); diff -r 53b6e0bc8ccf -r 3106a99d30a5 src/HOL/Auth/NS_Shared.thy --- a/src/HOL/Auth/NS_Shared.thy Sun Oct 27 13:47:02 1996 +0100 +++ b/src/HOL/Auth/NS_Shared.thy Mon Oct 28 12:55:24 1996 +0100 @@ -67,10 +67,11 @@ ==> Says A B (Crypt {|Nonce NB, Nonce NB|} K) # evs : ns_shared lost" (*This message models possible leaks of session keys. - The two Nonces identify the protocol run.*) - Revl "[| evs: ns_shared lost; A ~= Spy; - Says B' A (Crypt (Nonce NB) K) : set_of_list evs; - Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)) + The two Nonces identify the protocol run: the rule insists upon + the true senders in order to make them accurate.*) + Oops "[| evs: ns_shared lost; A ~= Spy; + Says B A (Crypt (Nonce NB) K) : set_of_list evs; + Says Server A (Crypt {|Nonce NA, Agent B, Key K, X|} (shrK A)) : set_of_list evs |] ==> Says A Spy {|Nonce NA, Nonce NB, Key K|} # evs : ns_shared lost" diff -r 53b6e0bc8ccf -r 3106a99d30a5 src/HOL/Auth/OtwayRees_AN.ML --- a/src/HOL/Auth/OtwayRees_AN.ML Sun Oct 27 13:47:02 1996 +0100 +++ b/src/HOL/Auth/OtwayRees_AN.ML Mon Oct 28 12:55:24 1996 +0100 @@ -59,16 +59,15 @@ by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1); qed "OR4_analz_sees_Spy"; -goal thy "!!evs. Says B' A (Crypt {|N,Agent A,B,K|} K') : set_of_list evs ==> \ -\ K : parts (sees lost Spy evs)"; +goal thy "!!evs. Says Server B {|X, Crypt {|NB, a, Agent B, K|} K'|} \ +\ : set_of_list evs ==> K : parts (sees lost Spy evs)"; by (fast_tac (!claset addSEs partsEs addSDs [Says_imp_sees_Spy RS parts.Inj]) 1); -qed "Reveal_parts_sees_Spy"; +qed "Oops_parts_sees_Spy"; -(*OR2_analz... and OR4_analz... let us treat those cases using the same +(*OR4_analz_sees_Spy lets us treat those cases using the same 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 Spy. *) + proofs, since Fake messages originate from the Spy. *) bind_thm ("OR4_parts_sees_Spy", OR4_analz_sees_Spy RS (impOfSubs analz_subset_parts)); @@ -77,7 +76,7 @@ harder to complete, since simplification does less for us.*) val parts_Fake_tac = forw_inst_tac [("lost","lost")] OR4_parts_sees_Spy 6 THEN - forw_inst_tac [("lost","lost")] Reveal_parts_sees_Spy 7; + forw_inst_tac [("lost","lost")] Oops_parts_sees_Spy 7; (*For proving the easier theorems about X ~: parts (sees lost Spy evs) *) fun parts_induct_tac i = SELECT_GOAL @@ -95,34 +94,27 @@ (*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)"; + "!!evs. evs : otway lost \ +\ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)"; by (parts_induct_tac 1); by (Auto_tac()); -qed "Spy_not_see_shrK"; - -bind_thm ("Spy_not_analz_shrK", - [analz_subset_parts, Spy_not_see_shrK] MRS contra_subsetD); - -Addsimps [Spy_not_see_shrK, Spy_not_analz_shrK]; +qed "Spy_see_shrK"; +Addsimps [Spy_see_shrK]; -(*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 lost Spy evs); \ -\ evs : otway lost; \ -\ A:lost ==> R \ -\ |] ==> R"; -by (rtac ccontr 1); -by (rtac ([major, Spy_not_see_shrK] MRS rev_notE) 1); -by (swap_res_tac prems 2); -by (ALLGOALS (fast_tac (!claset addIs prems))); -qed "Spy_see_shrK_E"; +goal thy + "!!evs. evs : otway lost \ +\ ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)"; +by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset)); +qed "Spy_analz_shrK"; +Addsimps [Spy_analz_shrK]; -bind_thm ("Spy_analz_shrK_E", - analz_subset_parts RS subsetD RS Spy_see_shrK_E); +goal thy "!!A. [| Key (shrK A) : parts (sees lost Spy evs); \ +\ evs : otway lost |] ==> A:lost"; +by (fast_tac (!claset addDs [Spy_see_shrK]) 1); +qed "Spy_see_shrK_D"; -AddSEs [Spy_see_shrK_E, Spy_analz_shrK_E]; +bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D); +AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; (*** Future keys can't be seen or used! ***) @@ -134,7 +126,7 @@ The Union over C is essential for the induction! *) goal thy "!!evs. evs : otway lost ==> \ \ length evs <= length evs' --> \ -\ Key (newK evs') ~: (UN C. parts (sees lost C evs))"; +\ Key (newK evs') ~: (UN C. parts (sees lost C evs))"; by (parts_induct_tac 1); by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts, impOfSubs parts_insert_subset_Un, @@ -224,39 +216,27 @@ (*** 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, Agent A, B, 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.*) - +(*Describes the form of K and NA when the Server sends this message.*) goal thy - "!!evs. [| Says B' A (Crypt {|N, Agent A, B, 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]) 1); -by (fast_tac (!claset addSDs [Says_Crypt_lost]) 1); -qed "Reveal_message_form"; + "!!evs. [| Says Server B \ +\ {|Crypt {|NA, Agent A, Agent B, K|} (shrK A), \ +\ Crypt {|NB, Agent A, Agent B, K|} (shrK B)|} : set_of_list evs; \ +\ evs : otway lost |] \ +\ ==> (EX evt: otway lost. K = Key(newK evt)) & \ +\ (EX i. NA = Nonce i) & \ +\ (EX j. NB = Nonce j)"; +by (etac rev_mp 1); +by (etac otway.induct 1); +by (ALLGOALS (fast_tac (!claset addss (!simpset)))); +qed "Says_Server_message_form"; (*For proofs involving analz. We again instantiate the variable to "lost".*) val analz_Fake_tac = dres_inst_tac [("lost","lost")] OR4_analz_sees_Spy 6 THEN - forw_inst_tac [("lost","lost")] Reveal_message_form 7; + forw_inst_tac [("lost","lost")] Says_Server_message_form 7 THEN + assume_tac 7 THEN Full_simp_tac 7 THEN + REPEAT ((eresolve_tac [bexE, exE, conjE] ORELSE' hyp_subst_tac) 7); (**** @@ -280,16 +260,15 @@ by (etac otway.induct 1); 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*) (asm_simp_tac (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK] @ pushes) setloop split_tac [expand_if]))); (** LEVEL 5 **) -(*Reveal case 2, OR4, Fake*) -by (EVERY (map spy_analz_tac [6, 4, 2])); -(*Reveal case 1, OR3, Base*) +(*OR4, Fake*) +by (EVERY (map spy_analz_tac [4,2])); +(*Oops, OR3, Base*) by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1)); qed_spec_mp "analz_image_newK"; @@ -306,8 +285,6 @@ (*** The Key K uniquely identifies the Server's message. **) -fun ex_strip_tac i = REPEAT (ares_tac [exI, conjI] i) THEN assume_tac (i+1); - goal thy "!!evs. evs : otway lost ==> \ \ EX A' B' NA' NB'. ALL A B NA NB. \ @@ -387,21 +364,6 @@ qed "A_trust_OR4"; -(*Describes the form of K and NA when the Server sends this message.*) -goal thy - "!!evs. [| Says Server B \ -\ {|Crypt {|NA, Agent A, Agent B, K|} (shrK A), \ -\ Crypt {|NB, Agent A, Agent B, K|} (shrK B)|} : set_of_list evs; \ -\ evs : otway lost |] \ -\ ==> (EX evt: otway lost. K = Key(newK evt)) & \ -\ (EX i. NA = Nonce i) & \ -\ (EX j. NB = Nonce j)"; -by (etac rev_mp 1); -by (etac otway.induct 1); -by (ALLGOALS (fast_tac (!claset addss (!simpset)))); -qed "Says_Server_message_form"; - - (** Crucial secrecy property: Spy does not see the keys sent in msg OR3 Does not in itself guarantee security: an attack could violate the premises, e.g. by having A=Spy **) @@ -412,40 +374,31 @@ \ {|Crypt {|NA, Agent A, Agent B, Key K|} (shrK A), \ \ Crypt {|NB, Agent A, Agent B, Key K|} (shrK B)|} \ \ : set_of_list evs --> \ -\ Says A Spy {|NA, Key K|} ~: set_of_list evs --> \ +\ Says B Spy {|NA, NB, Key K|} ~: set_of_list evs --> \ \ Key K ~: analz (sees lost Spy evs)"; by (etac otway.induct 1); by analz_Fake_tac; -by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, disjE] ORELSE' hyp_subst_tac)); by (ALLGOALS (asm_full_simp_tac (!simpset addsimps ([analz_subset_parts RS contra_subsetD, analz_insert_Key_newK] @ pushes) setloop split_tac [expand_if]))); -(** LEVEL 4 **) (*OR3*) by (fast_tac (!claset addSIs [parts_insertI] addEs [Says_imp_old_keys RS less_irrefl] addss (!simpset addsimps [parts_insert2])) 2); -(*Reveal case 2, OR4, Fake*) +(*OR4, Fake*) by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac)); -(*Reveal case 1*) (** LEVEL 6 **) -by (case_tac "Aa : lost" 1); -(*But this contradicts Key K ~: analz (sees lost Spy evsa) *) -by (dtac (Says_imp_sees_Spy RS analz.Inj) 1); -by (fast_tac (!claset addSDs [analz.Decrypt] addss (!simpset)) 1); -(*So now we have Aa ~: lost *) -by (dtac A_trust_OR4 1); -by (REPEAT (assume_tac 1)); +(*Oops*) by (fast_tac (!claset addDs [unique_session_keys] addss (!simpset)) 1); val lemma = result() RS mp RS mp RSN(2,rev_notE); goal thy "!!evs. [| Says Server B \ -\ {|Crypt {|NA, Agent A, Agent B, K|} (shrK A), \ -\ Crypt {|NB, Agent A, Agent B, K|} (shrK B)|} : set_of_list evs; \ -\ Says A Spy {|NA, K|} ~: set_of_list evs; \ -\ A ~: lost; B ~: lost; evs : otway lost |] \ +\ {|Crypt {|NA, Agent A, Agent B, K|} (shrK A), \ +\ Crypt {|NB, Agent A, Agent B, K|} (shrK B)|} : set_of_list evs;\ +\ Says B Spy {|NA, NB, K|} ~: set_of_list evs; \ +\ A ~: lost; B ~: lost; evs : otway lost |] \ \ ==> K ~: analz (sees lost Spy evs)"; by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); by (fast_tac (!claset addSEs [lemma]) 1); @@ -455,9 +408,9 @@ goal thy "!!evs. [| C ~: {A,B,Server}; \ \ Says Server B \ -\ {|Crypt {|NA, Agent A, Agent B, K|} (shrK A), \ -\ Crypt {|NB, Agent A, Agent B, K|} (shrK B)|} : set_of_list evs; \ -\ Says A Spy {|NA, K|} ~: set_of_list evs; \ +\ {|Crypt {|NA, Agent A, Agent B, K|} (shrK A), \ +\ Crypt {|NB, Agent A, Agent B, K|} (shrK B)|} : set_of_list evs;\ +\ Says B Spy {|NA, NB, K|} ~: set_of_list evs; \ \ A ~: lost; B ~: lost; evs : otway lost |] \ \ ==> K ~: analz (sees lost C evs)"; by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1); diff -r 53b6e0bc8ccf -r 3106a99d30a5 src/HOL/Auth/OtwayRees_AN.thy --- a/src/HOL/Auth/OtwayRees_AN.thy Sun Oct 27 13:47:02 1996 +0100 +++ b/src/HOL/Auth/OtwayRees_AN.thy Mon Oct 28 12:55:24 1996 +0100 @@ -51,7 +51,7 @@ (*Bob receives the Server's (?) message and compares the Nonces with those in the message he previously sent the Server.*) - OR4 "[| evs: otway lost; A ~= B; B ~= Server; + OR4 "[| evs: otway lost; A ~= B; Says S B {|X, Crypt {|Nonce NB, Agent A, Agent B, Key K|} (shrK B)|} : set_of_list evs; @@ -59,12 +59,13 @@ : set_of_list evs |] ==> Says B A X # evs : otway lost" - (*This message models possible leaks of session keys. Alice's Nonce - identifies the protocol run.*) - Revl "[| evs: otway lost; A ~= Spy; - Says B' A (Crypt {|Nonce NA, Agent A, Agent B, Key K|} (shrK A)) - : set_of_list evs; - Says A B {|Agent A, Agent B, Nonce NA|} : set_of_list evs |] - ==> Says A Spy {|Nonce NA, Key K|} # evs : otway lost" + (*This message models possible leaks of session keys. The nonces + identify the protocol run. B is not assumed to know shrK A.*) + Oops "[| evs: otway lost; B ~= Spy; + Says Server B + {|Crypt {|Nonce NA, Agent A, Agent B, Key K|} (shrK A), + Crypt {|Nonce NB, Agent A, Agent B, Key K|} (shrK B)|} + : set_of_list evs |] + ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway lost" end diff -r 53b6e0bc8ccf -r 3106a99d30a5 src/HOL/Auth/OtwayRees_Bad.ML --- a/src/HOL/Auth/OtwayRees_Bad.ML Sun Oct 27 13:47:02 1996 +0100 +++ b/src/HOL/Auth/OtwayRees_Bad.ML Mon Oct 28 12:55:24 1996 +0100 @@ -68,11 +68,11 @@ by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj]) 1); qed "OR4_analz_sees_Spy"; -goal thy "!!evs. Says B' A {|N, Crypt {|N,K|} K'|} : set_of_list evs ==> \ -\ K : parts (sees lost Spy evs)"; +goal thy "!!evs. Says Server B {|NA, X, Crypt {|NB,K|} K'|} : set_of_list evs \ +\ ==> K : parts (sees lost Spy evs)"; by (fast_tac (!claset addSEs partsEs addSDs [Says_imp_sees_Spy RS parts.Inj]) 1); -qed "Reveal_parts_sees_Spy"; +qed "Oops_parts_sees_Spy"; (*OR2_analz... and OR4_analz... let us treat those cases using the same argument as for the Fake case. This is possible for most, but not all, @@ -87,46 +87,46 @@ val parts_Fake_tac = forward_tac [OR2_parts_sees_Spy] 4 THEN forward_tac [OR4_parts_sees_Spy] 6 THEN - forward_tac [Reveal_parts_sees_Spy] 7; + forward_tac [Oops_parts_sees_Spy] 7; + +(*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 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; A ~: lost |] \ -\ ==> Key (shrK A) ~: parts (sees lost Spy evs)"; -by (etac otway.induct 1); -by parts_Fake_tac; + "!!evs. evs : otway \ +\ ==> (Key (shrK A) : parts (sees lost Spy evs)) = (A : lost)"; +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", - [analz_subset_parts, Spy_not_see_shrK] MRS contra_subsetD); - -Addsimps [Spy_not_see_shrK, Spy_not_analz_shrK]; +qed "Spy_see_shrK"; +Addsimps [Spy_see_shrK]; -(*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 lost Spy evs); \ -\ evs : otway; \ -\ A:lost ==> R \ -\ |] ==> R"; -by (rtac ccontr 1); -by (rtac ([major, Spy_not_see_shrK] MRS rev_notE) 1); -by (swap_res_tac prems 2); -by (ALLGOALS (fast_tac (!claset addIs prems))); -qed "Spy_see_shrK_E"; +goal thy + "!!evs. evs : otway \ +\ ==> (Key (shrK A) : analz (sees lost Spy evs)) = (A : lost)"; +by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset)); +qed "Spy_analz_shrK"; +Addsimps [Spy_analz_shrK]; -bind_thm ("Spy_analz_shrK_E", - analz_subset_parts RS subsetD RS Spy_see_shrK_E); +goal thy "!!A. [| Key (shrK A) : parts (sees lost Spy evs); \ +\ evs : otway |] ==> A:lost"; +by (fast_tac (!claset addDs [Spy_see_shrK]) 1); +qed "Spy_see_shrK_D"; -AddSEs [Spy_see_shrK_E, Spy_analz_shrK_E]; +bind_thm ("Spy_analz_shrK_D", analz_subset_parts RS subsetD RS Spy_see_shrK_D); +AddSDs [Spy_see_shrK_D, Spy_analz_shrK_D]; (*** Future keys can't be seen or used! ***) @@ -139,10 +139,7 @@ goal thy "!!evs. evs : otway ==> \ \ 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 +211,7 @@ goal thy "!!evs. evs : otway ==> \ \ 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*) @@ -242,7 +237,30 @@ 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 K and NA when the Server sends this message. Also + for Oops case.*) +goal thy + "!!evs. [| Says Server B \ +\ {|NA, X, Crypt {|NB, K|} (shrK B)|} : set_of_list evs; \ +\ evs : otway |] \ +\ ==> (EX evt: otway. K = Key(newK evt)) & \ +\ (EX i. NA = Nonce i) & (EX j. NB = Nonce j)"; +by (etac rev_mp 1); +by (etac otway.induct 1); +by (ALLGOALS (fast_tac (!claset addss (!simpset)))); +qed "Says_Server_message_form"; + + +(*For proofs involving analz.*) +val analz_Fake_tac = + dtac OR2_analz_sees_Spy 4 THEN + dtac OR4_analz_sees_Spy 6 THEN + forward_tac [Says_Server_message_form] 7 THEN + assume_tac 7 THEN Full_simp_tac 7 THEN + REPEAT ((eresolve_tac [bexE, exE, conjE] ORELSE' hyp_subst_tac) 7); (**** @@ -258,40 +276,6 @@ (** 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 ==> \ -\ Crypt {|N, Key K|} (shrK A) : parts (sees lost Spy evs) & \ -\ A ~: lost --> \ -\ (EX evt:otway. K = newK evt)"; -by (etac otway.induct 1); -by parts_Fake_tac; -by (Auto_tac()); -(*Deals with Fake message*) -by (best_tac (!claset addDs [impOfSubs analz_subset_parts, - impOfSubs Fake_parts_insert]) 1); -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 |] \ -\ ==> (EX evt:otway. K = newK evt) | Key K : analz (sees lost Spy evs)"; -by (case_tac "A : lost" 1); -by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj] - addss (!simpset)) 1); -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"; - - (*Lemma for the trivial direction of the if-and-only-if*) goal thy "!!evs. (Key K : analz (Key``nE Un sEe)) --> \ @@ -307,21 +291,18 @@ \ 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, lemma])); -by (REPEAT ((eresolve_tac [bexE, disjE] ORELSE' hyp_subst_tac) 7)); -by (ALLGOALS (*Takes 28 secs*) +by (ALLGOALS (asm_simp_tac (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK] @ pushes) setloop split_tac [expand_if]))); (** LEVEL 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()); +(*OR4, OR2, Fake*) +by (EVERY (map spy_analz_tac [5,3,2])); +(*Oops, OR3, Base*) +by (REPEAT (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1)); qed_spec_mp "analz_image_newK"; @@ -335,82 +316,13 @@ qed "analz_insert_Key_newK"; -(*Describes the form of K and NA when the Server sends this message.*) -goal thy - "!!evs. [| Says Server B \ -\ {|NA, Crypt {|NA, K|} (shrK A), \ -\ Crypt {|NB, K|} (shrK B)|} : set_of_list evs; \ -\ evs : otway |] \ -\ ==> (EX evt:otway. K = Key(newK evt)) & \ -\ (EX i. NA = Nonce i) & \ -\ (EX j. NB = Nonce j)"; -by (etac rev_mp 1); -by (etac otway.induct 1); -by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset)))); -qed "Says_Server_message_form"; - - -(*Crucial security property, but not itself enough to guarantee correctness! - The need for quantification over N, C seems to indicate the problem. - Omitting the Reveal message from the description deprives us of even - this clue. *) -goal thy - "!!evs. [| A ~: lost; B ~: lost; evs : otway; evt : otway |] \ -\ ==> Says Server B \ -\ {|NA, Crypt {|NA, Key K|} (shrK A), \ -\ Crypt {|NB, Key K|} (shrK B)|} : set_of_list evs --> \ -\ (ALL N C. Says C Spy {|N, 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 (dtac Reveal_message_form 7); -by (REPEAT_FIRST (eresolve_tac [asm_rl, bexE, disjE] ORELSE' hyp_subst_tac)); -by (ALLGOALS - (asm_full_simp_tac - (!simpset addsimps ([analz_subset_parts RS contra_subsetD, - analz_insert_Key_newK] @ pushes) - setloop split_tac [expand_if]))); -(** LEVEL 6 **) -(*Reveal case 1*) -by (Fast_tac 5); -(*OR3*) -by (fast_tac (!claset addSIs [parts_insertI] - addEs [Says_imp_old_keys RS less_irrefl] - addss (!simpset addsimps [parts_insert2])) 3); -(*Reveal case 2, OR4, OR2, Fake*) -by (rtac conjI 3); -by (REPEAT (spy_analz_tac 1)); -val lemma = result() RS mp RS mp RSN(2,rev_notE); - - - -(*WEAK VERSION: NEED TO ELIMINATE QUANTIFICATION OVER N, C!!*) -goal thy - "!!evs. [| Says Server B \ -\ {|NA, Crypt {|NA, K|} (shrK A), \ -\ Crypt {|NB, K|} (shrK B)|} : set_of_list evs; \ -\ (ALL N C. Says C Spy {|N, K|} ~: set_of_list evs); \ -\ A ~: lost; B ~: lost; evs : otway |] \ -\ ==> K ~: analz (sees lost Spy evs)"; -by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); -by (fast_tac (!claset addSEs [lemma]) 1); -qed "Spy_not_see_encrypted_key"; - - -(*** Attempting to prove stronger properties ***) - -(** The Key K uniquely identifies the Server's message. **) - -fun ex_strip_tac i = REPEAT (ares_tac [exI, conjI] i) THEN assume_tac (i+1); +(*** The Key K uniquely identifies the Server's message. **) goal thy - "!!evs. evs : otway ==> \ -\ EX A' B' NA' NB'. ALL A B NA NB. \ -\ Says Server B \ -\ {|NA, Crypt {|NA, K|} (shrK A), \ -\ Crypt {|NB, K|} (shrK B)|} : set_of_list evs --> \ -\ A=A' & B=B' & NA=NA' & NB=NB'"; + "!!evs. evs : otway ==> \ +\ EX B' NA' NB' X'. ALL B NA NB X. \ +\ Says Server B {|NA, X, Crypt {|NB, K|} (shrK B)|} : set_of_list evs --> \ +\ B=B' & NA=NA' & NB=NB' & X=X'"; by (etac otway.induct 1); by (ALLGOALS (asm_simp_tac (!simpset addsimps [all_conj_distrib]))); by (Step_tac 1); @@ -426,16 +338,11 @@ val lemma = result(); goal thy - "!!evs. [| Says Server B \ -\ {|NA, Crypt {|NA, K|} (shrK A), \ -\ Crypt {|NB, K|} (shrK B)|} \ + "!!evs. [| Says Server B {|NA, X, Crypt {|NB, K|} (shrK B)|} \ \ : set_of_list evs; \ -\ Says Server B' \ -\ {|NA', Crypt {|NA', K|} (shrK A'), \ -\ Crypt {|NB', K|} (shrK B')|} \ +\ Says Server B' {|NA',X',Crypt {|NB',K|} (shrK B')|} \ \ : set_of_list evs; \ -\ evs : otway |] \ -\ ==> A=A' & B=B' & NA=NA' & NB=NB'"; +\ evs : otway |] ==> X=X' & B=B' & NA=NA' & NB=NB'"; by (dtac lemma 1); by (REPEAT (etac exE 1)); (*Duplicate the assumption*) @@ -444,59 +351,91 @@ qed "unique_session_keys"; +(*Crucial security property, but not itself enough to guarantee correctness!*) +goal thy + "!!evs. [| A ~: lost; B ~: lost; evs : otway; evt : otway |] \ +\ ==> Says Server B \ +\ {|NA, Crypt {|NA, Key K|} (shrK A), \ +\ Crypt {|NB, Key K|} (shrK B)|} : set_of_list evs --> \ +\ Says B Spy {|NA, NB, Key K|} ~: set_of_list evs --> \ +\ Key K ~: analz (sees lost Spy evs)"; +by (etac otway.induct 1); +by analz_Fake_tac; +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 addSIs [parts_insertI] + addEs [Says_imp_old_keys RS less_irrefl] + addss (!simpset addsimps [parts_insert2])) 3); +(*OR4, OR2, Fake*) +by (REPEAT_FIRST (resolve_tac [conjI, impI] ORELSE' spy_analz_tac)); +(*Oops*) (** LEVEL 5 **) +by (fast_tac (!claset delrules [disjE] + addDs [unique_session_keys] addss (!simpset)) 1); +val lemma = result() RS mp RS mp RSN(2,rev_notE); + + +goal thy + "!!evs. [| Says Server B \ +\ {|NA, Crypt {|NA, K|} (shrK A), \ +\ Crypt {|NB, K|} (shrK B)|} : set_of_list evs; \ +\ Says B Spy {|NA, NB, K|} ~: set_of_list evs; \ +\ A ~: lost; B ~: lost; evs : otway |] \ +\ ==> K ~: analz (sees lost Spy evs)"; +by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); +by (fast_tac (!claset addSEs [lemma]) 1); +qed "Spy_not_see_encrypted_key"; + + +(*** Attempting to prove stronger properties ***) + (*Only OR1 can have caused such a part of a message to appear. I'm not sure why A ~= B premise is needed: OtwayRees.ML doesn't need it. Perhaps it's because OR2 has two similar-looking encrypted messages in this version.*) goal thy - "!!evs. [| A ~: lost; A ~= B; evs : otway |] \ -\ ==> Crypt {|NA, Agent A, Agent B|} (shrK A) \ + "!!evs. [| A ~: lost; A ~= B; evs : otway |] \ +\ ==> Crypt {|NA, Agent A, Agent B|} (shrK A) \ \ : parts (sees lost Spy evs) --> \ -\ Says A B {|NA, Agent A, Agent B, \ +\ 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); +by (Fast_tac 1); qed_spec_mp "Crypt_imp_OR1"; -(*This key property is FALSE. Somebody could make a fake message to Server +(*Crucial property: If the encrypted message appears, and A has used NA + to start a run, then it originated with the Server!*) +(*Only it is FALSE. Somebody could make a fake message to Server substituting some other nonce NA' for NB.*) goal thy "!!evs. [| A ~: lost; A ~= Spy; evs : otway |] \ \ ==> Crypt {|NA, Key K|} (shrK A) : parts (sees lost Spy evs) --> \ -\ Says A B {|NA, Agent A, Agent B, \ +\ Says A B {|NA, Agent A, Agent B, \ \ Crypt {|NA, Agent A, Agent B|} (shrK A)|} \ -\ : set_of_list evs --> \ -\ (EX B NB. Says Server B \ -\ {|NA, \ +\ : set_of_list evs --> \ +\ (EX B NB. Says Server B \ +\ {|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); -(*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 **) (*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 **) +(*OR3*) (** LEVEL 5 **) by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib]))); by (step_tac (!claset delrules [disjCI, impCE]) 1); (*The hypotheses at this point suggest an attack in which nonce NA is used @@ -511,7 +450,7 @@ Crypt {|Nonce NA, Agent A, Agent B|} (shrK A)|} : set_of_list evsa *) -writeln "GIVE UP!"; +writeln "GIVE UP! on NA_Crypt_imp_Server_msg"; (*Thus the key property A_can_trust probably fails too.*) diff -r 53b6e0bc8ccf -r 3106a99d30a5 src/HOL/Auth/OtwayRees_Bad.thy --- a/src/HOL/Auth/OtwayRees_Bad.thy Sun Oct 27 13:47:02 1996 +0100 +++ b/src/HOL/Auth/OtwayRees_Bad.thy Mon Oct 28 12:55:24 1996 +0100 @@ -61,21 +61,18 @@ (*Bob receives the Server's (?) message and compares the Nonces with those in the message he previously sent the Server.*) - OR4 "[| evs: otway; A ~= B; B ~= Server; + OR4 "[| evs: otway; A ~= B; Says S B {|Nonce NA, X, Crypt {|Nonce NB, Key K|} (shrK B)|} : set_of_list evs; Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB, X''|} : set_of_list evs |] ==> Says B A {|Nonce NA, X|} # evs : otway" - (*This message models possible leaks of session keys. Alice's Nonce - identifies the protocol run.*) - Revl "[| evs: otway; 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)|} + (*This message models possible leaks of session keys. The nonces + identify the protocol run.*) + Oops "[| evs: otway; B ~= Spy; + Says Server B {|Nonce NA, X, Crypt {|Nonce NB, Key K|} (shrK B)|} : set_of_list evs |] - ==> Says A Spy {|Nonce NA, Key K|} # evs : otway" + ==> Says B Spy {|Nonce NA, Nonce NB, Key K|} # evs : otway" end