# HG changeset patch # User paulson # Date 880977138 -3600 # Node ID 34bb65b037dd298054f3c6bfecceccb81834aaf0 # Parent a5a82aaf2d76c4d85046a21b35781b47496d4a21 New guarantee B_trusts_NS5, and tidying diff -r a5a82aaf2d76 -r 34bb65b037dd src/HOL/Auth/NS_Shared.ML --- a/src/HOL/Auth/NS_Shared.ML Mon Dec 01 12:50:04 1997 +0100 +++ b/src/HOL/Auth/NS_Shared.ML Mon Dec 01 12:52:18 1997 +0100 @@ -60,10 +60,11 @@ (*For proving the easier theorems about X ~: parts (spies evs).*) fun parts_induct_tac i = - etac ns_shared.induct i THEN - forward_tac [Oops_parts_spies] (i+7) THEN - forward_tac [NS3_msg_in_parts_spies] (i+4) THEN - prove_simple_subgoals_tac i; + EVERY [etac ns_shared.induct i, + REPEAT (FIRSTGOAL analz_mono_contra_tac), + forward_tac [Oops_parts_spies] (i+7), + forward_tac [NS3_msg_in_parts_spies] (i+4), + prove_simple_subgoals_tac i]; (** Theorems of the form X ~: parts (spies evs) imply that NOBODY @@ -141,6 +142,14 @@ qed "A_trusts_NS2"; +goal thy + "!!evs. [| Crypt (shrK A) {|NA, Agent B, Key K, X|} : parts (spies evs); \ +\ A ~: bad; evs : ns_shared |] \ +\ ==> K ~: range shrK & X = (Crypt (shrK B) {|Key K, Agent A|})"; +by (blast_tac (claset() addSDs [A_trusts_NS2, Says_Server_message_form]) 1); +qed "cert_A_form"; + + (*EITHER describes the form of X when the following message is sent, OR reduces it to the Fake case. Use Says_Server_message_form if applicable.*) @@ -153,8 +162,7 @@ by (case_tac "A : bad" 1); by (fast_tac (claset() addSDs [Says_imp_spies RS analz.Inj] addss (simpset())) 1); -by (forward_tac [Says_imp_spies RS parts.Inj] 1); -by (blast_tac (claset() addSDs [A_trusts_NS2, Says_Server_message_form]) 1); +by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj, cert_A_form]) 1); qed "Says_S_message_form"; @@ -172,7 +180,6 @@ Key K : analz (spies evs) A more general formula must be proved inductively. - ****) @@ -291,8 +298,8 @@ (*Final version: Server's message in the most abstract form*) goal thy "!!evs. [| Says Server A \ -\ (Crypt K' {|NA, Agent B, Key K, X|}) : set evs; \ -\ (ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs); \ +\ (Crypt K' {|NA, Agent B, Key K, X|}) : set evs; \ +\ ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs; \ \ A ~: bad; B ~: bad; evs : ns_shared \ \ |] ==> Key K ~: analz (spies evs)"; by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); @@ -322,42 +329,112 @@ goal thy - "!!evs. [| B ~: bad; evs : ns_shared |] \ -\ ==> Key K ~: analz (spies evs) --> \ -\ Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|}) \ -\ : set evs --> \ -\ Crypt K (Nonce NB) : parts (spies evs) --> \ -\ Says B A (Crypt K (Nonce NB)) : set evs"; -by (etac ns_shared.induct 1); -by (forward_tac [Says_S_message_form] 5 THEN assume_tac 5); -by (dtac NS3_msg_in_parts_spies 5); -by (forward_tac [Oops_parts_spies] 8); -by (REPEAT (FIRSTGOAL analz_mono_contra_tac)); -by (ALLGOALS (asm_simp_tac (simpset() addsimps [all_conj_distrib]))); -(**LEVEL 6**) + "!!evs. [| Crypt K (Nonce NB) : parts (spies evs); \ +\ Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|}) \ +\ : set evs; \ +\ Key K ~: analz (spies evs); \ +\ evs : ns_shared |] \ +\ ==> Says B A (Crypt K (Nonce NB)) : set evs"; +by (etac rev_mp 1); +by (etac rev_mp 1); +by (etac rev_mp 1); +by (parts_induct_tac 1); (*NS3*) by (Blast_tac 3); by (Fake_parts_insert_tac 1); -by (ALLGOALS Clarify_tac); (*NS2: contradiction from the assumptions - Key K ~: used evsa and Crypt K (Nonce NB) : parts (spies evsa) *) -by (dtac Crypt_imp_invKey_keysFor 1); -by (Asm_full_simp_tac 1); -(*NS4*) (**LEVEL 11**) -by (case_tac "Ba : bad" 1); + Key K ~: used evs2 and Crypt K (Nonce NB) : parts (spies evs2) *) +by (blast_tac (claset() addSEs [new_keys_not_used RSN (2,rev_notE)] + addSDs [Crypt_imp_keysFor]) 1); +(**LEVEL 7**) +(*NS4*) +by (Clarify_tac 1); +by (not_bad_tac "Ba" 1); by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS B_trusts_NS3, - unique_session_keys]) 2); -by (blast_tac (claset() addDs [Says_imp_spies RS analz.Inj RS - Crypt_Spy_analz_bad]) 1); -val lemma = result(); + unique_session_keys]) 1); +qed "A_trusts_NS4_lemma"; + +(*This version no longer assumes that K is secure*) goal thy "!!evs. [| Crypt K (Nonce NB) : parts (spies evs); \ -\ Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|}) \ -\ : set evs; \ +\ Crypt (shrK A) {|NA, Agent B, Key K, X|} : parts (spies evs); \ \ ALL NB. Says A Spy {|NA, NB, Key K|} ~: set evs; \ \ A ~: bad; B ~: bad; evs : ns_shared |] \ \ ==> Says B A (Crypt K (Nonce NB)) : set evs"; -by (blast_tac (claset() addSIs [lemma RS mp RS mp RS mp] +by (blast_tac (claset() addSIs [A_trusts_NS2, A_trusts_NS4_lemma] addSEs [Spy_not_see_encrypted_key RSN (2,rev_notE)]) 1); qed "A_trusts_NS4"; + + +(*If the session key has been used in NS4 then somebody has forwarded + component X in some instance of NS4. Perhaps an interesting property, + but not needed (after all) for the proofs below.*) +goal thy + "!!evs. [| Crypt K (Nonce NB) : parts (spies evs); \ +\ Says Server A (Crypt (shrK A) {|NA, Agent B, Key K, X|}) \ +\ : set evs; \ +\ Key K ~: analz (spies evs); \ +\ evs : ns_shared |] \ +\ ==> EX A'. Says A' B X : set evs"; +by (etac rev_mp 1); +by (etac rev_mp 1); +by (etac rev_mp 1); +by (parts_induct_tac 1); +by (ALLGOALS (asm_simp_tac (simpset() addsimps [ex_disj_distrib]))); +by (ALLGOALS Clarify_tac); +by (Fake_parts_insert_tac 1); +(**LEVEL 7**) +(*NS2*) +by (blast_tac (claset() addSEs [new_keys_not_used RSN (2,rev_notE)] + addSDs [Crypt_imp_keysFor]) 1); +(*NS4*) +by (not_bad_tac "Ba" 1); +by (Asm_full_simp_tac 1); +by (forward_tac [Says_imp_spies RS parts.Inj RS B_trusts_NS3] 1); +by (ALLGOALS Clarify_tac); +by (blast_tac (claset() addDs [unique_session_keys]) 1); +qed "NS4_implies_NS3"; + + +goal thy + "!!evs. [| B ~: bad; evs : ns_shared |] \ +\ ==> Key K ~: analz (spies evs) --> \ +\ Says Server A \ +\ (Crypt (shrK A) {|NA, Agent B, Key K, \ +\ Crypt (shrK B) {|Key K, Agent A|}|}) \ +\ : set evs --> \ +\ Says B A (Crypt K (Nonce NB)) : set evs --> \ +\ Crypt K {|Nonce NB, Nonce NB|} : parts (spies evs) --> \ +\ Says A B (Crypt K {|Nonce NB, Nonce NB|}) : set evs"; +by (parts_induct_tac 1); +(*NS4*) +by (blast_tac (claset() addSEs spies_partsEs) 4); +(*NS3*) +by (blast_tac (claset() addSDs [Says_imp_spies RS parts.Inj, cert_A_form]) 3); +(*NS2*) +by (blast_tac (claset() addSEs [new_keys_not_used RSN (2,rev_notE)] + addSDs [Crypt_imp_keysFor]) 2); +by (Fake_parts_insert_tac 1); +(**LEVEL 5**) +(*NS5*) +by (Clarify_tac 1); +by (not_bad_tac "Aa" 1); +by (blast_tac (claset() addDs [Says_imp_spies RS parts.Inj RS A_trusts_NS2, + unique_session_keys]) 1); +val lemma = result(); + + +(*Very strong Oops condition reveals protocol's weakness*) +goal thy + "!!evs. [| Crypt K {|Nonce NB, Nonce NB|} : parts (spies evs); \ +\ Says B A (Crypt K (Nonce NB)) : set evs; \ +\ Crypt (shrK B) {|Key K, Agent A|} : parts (spies evs); \ +\ ALL NA NB. Says A Spy {|NA, NB, Key K|} ~: set evs; \ +\ A ~: bad; B ~: bad; evs : ns_shared |] \ +\ ==> Says A B (Crypt K {|Nonce NB, Nonce NB|}) : set evs"; +by (dtac B_trusts_NS3 1); +by (ALLGOALS Clarify_tac); +by (blast_tac (claset() addSIs [normalize_thm [RSspec, RSmp] lemma] + addSEs [Spy_not_see_encrypted_key RSN (2,rev_notE)]) 1); +qed "B_trusts_NS5";