# HG changeset patch # User paulson # Date 849805647 -3600 # Node ID 6d3f7c7f70b0990a1cae7b3730e975124513aa3c # Parent 672015b535d774098436b64202e1142959c61829 Public-key examples diff -r 672015b535d7 -r 6d3f7c7f70b0 src/HOL/Auth/NS_Public.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Auth/NS_Public.ML Thu Dec 05 18:07:27 1996 +0100 @@ -0,0 +1,438 @@ +(* Title: HOL/Auth/NS_Public + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1996 University of Cambridge + +Inductive relation "ns_public" for the Needham-Schroeder Public-Key protocol. +Version incorporating Lowe's fix (inclusion of B's identify in round 2). +*) + +open NS_Public; + +proof_timing:=true; +HOL_quantifiers := false; +Pretty.setdepth 20; + +AddIffs [Spy_in_lost]; + +(*Replacing the variable by a constant improves search speed by 50%!*) +val Says_imp_sees_Spy' = + read_instantiate_sg (sign_of thy) [("lost","lost")] Says_imp_sees_Spy; + + +(*A "possibility property": there are traces that reach the end*) +goal thy + "!!A B. A ~= B ==> EX NB. EX evs: ns_public. \ +\ Says A B (Crypt (pubK B) (Nonce NB)) : set_of_list evs"; +by (REPEAT (resolve_tac [exI,bexI] 1)); +by (rtac (ns_public.Nil RS ns_public.NS1 RS ns_public.NS2 RS ns_public.NS3) 2); +by (ALLGOALS (simp_tac (!simpset setsolver safe_solver))); +by (REPEAT_FIRST (resolve_tac [refl, conjI])); +by (REPEAT_FIRST (fast_tac (!claset addss (!simpset setsolver safe_solver)))); +result(); + + +(**** Inductive proofs about ns_public ****) + +(*Nobody sends themselves messages*) +goal thy "!!evs. evs : ns_public ==> ALL A X. Says A A X ~: set_of_list evs"; +by (etac ns_public.induct 1); +by (Auto_tac()); +qed_spec_mp "not_Says_to_self"; +Addsimps [not_Says_to_self]; +AddSEs [not_Says_to_self RSN (2, rev_notE)]; + + +(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *) +fun parts_induct_tac i = SELECT_GOAL + (DETERM (etac ns_public.induct 1 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 private key! (unless it's lost at start)*) +goal thy + "!!evs. evs : ns_public \ +\ ==> (Key (priK A) : parts (sees lost Spy evs)) = (A : lost)"; +by (parts_induct_tac 1); +by (Auto_tac()); +qed "Spy_see_priK"; +Addsimps [Spy_see_priK]; + +goal thy + "!!evs. evs : ns_public \ +\ ==> (Key (priK A) : analz (sees lost Spy evs)) = (A : lost)"; +by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset)); +qed "Spy_analz_priK"; +Addsimps [Spy_analz_priK]; + +goal thy "!!A. [| Key (priK A) : parts (sees lost Spy evs); \ +\ evs : ns_public |] ==> A:lost"; +by (fast_tac (!claset addDs [Spy_see_priK]) 1); +qed "Spy_see_priK_D"; + +bind_thm ("Spy_analz_priK_D", analz_subset_parts RS subsetD RS Spy_see_priK_D); +AddSDs [Spy_see_priK_D, Spy_analz_priK_D]; + + +(*** Future nonces can't be seen or used! ***) + +goal thy "!!evs. evs : ns_public ==> \ +\ length evs <= length evt --> \ +\ Nonce (newN evt) ~: parts (sees lost Spy evs)"; +by (parts_induct_tac 1); +by (REPEAT_FIRST (fast_tac (!claset + addSEs partsEs + addSDs [Says_imp_sees_Spy' RS parts.Inj] + addEs [leD RS notE] + addDs [impOfSubs analz_subset_parts, + impOfSubs parts_insert_subset_Un, + Suc_leD] + addss (!simpset)))); +qed_spec_mp "new_nonces_not_seen"; +Addsimps [new_nonces_not_seen]; + +val nonce_not_seen_now = le_refl RSN (2, new_nonces_not_seen) RSN (2,rev_notE); + + +(**** Authenticity properties obtained from NS2 ****) + +(*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce + is secret. (Honest users generate fresh nonces.)*) +goal thy + "!!evs. evs : ns_public \ +\ ==> Nonce NA ~: analz (sees lost Spy evs) --> \ +\ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs) --> \ +\ Crypt (pubK C) {|X, Nonce NA, Agent D|} ~: parts (sees lost Spy evs)"; +by (etac ns_public.induct 1); +by (ALLGOALS + (asm_simp_tac + (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes) + setloop split_tac [expand_if]))); +(*NS3*) +by (fast_tac (!claset addSEs partsEs + addEs [nonce_not_seen_now]) 4); +(*NS2*) +by (fast_tac (!claset addSEs partsEs + addEs [nonce_not_seen_now]) 3); +(*Fake*) +by (best_tac (!claset addIs [impOfSubs (subset_insertI RS analz_mono)] + addDs [impOfSubs analz_subset_parts, + impOfSubs Fake_parts_insert] + addss (!simpset)) 2); +(*Base*) +by (fast_tac (!claset addDs [impOfSubs analz_subset_parts] + addss (!simpset)) 1); +bind_thm ("no_nonce_NS1_NS2", result() RSN (2, rev_mp) RSN (2, rev_mp)); + + +(*Uniqueness for NS1: nonce NA identifies agents A and B*) +goal thy + "!!evs. evs : ns_public \ +\ ==> Nonce NA ~: analz (sees lost Spy evs) --> \ +\ (EX A' B'. ALL A B. \ +\ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs) --> \ +\ A=A' & B=B')"; +by (etac ns_public.induct 1); +by (ALLGOALS + (asm_simp_tac + (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes) + setloop split_tac [expand_if]))); +(*NS1*) +by (expand_case_tac "NA = ?y" 3 THEN + REPEAT (fast_tac (!claset addSEs (nonce_not_seen_now::partsEs)) 3)); +(*Base*) +by (fast_tac (!claset addss (!simpset)) 1); +(*Fake*) +by (simp_tac (!simpset addsimps [all_conj_distrib,parts_insert_sees]) 1); +by (step_tac (!claset addSIs [impOfSubs (subset_insertI RS analz_mono)]) 1); +by (ex_strip_tac 1); +by (best_tac (!claset delrules [conjI] + addDs [impOfSubs analz_subset_parts, + impOfSubs Fake_parts_insert] + addss (!simpset)) 1); +val lemma = result(); + +goal thy + "!!evs. [| Crypt(pubK B) {|Nonce NA, Agent A|} : parts(sees lost Spy evs); \ +\ Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(sees lost Spy evs); \ +\ Nonce NA ~: analz (sees lost Spy evs); \ +\ evs : ns_public |] \ +\ ==> A=A' & B=B'"; +by (dtac lemma 1); +by (mp_tac 1); +by (REPEAT (etac exE 1)); +(*Duplicate the assumption*) +by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1); +by (fast_tac (!claset addSDs [spec]) 1); +qed "unique_NA"; + + +(*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*) +goal thy + "!!evs. [| A ~: lost; B ~: lost; evs : ns_public |] \ +\ ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs \ +\ --> Nonce NA ~: analz (sees lost Spy evs)"; +by (etac ns_public.induct 1); +by (ALLGOALS + (asm_simp_tac + (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes) + setloop split_tac [expand_if]))); +(*NS3*) +by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] + addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4); +(*NS1*) +by (fast_tac (!claset addSEs partsEs + addSDs [new_nonces_not_seen, + Says_imp_sees_Spy' RS parts.Inj]) 2); +(*Fake*) +by (REPEAT_FIRST (rtac conjI ORELSE' spy_analz_tac)); +(*NS2*) +by (Step_tac 1); +by (fast_tac (!claset addSEs partsEs + addSDs [new_nonces_not_seen, + Says_imp_sees_Spy' RS parts.Inj]) 2); +by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] + addDs [unique_NA]) 1); +bind_thm ("Spy_not_see_NA", result() RSN (2, rev_mp)); + + +(*Authentication for A: if she receives message 2 and has used NA + to start a run, then B has sent message 2.*) +goal thy + "!!evs. [| A ~: lost; B ~: lost; evs : ns_public |] \ +\ ==> Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|} \ +\ : parts (sees lost Spy evs) \ +\ --> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs \ +\ --> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \ +\ : set_of_list evs"; +by (etac ns_public.induct 1); +by (ALLGOALS Asm_simp_tac); +(*NS1*) +by (fast_tac (!claset addSEs partsEs + addSDs [new_nonces_not_seen, + Says_imp_sees_Spy' RS parts.Inj]) 2); +(*Fake*) +by (REPEAT_FIRST (resolve_tac [impI, conjI])); +by (fast_tac (!claset addss (!simpset)) 1); +by (forward_tac [Spy_not_see_NA] 1 THEN REPEAT (assume_tac 1)); +by (best_tac (!claset addSIs [disjI2] + addDs [impOfSubs analz_subset_parts, + impOfSubs Fake_parts_insert] + addss (!simpset)) 1); +qed_spec_mp "NA_decrypt_imp_B_msg"; + +(*Corollary: if A receives B's message NS2 and the nonce NA agrees + then that message really originated with B.*) +goal thy + "!!evs. [| Says B' A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|}) \ +\ : set_of_list evs;\ +\ Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs;\ +\ A ~: lost; B ~: lost; evs : ns_public |] \ +\ ==> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|}) \ +\ : set_of_list evs"; +by (fast_tac (!claset addSIs [NA_decrypt_imp_B_msg] + addEs partsEs + addDs [Says_imp_sees_Spy' RS parts.Inj]) 1); +qed "A_trusts_NS2"; + +(*If the encrypted message appears then it originated with Alice in NS1*) +goal thy + "!!evs. evs : ns_public \ +\ ==> Nonce NA ~: analz (sees lost Spy evs) --> \ +\ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs) --> \ +\ Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs"; +by (etac ns_public.induct 1); +by (ALLGOALS + (asm_simp_tac + (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes) + setloop split_tac [expand_if]))); +(*Fake*) +by (best_tac (!claset addSIs [disjI2] + addIs [impOfSubs (subset_insertI RS analz_mono)] + addDs [impOfSubs analz_subset_parts, + impOfSubs Fake_parts_insert] + addss (!simpset)) 2); +(*Base*) +by (fast_tac (!claset addss (!simpset)) 1); +qed_spec_mp "B_trusts_NS1"; + + + +(**** Authenticity properties obtained from NS2 ****) + +(*Uniqueness for NS2: nonce NB identifies nonce NA and agents A, B + [unicity of B makes Lowe's fix work] + [proof closely follows that for unique_NA] *) +goal thy + "!!evs. evs : ns_public \ +\ ==> Nonce NB ~: analz (sees lost Spy evs) --> \ +\ (EX A' NA' B'. ALL A NA B. \ +\ Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|} \ +\ : parts (sees lost Spy evs) --> A=A' & NA=NA' & B=B')"; +by (etac ns_public.induct 1); +by (ALLGOALS + (asm_simp_tac + (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes) + setloop split_tac [expand_if]))); +(*NS2*) +by (expand_case_tac "NB = ?y" 3 THEN + REPEAT (fast_tac (!claset addSEs (nonce_not_seen_now::partsEs)) 3)); +(*Base*) +by (fast_tac (!claset addss (!simpset)) 1); +(*Fake*) +by (simp_tac (!simpset addsimps [all_conj_distrib,parts_insert_sees]) 1); +by (step_tac (!claset addSIs [impOfSubs (subset_insertI RS analz_mono)]) 1); +by (ex_strip_tac 1); +by (best_tac (!claset delrules [conjI] + addDs [impOfSubs analz_subset_parts, + impOfSubs Fake_parts_insert] + addss (!simpset)) 1); +val lemma = result(); + +goal thy + "!!evs. [| Crypt(pubK A) {|Nonce NA, Nonce NB, Agent B|} \ +\ : parts(sees lost Spy evs); \ +\ Crypt(pubK A') {|Nonce NA', Nonce NB, Agent B'|} \ +\ : parts(sees lost Spy evs); \ +\ Nonce NB ~: analz (sees lost Spy evs); \ +\ evs : ns_public |] \ +\ ==> A=A' & NA=NA' & B=B'"; +by (dtac lemma 1); +by (mp_tac 1); +by (REPEAT (etac exE 1)); +(*Duplicate the assumption*) +by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1); +by (fast_tac (!claset addSDs [spec]) 1); +qed "unique_NB"; + + +(*Secrecy: Spy does not see the nonce sent in msg NS2 if A and B are secure*) +goal thy + "!!evs. [| A ~: lost; B ~: lost; evs : ns_public |] \ +\ ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \ +\ : set_of_list evs \ +\ --> Nonce NB ~: analz (sees lost Spy evs)"; +by (etac ns_public.induct 1); +by (ALLGOALS + (asm_simp_tac + (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes) + setloop split_tac [expand_if]))); +(*NS3*) +by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] + addDs [unique_NB]) 4); +(*NS1*) +by (fast_tac (!claset addSEs partsEs + addSDs [new_nonces_not_seen, + Says_imp_sees_Spy' RS parts.Inj]) 2); +(*Fake*) +by (REPEAT_FIRST (rtac conjI ORELSE' spy_analz_tac)); +(*NS2*) +by (Step_tac 1); +by (fast_tac (!claset addSEs partsEs + addSDs [new_nonces_not_seen, + Says_imp_sees_Spy' RS parts.Inj]) 2); +by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] + addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 1); +bind_thm ("Spy_not_see_NB", result() RSN (2, rev_mp)); + + +(*Matches only NS2, not NS1 (or NS3)*) +val Says_imp_sees_Spy'' = + read_instantiate [("X","Crypt ?K {|?XX,?YY,?ZZ|}")] Says_imp_sees_Spy'; + + +(*Authentication for B: if he receives message 3 and has used NB + in message 2, then A has sent message 3.*) +goal thy + "!!evs. [| A ~: lost; B ~: lost; evs : ns_public |] \ +\ ==> Crypt (pubK B) (Nonce NB) : parts (sees lost Spy evs) \ +\ --> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \ +\ : set_of_list evs \ +\ --> Says A B (Crypt (pubK B) (Nonce NB)) : set_of_list evs"; +by (etac ns_public.induct 1); +by (ALLGOALS Asm_simp_tac); +(*NS1*) +by (fast_tac (!claset addSEs partsEs + addSDs [new_nonces_not_seen, + Says_imp_sees_Spy' RS parts.Inj]) 2); +(*Fake*) +by (REPEAT_FIRST (resolve_tac [impI, conjI])); +by (fast_tac (!claset addss (!simpset)) 1); +by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1)); +by (best_tac (!claset addSIs [disjI2] + addDs [impOfSubs analz_subset_parts, + impOfSubs Fake_parts_insert] + addss (!simpset)) 1); +(*NS3*) +by (Step_tac 1); +by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1)); +by (best_tac (!claset addSDs [Says_imp_sees_Spy'' RS parts.Inj] + addDs [unique_NB]) 1); +qed_spec_mp "NB_decrypt_imp_A_msg"; + +(*Corollary: if B receives message NS3 and the nonce NB agrees + then that message really originated with A.*) +goal thy + "!!evs. [| Says A' B (Crypt (pubK B) (Nonce NB)): set_of_list evs; \ +\ Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \ +\ : set_of_list evs; \ +\ A ~: lost; B ~: lost; evs : ns_public |] \ +\ ==> Says A B (Crypt (pubK B) (Nonce NB)) : set_of_list evs"; +by (fast_tac (!claset addSIs [NB_decrypt_imp_A_msg] + addEs partsEs + addDs [Says_imp_sees_Spy' RS parts.Inj]) 1); +qed "B_trusts_NS3"; + + +(**** Overall guarantee for B*) + +(*If B receives NS3 and the nonce NB agrees with the nonce he joined with + NA, then A initiated the run using NA. + SAME PROOF AS NB_decrypt_imp_A_msg*) +goal thy + "!!evs. [| A ~: lost; B ~: lost; evs : ns_public |] \ +\ ==> Crypt (pubK B) (Nonce NB) : parts (sees lost Spy evs) \ +\ --> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \ +\ : set_of_list evs \ +\ --> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs"; +by (etac ns_public.induct 1); +by (ALLGOALS Asm_simp_tac); +(*Fake, NS2, NS3*) +(*NS1*) +by (fast_tac (!claset addSEs partsEs + addSDs [new_nonces_not_seen, + Says_imp_sees_Spy' RS parts.Inj]) 2); +(*Fake*) +by (REPEAT_FIRST (resolve_tac [impI, conjI])); +by (fast_tac (!claset addss (!simpset)) 1); +by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1)); +by (best_tac (!claset addSIs [disjI2] + addDs [impOfSubs analz_subset_parts, + impOfSubs Fake_parts_insert] + addss (!simpset)) 1); +(*NS3*) +by (Step_tac 1); +by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1)); +by (best_tac (!claset addSDs [Says_imp_sees_Spy'' RS parts.Inj] + addDs [unique_NB]) 1); +val lemma = result() RSN (2, rev_mp) RSN (2, rev_mp); + +goal thy + "!!evs. [| Says A' B (Crypt (pubK B) (Nonce NB)): set_of_list evs; \ +\ Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) \ +\ : set_of_list evs; \ +\ A ~: lost; B ~: lost; evs : ns_public |] \ +\ ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs"; +by (fast_tac (!claset addSIs [lemma] + addEs partsEs + addDs [Says_imp_sees_Spy' RS parts.Inj]) 1); +qed_spec_mp "B_trusts_protocol"; + diff -r 672015b535d7 -r 6d3f7c7f70b0 src/HOL/Auth/NS_Public.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Auth/NS_Public.thy Thu Dec 05 18:07:27 1996 +0100 @@ -0,0 +1,52 @@ +(* Title: HOL/Auth/NS_Public + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1996 University of Cambridge + +Inductive relation "ns_public" for the Needham-Schroeder Public-Key protocol. +Version incorporating Lowe's fix (inclusion of B's identify in round 2). +*) + +NS_Public = Public + + +consts lost :: agent set (*No need for it to be a variable*) + ns_public :: event list set +inductive ns_public + intrs + (*Initial trace is empty*) + Nil "[]: ns_public" + + (*The spy MAY say anything he CAN say. We do not expect him to + invent new nonces here, but he can also use NS1. Common to + all similar protocols.*) + Fake "[| evs: ns_public; B ~= Spy; + X: synth (analz (sees lost Spy evs)) |] + ==> Says Spy B X # evs : ns_public" + + (*Alice initiates a protocol run, sending a nonce to Bob*) + NS1 "[| evs: ns_public; A ~= B |] + ==> Says A B (Crypt (pubK B) {|Nonce (newN evs), Agent A|}) # evs + : ns_public" + + (*Bob responds to Alice's message with a further nonce*) + NS2 "[| evs: ns_public; A ~= B; + Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|}) + : set_of_list evs |] + ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce (newN evs), Agent B|}) + # evs : ns_public" + + (*Alice proves her existence by sending NB back to Bob.*) + NS3 "[| evs: ns_public; A ~= B; + Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB, Agent B|}) + : set_of_list evs; + Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) + : set_of_list evs |] + ==> Says A B (Crypt (pubK B) (Nonce NB)) # evs : ns_public" + + (**Oops message??**) + +rules + (*Spy has access to his own key for spoof messages*) + Spy_in_lost "Spy: lost" + +end diff -r 672015b535d7 -r 6d3f7c7f70b0 src/HOL/Auth/NS_Public_Bad.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Auth/NS_Public_Bad.ML Thu Dec 05 18:07:27 1996 +0100 @@ -0,0 +1,453 @@ +(* Title: HOL/Auth/NS_Public_Bad + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1996 University of Cambridge + +Inductive relation "ns_public" for the Needham-Schroeder Public-Key protocol. +Flawed version, vulnerable to Lowe's attack. + +From page 260 of + Burrows, Abadi and Needham. A Logic of Authentication. + Proc. Royal Soc. 426 (1989) +*) + +open NS_Public_Bad; + +proof_timing:=true; +HOL_quantifiers := false; +Pretty.setdepth 20; + +AddIffs [Spy_in_lost]; + +(*Replacing the variable by a constant improves search speed by 50%!*) +val Says_imp_sees_Spy' = + read_instantiate_sg (sign_of thy) [("lost","lost")] Says_imp_sees_Spy; + + +(*A "possibility property": there are traces that reach the end*) +goal thy + "!!A B. [| A ~= B |] \ +\ ==> EX NB. EX evs: ns_public. \ +\ Says A B (Crypt (pubK B) (Nonce NB)) : set_of_list evs"; +by (REPEAT (resolve_tac [exI,bexI] 1)); +by (rtac (ns_public.Nil RS ns_public.NS1 RS ns_public.NS2 RS ns_public.NS3) 2); +by (ALLGOALS (simp_tac (!simpset setsolver safe_solver))); +by (REPEAT_FIRST (resolve_tac [refl, conjI])); +by (REPEAT_FIRST (fast_tac (!claset addss (!simpset setsolver safe_solver)))); +result(); + + +(**** Inductive proofs about ns_public ****) + +(*Nobody sends themselves messages*) +goal thy "!!evs. evs : ns_public ==> ALL A X. Says A A X ~: set_of_list evs"; +by (etac ns_public.induct 1); +by (Auto_tac()); +qed_spec_mp "not_Says_to_self"; +Addsimps [not_Says_to_self]; +AddSEs [not_Says_to_self RSN (2, rev_notE)]; + + +(*For proving the easier theorems about X ~: parts (sees lost Spy evs) *) +fun parts_induct_tac i = SELECT_GOAL + (DETERM (etac ns_public.induct 1 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 private key! (unless it's lost at start)*) +goal thy + "!!evs. evs : ns_public \ +\ ==> (Key (priK A) : parts (sees lost Spy evs)) = (A : lost)"; +by (parts_induct_tac 1); +by (Auto_tac()); +qed "Spy_see_priK"; +Addsimps [Spy_see_priK]; + +goal thy + "!!evs. evs : ns_public \ +\ ==> (Key (priK A) : analz (sees lost Spy evs)) = (A : lost)"; +by (auto_tac(!claset addDs [impOfSubs analz_subset_parts], !simpset)); +qed "Spy_analz_priK"; +Addsimps [Spy_analz_priK]; + +goal thy "!!A. [| Key (priK A) : parts (sees lost Spy evs); \ +\ evs : ns_public |] ==> A:lost"; +by (fast_tac (!claset addDs [Spy_see_priK]) 1); +qed "Spy_see_priK_D"; + +bind_thm ("Spy_analz_priK_D", analz_subset_parts RS subsetD RS Spy_see_priK_D); +AddSDs [Spy_see_priK_D, Spy_analz_priK_D]; + + +(*** Future nonces can't be seen or used! ***) + +goal thy "!!evs. evs : ns_public ==> \ +\ length evs <= length evt --> \ +\ Nonce (newN evt) ~: parts (sees lost Spy evs)"; +by (parts_induct_tac 1); +by (REPEAT_FIRST (fast_tac (!claset + addSEs partsEs + addSDs [Says_imp_sees_Spy' RS parts.Inj] + addEs [leD RS notE] + addDs [impOfSubs analz_subset_parts, + impOfSubs parts_insert_subset_Un, + Suc_leD] + addss (!simpset)))); +qed_spec_mp "new_nonces_not_seen"; +Addsimps [new_nonces_not_seen]; + +val nonce_not_seen_now = le_refl RSN (2, new_nonces_not_seen) RSN (2,rev_notE); + + +(**** Authenticity properties obtained from NS2 ****) + +(*It is impossible to re-use a nonce in both NS1 and NS2, provided the nonce + is secret. (Honest users generate fresh nonces.)*) +goal thy + "!!evs. evs : ns_public \ +\ ==> Nonce NA ~: analz (sees lost Spy evs) --> \ +\ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs) --> \ +\ Crypt (pubK C) {|NA', Nonce NA|} ~: parts (sees lost Spy evs)"; +by (etac ns_public.induct 1); +by (ALLGOALS + (asm_simp_tac + (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes) + setloop split_tac [expand_if]))); +(*NS3*) +by (fast_tac (!claset addSEs partsEs + addEs [nonce_not_seen_now]) 4); +(*NS2*) +by (fast_tac (!claset addSEs partsEs + addEs [nonce_not_seen_now]) 3); +(*Fake*) +by (best_tac (!claset addIs [impOfSubs (subset_insertI RS analz_mono)] + addDs [impOfSubs analz_subset_parts, + impOfSubs Fake_parts_insert] + addss (!simpset)) 2); +(*Base*) +by (fast_tac (!claset addDs [impOfSubs analz_subset_parts] + addss (!simpset)) 1); +bind_thm ("no_nonce_NS1_NS2", result() RSN (2, rev_mp) RSN (2, rev_mp)); + + +(*Uniqueness for NS1: nonce NA identifies agents A and B*) +goal thy + "!!evs. evs : ns_public \ +\ ==> Nonce NA ~: analz (sees lost Spy evs) --> \ +\ (EX A' B'. ALL A B. \ +\ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs) --> \ +\ A=A' & B=B')"; +by (etac ns_public.induct 1); +by (ALLGOALS + (asm_simp_tac + (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes) + setloop split_tac [expand_if]))); +(*NS1*) +by (expand_case_tac "NA = ?y" 3 THEN + REPEAT (fast_tac (!claset addSEs (nonce_not_seen_now::partsEs)) 3)); +(*Base*) +by (fast_tac (!claset addss (!simpset)) 1); +(*Fake*) +by (simp_tac (!simpset addsimps [all_conj_distrib,parts_insert_sees]) 1); +by (step_tac (!claset addSIs [impOfSubs (subset_insertI RS analz_mono)]) 1); +by (ex_strip_tac 1); +by (best_tac (!claset delrules [conjI] + addDs [impOfSubs analz_subset_parts, + impOfSubs Fake_parts_insert] + addss (!simpset)) 1); +val lemma = result(); + +goal thy + "!!evs. [| Crypt(pubK B) {|Nonce NA, Agent A|} : parts(sees lost Spy evs); \ +\ Crypt(pubK B') {|Nonce NA, Agent A'|} : parts(sees lost Spy evs); \ +\ Nonce NA ~: analz (sees lost Spy evs); \ +\ evs : ns_public |] \ +\ ==> A=A' & B=B'"; +by (dtac lemma 1); +by (mp_tac 1); +by (REPEAT (etac exE 1)); +(*Duplicate the assumption*) +by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1); +by (fast_tac (!claset addSDs [spec]) 1); +qed "unique_NA"; + + +(*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*) +goal thy + "!!evs. [| A ~: lost; B ~: lost; evs : ns_public |] \ +\ ==> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs \ +\ --> Nonce NA ~: analz (sees lost Spy evs)"; +by (etac ns_public.induct 1); +by (ALLGOALS + (asm_simp_tac + (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes) + setloop split_tac [expand_if]))); +(*NS3*) +by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] + addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 4); +(*NS1*) +by (fast_tac (!claset addSEs partsEs + addSDs [new_nonces_not_seen, + Says_imp_sees_Spy' RS parts.Inj]) 2); +(*Fake*) +by (REPEAT_FIRST (rtac conjI ORELSE' spy_analz_tac)); +(*NS2*) +by (Step_tac 1); +by (fast_tac (!claset addSEs partsEs + addSDs [new_nonces_not_seen, + Says_imp_sees_Spy' RS parts.Inj]) 2); +by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] + addDs [unique_NA]) 1); +bind_thm ("Spy_not_see_NA", result() RSN (2, rev_mp)); + + +(*Authentication for A: if she receives message 2 and has used NA + to start a run, then B has sent message 2.*) +goal thy + "!!evs. [| A ~: lost; B ~: lost; evs : ns_public |] \ +\ ==> Crypt (pubK A) {|Nonce NA, Nonce NB|} : parts (sees lost Spy evs) \ +\ --> Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs \ +\ --> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set_of_list evs"; +by (etac ns_public.induct 1); +by (ALLGOALS Asm_simp_tac); +(*NS1*) +by (fast_tac (!claset addSEs partsEs + addSDs [new_nonces_not_seen, + Says_imp_sees_Spy' RS parts.Inj]) 2); +(*Fake*) +by (REPEAT_FIRST (resolve_tac [impI, conjI])); +by (fast_tac (!claset addss (!simpset)) 1); +by (forward_tac [Spy_not_see_NA] 1 THEN REPEAT (assume_tac 1)); +by (best_tac (!claset addDs [impOfSubs analz_subset_parts, + impOfSubs Fake_parts_insert] + addss (!simpset)) 1); +(*NS2*) +by (Step_tac 1); +by (forward_tac [Spy_not_see_NA] 1 THEN REPEAT (assume_tac 1)); +by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] + addDs [unique_NA]) 1); +qed_spec_mp "NA_decrypt_imp_B_msg"; + +(*Corollary: if A receives B's message NS2 and the nonce NA agrees + then that message really originated with B.*) +goal thy + "!!evs. [| Says B' A (Crypt(pubK A) {|Nonce NA, Nonce NB|}): set_of_list evs;\ +\ Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs;\ +\ A ~: lost; B ~: lost; evs : ns_public |] \ +\ ==> Says B A (Crypt(pubK A) {|Nonce NA, Nonce NB|}): set_of_list evs"; +by (fast_tac (!claset addSIs [NA_decrypt_imp_B_msg] + addEs partsEs + addDs [Says_imp_sees_Spy' RS parts.Inj]) 1); +qed "A_trusts_NS2"; + +(*If the encrypted message appears then it originated with Alice in NS1*) +goal thy + "!!evs. evs : ns_public \ +\ ==> Nonce NA ~: analz (sees lost Spy evs) --> \ +\ Crypt (pubK B) {|Nonce NA, Agent A|} : parts (sees lost Spy evs) --> \ +\ Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) : set_of_list evs"; +by (etac ns_public.induct 1); +by (ALLGOALS + (asm_simp_tac + (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes) + setloop split_tac [expand_if]))); +(*Fake*) +by (best_tac (!claset addSIs [disjI2] + addIs [impOfSubs (subset_insertI RS analz_mono)] + addDs [impOfSubs analz_subset_parts, + impOfSubs Fake_parts_insert] + addss (!simpset)) 2); +(*Base*) +by (fast_tac (!claset addss (!simpset)) 1); +qed_spec_mp "B_trusts_NS1"; + + + +(**** Authenticity properties obtained from NS2 ****) + +(*Uniqueness for NS2: nonce NB identifies agent A and nonce NA + [proof closely follows that for unique_NA] *) +goal thy + "!!evs. evs : ns_public \ +\ ==> Nonce NB ~: analz (sees lost Spy evs) --> \ +\ (EX A' NA'. ALL A NA. \ +\ Crypt (pubK A) {|Nonce NA, Nonce NB|} : parts (sees lost Spy evs) --> \ +\ A=A' & NA=NA')"; +by (etac ns_public.induct 1); +by (ALLGOALS + (asm_simp_tac + (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes) + setloop split_tac [expand_if]))); +(*NS2*) +by (expand_case_tac "NB = ?y" 3 THEN + REPEAT (fast_tac (!claset addSEs (nonce_not_seen_now::partsEs)) 3)); +(*Base*) +by (fast_tac (!claset addss (!simpset)) 1); +(*Fake*) +by (simp_tac (!simpset addsimps [all_conj_distrib,parts_insert_sees]) 1); +by (step_tac (!claset addSIs [impOfSubs (subset_insertI RS analz_mono)]) 1); +by (ex_strip_tac 1); +by (best_tac (!claset delrules [conjI] + addDs [impOfSubs analz_subset_parts, + impOfSubs Fake_parts_insert] + addss (!simpset)) 1); +val lemma = result(); + +goal thy + "!!evs. [| Crypt(pubK A) {|Nonce NA, Nonce NB|} : parts(sees lost Spy evs); \ +\ Crypt(pubK A'){|Nonce NA', Nonce NB|} : parts(sees lost Spy evs); \ +\ Nonce NB ~: analz (sees lost Spy evs); \ +\ evs : ns_public |] \ +\ ==> A=A' & NA=NA'"; +by (dtac lemma 1); +by (mp_tac 1); +by (REPEAT (etac exE 1)); +(*Duplicate the assumption*) +by (forw_inst_tac [("psi", "ALL C.?P(C)")] asm_rl 1); +by (fast_tac (!claset addSDs [spec]) 1); +qed "unique_NB"; + + +(*NB remains secret PROVIDED Alice never responds with round 3*) +goal thy + "!!evs. [| A ~: lost; B ~: lost; evs : ns_public |] \ +\ ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set_of_list evs --> \ +\ (ALL C. Says A C (Crypt (pubK C) (Nonce NB)) ~: set_of_list evs) --> \ +\ Nonce NB ~: analz (sees lost Spy evs)"; +by (etac ns_public.induct 1); +by (ALLGOALS + (asm_simp_tac + (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes) + setloop split_tac [expand_if]))); +(*NS1*) +by (fast_tac (!claset addSEs partsEs + addSDs [new_nonces_not_seen, + Says_imp_sees_Spy' RS parts.Inj]) 2); +(*Fake*) +by (REPEAT_FIRST (rtac conjI ORELSE' spy_analz_tac)); +(*NS2 and NS3*) +by (Step_tac 1); +(*NS2*) +by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] + addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 3); +by (fast_tac (!claset addSEs partsEs + addSDs [new_nonces_not_seen, + Says_imp_sees_Spy' RS parts.Inj]) 2); +by (Fast_tac 1); +(*NS3*) +by (Fast_tac 2); +by (fast_tac (!claset addSEs partsEs + addSDs [Says_imp_sees_Spy' RS parts.Inj, + new_nonces_not_seen, + impOfSubs analz_subset_parts]) 1); + +by (forw_inst_tac [("A'","A")] (Says_imp_sees_Spy' RS parts.Inj RS unique_NB) 1 + THEN REPEAT (eresolve_tac [asm_rl, Says_imp_sees_Spy' RS parts.Inj] 1)); +by (Fast_tac 1); +bind_thm ("Spy_not_see_NB", result() RSN (2, rev_mp) RS mp); + + + +(*Authentication for B: if he receives message 3 and has used NB + in message 2, then A has sent message 3.*) +goal thy + "!!evs. [| A ~: lost; B ~: lost; evs : ns_public |] \ +\ ==> Crypt (pubK B) (Nonce NB) : parts (sees lost Spy evs) \ +\ --> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set_of_list evs \ +\ --> (EX C. Says A C (Crypt (pubK C) (Nonce NB)) : set_of_list evs)"; +by (etac ns_public.induct 1); +by (ALLGOALS (asm_simp_tac (!simpset addsimps [ex_disj_distrib]))); +by (ALLGOALS Asm_simp_tac); +(*NS1*) +by (fast_tac (!claset addSEs partsEs + addSDs [new_nonces_not_seen, + Says_imp_sees_Spy' RS parts.Inj]) 2); +(*Fake*) +by (REPEAT_FIRST (resolve_tac [impI, conjI])); +by (fast_tac (!claset addss (!simpset)) 1); +br (ccontr RS disjI2) 1; +by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT (assume_tac 1)); +by (Fast_tac 1); +(*37 seconds??*) +by (best_tac (!claset addSDs [impOfSubs Fake_parts_insert] + addDs [impOfSubs analz_subset_parts] + addss (!simpset)) 1); +(*NS3*) +by (Step_tac 1); +by (forward_tac [Spy_not_see_NB] 1 THEN REPEAT1 (assume_tac 1)); +by (Fast_tac 1); +by (best_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] + addDs [unique_NB]) 1); +qed_spec_mp "NB_decrypt_imp_A_msg"; + + +(*Corollary: if B receives message NS3 and the nonce NB agrees + then A sent NB to somebody....*) +goal thy + "!!evs. [| Says A' B (Crypt (pubK B) (Nonce NB)): set_of_list evs; \ +\ Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) \ +\ : set_of_list evs; \ +\ A ~: lost; B ~: lost; evs : ns_public |] \ +\ ==> EX C. Says A C (Crypt (pubK C) (Nonce NB)) : set_of_list evs"; +by (fast_tac (!claset addSIs [NB_decrypt_imp_A_msg] + addEs partsEs + addDs [Says_imp_sees_Spy' RS parts.Inj]) 1); +qed "B_trusts_NS3"; + + +(*Can we strengthen the secrecy theorem? NO*) +goal thy + "!!evs. [| A ~: lost; B ~: lost; evs : ns_public |] \ +\ ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set_of_list evs \ +\ --> Nonce NB ~: analz (sees lost Spy evs)"; +by (etac ns_public.induct 1); +by (ALLGOALS + (asm_simp_tac + (!simpset addsimps ([analz_subset_parts RS contra_subsetD] @ pushes) + setloop split_tac [expand_if]))); +(*NS1*) +by (fast_tac (!claset addSEs partsEs + addSDs [new_nonces_not_seen, + Says_imp_sees_Spy' RS parts.Inj]) 2); +(*Fake*) +by (REPEAT_FIRST (rtac conjI ORELSE' spy_analz_tac)); +(*NS2 and NS3*) +by (Step_tac 1); +(*NS2*) +by (fast_tac (!claset addSEs partsEs + addSDs [new_nonces_not_seen, + Says_imp_sees_Spy' RS parts.Inj]) 2); +by (fast_tac (!claset addSDs [Says_imp_sees_Spy' RS parts.Inj] + addEs [no_nonce_NS1_NS2 RSN (2, rev_notE)]) 1); +(*NS3*) +by (forw_inst_tac [("A'","A")] (Says_imp_sees_Spy' RS parts.Inj RS unique_NB) 1 + THEN REPEAT (eresolve_tac [asm_rl, Says_imp_sees_Spy' RS parts.Inj] 1)); +by (Step_tac 1); + +(* +THIS IS THE ATTACK! +Level 9 +!!evs. [| A ~: lost; B ~: lost; evs : ns_public |] + ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) + : set_of_list evs --> + Nonce NB ~: analz (sees lost Spy evs) + 1. !!evs Aa Ba B' NAa NBa evsa. + [| A ~: lost; B ~: lost; evsa : ns_public; A ~= Ba; + Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set_of_list evsa; + Says A Ba (Crypt (pubK Ba) {|Nonce NA, Agent A|}) : set_of_list evsa; + Ba : lost; + Says B A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) : set_of_list evsa; + Nonce NB ~: analz (sees lost Spy evsa) |] + ==> False +*) + + + diff -r 672015b535d7 -r 6d3f7c7f70b0 src/HOL/Auth/NS_Public_Bad.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Auth/NS_Public_Bad.thy Thu Dec 05 18:07:27 1996 +0100 @@ -0,0 +1,56 @@ +(* Title: HOL/Auth/NS_Public_Bad + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1996 University of Cambridge + +Inductive relation "ns_public" for the Needham-Schroeder Public-Key protocol. +Flawed version, vulnerable to Lowe's attack. + +From page 260 of + Burrows, Abadi and Needham. A Logic of Authentication. + Proc. Royal Soc. 426 (1989) +*) + +NS_Public_Bad = Public + + +consts lost :: agent set (*No need for it to be a variable*) + ns_public :: event list set +inductive ns_public + intrs + (*Initial trace is empty*) + Nil "[]: ns_public" + + (*The spy MAY say anything he CAN say. We do not expect him to + invent new nonces here, but he can also use NS1. Common to + all similar protocols.*) + Fake "[| evs: ns_public; B ~= Spy; + X: synth (analz (sees lost Spy evs)) |] + ==> Says Spy B X # evs : ns_public" + + (*Alice initiates a protocol run, sending a nonce to Bob*) + NS1 "[| evs: ns_public; A ~= B |] + ==> Says A B (Crypt (pubK B) {|Nonce (newN evs), Agent A|}) # evs + : ns_public" + + (*Bob responds to Alice's message with a further nonce*) + NS2 "[| evs: ns_public; A ~= B; + Says A' B (Crypt (pubK B) {|Nonce NA, Agent A|}) + : set_of_list evs |] + ==> Says B A (Crypt (pubK A) {|Nonce NA, Nonce (newN evs)|}) # evs + : ns_public" + + (*Alice proves her existence by sending NB back to Bob.*) + NS3 "[| evs: ns_public; A ~= B; + Says B' A (Crypt (pubK A) {|Nonce NA, Nonce NB|}) + : set_of_list evs; + Says A B (Crypt (pubK B) {|Nonce NA, Agent A|}) + : set_of_list evs |] + ==> Says A B (Crypt (pubK B) (Nonce NB)) # evs : ns_public" + + (**Oops message??**) + +rules + (*Spy has access to his own key for spoof messages*) + Spy_in_lost "Spy: lost" + +end diff -r 672015b535d7 -r 6d3f7c7f70b0 src/HOL/Auth/Public.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Auth/Public.ML Thu Dec 05 18:07:27 1996 +0100 @@ -0,0 +1,186 @@ +(* Title: HOL/Auth/Public + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1996 University of Cambridge + +Theory of Public Keys (common to all symmetric-key protocols) + +Server keys; initial states of agents; new nonces and keys; function "sees" +*) + + +open Public; + +(*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 + this means that some terms displayed as (f o g) will be rewritten, and others + will not!*) +Addsimps [o_def]; + +(*** Basic properties of pubK ***) + +(*Injectiveness and freshness of new keys and nonces*) +AddIffs [inj_pubK RS inj_eq]; +AddSDs [newN_length]; + +(** Rewrites should not refer to initState(Friend i) + -- not in normal form! **) + +Addsimps [priK_neq_pubK, priK_neq_pubK RS not_sym]; + +goal thy "Nonce (newN evs) ~: parts (initState lost B)"; +by (agent.induct_tac "B" 1); +by (Auto_tac ()); +qed "newN_notin_initState"; + +AddIffs [newN_notin_initState]; + +goalw thy [keysFor_def] "keysFor (parts (initState lost C)) = {}"; +by (agent.induct_tac "C" 1); +by (auto_tac (!claset addIs [range_eqI], !simpset)); +qed "keysFor_parts_initState"; +Addsimps [keysFor_parts_initState]; + +goalw thy [keysFor_def] "keysFor (Key``E) = {}"; +by (Auto_tac ()); +qed "keysFor_image_Key"; +Addsimps [keysFor_image_Key]; + + +(*** Function "sees" ***) + +goal thy + "!!evs. lost' <= lost ==> sees lost' A evs <= sees lost A evs"; +by (list.induct_tac "evs" 1); +by (agent.induct_tac "A" 1); +by (event.induct_tac "a" 2); +by (Auto_tac ()); +qed "sees_mono"; + +(*Agents see their own private keys!*) +goal thy "A ~= Spy --> Key (priK A) : sees lost A evs"; +by (list.induct_tac "evs" 1); +by (agent.induct_tac "A" 1); +by (Auto_tac ()); +qed_spec_mp "sees_own_priK"; + +(*All public keys are visible*) +goal thy "Key (pubK A) : sees lost A evs"; +by (list.induct_tac "evs" 1); +by (agent.induct_tac "A" 1); +by (Auto_tac ()); +qed_spec_mp "sees_pubK"; + +(*Spy sees private keys of lost agents!*) +goal thy "!!A. A: lost ==> Key (priK A) : sees lost Spy evs"; +by (list.induct_tac "evs" 1); +by (Auto_tac()); +qed "Spy_sees_lost"; + +AddIffs [sees_pubK]; +AddSIs [sees_own_priK, Spy_sees_lost]; + +(*Added for Yahalom/lost_tac*) +goal thy "!!A. [| Crypt (pubK A) X : analz (sees lost Spy evs); A: lost |] \ +\ ==> X : analz (sees lost Spy evs)"; +by (fast_tac (!claset addSDs [analz.Decrypt] addss (!simpset)) 1); +qed "Crypt_Spy_analz_lost"; + +(** Specialized rewrite rules for (sees lost A (Says...#evs)) **) + +goal thy "sees lost B (Says A B X # evs) = insert X (sees lost B evs)"; +by (Simp_tac 1); +qed "sees_own"; + +goal thy "!!A. Server ~= B ==> \ +\ sees lost Server (Says A B X # evs) = sees lost Server evs"; +by (Asm_simp_tac 1); +qed "sees_Server"; + +goal thy "!!A. Friend i ~= B ==> \ +\ sees lost (Friend i) (Says A B X # evs) = sees lost (Friend i) evs"; +by (Asm_simp_tac 1); +qed "sees_Friend"; + +goal thy "sees lost Spy (Says A B X # evs) = insert X (sees lost Spy evs)"; +by (Simp_tac 1); +qed "sees_Spy"; + +goal thy "sees lost A (Says A' B X # evs) <= insert X (sees lost A evs)"; +by (simp_tac (!simpset setloop split_tac [expand_if]) 1); +by (Fast_tac 1); +qed "sees_Says_subset_insert"; + +goal thy "sees lost A evs <= sees lost A (Says A' B X # evs)"; +by (simp_tac (!simpset setloop split_tac [expand_if]) 1); +by (Fast_tac 1); +qed "sees_subset_sees_Says"; + +(*Pushing Unions into parts. One of the agents A is B, and thus sees Y. + Once used to prove new_keys_not_seen; now obsolete.*) +goal thy "(UN A. parts (sees lost A (Says B C Y # evs))) = \ +\ parts {Y} Un (UN A. parts (sees lost A evs))"; +by (Step_tac 1); +by (etac rev_mp 1); (*split_tac does not work on assumptions*) +by (ALLGOALS + (fast_tac (!claset addss (!simpset addsimps [parts_Un, sees_Cons] + setloop split_tac [expand_if])))); +qed "UN_parts_sees_Says"; + +goal thy "Says A B X : set_of_list evs --> X : sees lost Spy evs"; +by (list.induct_tac "evs" 1); +by (Auto_tac ()); +qed_spec_mp "Says_imp_sees_Spy"; + +goal thy + "!!evs. [| Says A B (Crypt (pubK C) X) : 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 + "!!evs. [| Says A B (Crypt (pubK C) X) : set_of_list evs; \ +\ X ~: analz (sees lost Spy evs) |] \ +\ ==> C ~: lost"; +by (fast_tac (!claset addSDs [Says_imp_sees_Spy RS analz.Inj] + addss (!simpset)) 1); +qed "Says_Crypt_not_lost"; + +Addsimps [sees_own, sees_Server, sees_Friend, sees_Spy]; +Delsimps [sees_Cons]; (**** NOTE REMOVAL -- laws above are cleaner ****) + + +(** Power of the Spy **) + +(*The Spy can see more than anybody else, except for their initial state*) +goal thy "sees lost A evs <= initState lost A Un sees lost Spy evs"; +by (list.induct_tac "evs" 1); +by (event.induct_tac "a" 2); +by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD] + addss (!simpset)))); +qed "sees_agent_subset_sees_Spy"; + +(*The Spy can see more than anybody else who's lost their key!*) +goal thy "A: lost --> A ~= Server --> sees lost A evs <= sees lost Spy evs"; +by (list.induct_tac "evs" 1); +by (event.induct_tac "a" 2); +by (agent.induct_tac "A" 1); +by (auto_tac (!claset addDs [sees_Says_subset_insert RS subsetD], (!simpset))); +qed_spec_mp "sees_lost_agent_subset_sees_Spy"; + + +(** Simplifying parts (insert X (sees lost A evs)) + = parts {X} Un parts (sees lost A evs) -- since general case loops*) + +val parts_insert_sees = + parts_insert |> read_instantiate_sg (sign_of thy) + [("H", "sees lost A evs")] + |> standard; diff -r 672015b535d7 -r 6d3f7c7f70b0 src/HOL/Auth/Public.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Auth/Public.thy Thu Dec 05 18:07:27 1996 +0100 @@ -0,0 +1,66 @@ +(* Title: HOL/Auth/Public + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1996 University of Cambridge + +Theory of Public Keys (common to all symmetric-key protocols) + +Server keys; initial states of agents; new nonces and keys; function "sees" +*) + +Public = Message + List + + +consts + pubK :: agent => key + +syntax + priK :: agent => key + +translations + "priK x" == "invKey(pubK x)" + +consts (*Initial states of agents -- parameter of the construction*) + initState :: [agent set, agent] => msg set + +primrec initState agent + (*Agents know their private key and all public keys*) + initState_Server "initState lost Server = + insert (Key (priK Server)) (Key `` range pubK)" + initState_Friend "initState lost (Friend i) = + insert (Key (priK (Friend i))) (Key `` range pubK)" + initState_Spy "initState lost Spy = + (Key``invKey``pubK``lost) Un (Key `` range pubK)" + + +datatype (*Messages, and components of agent stores*) + event = Says agent agent msg + +consts + sees1 :: [agent, event] => msg set + +primrec sees1 event + (*Spy reads all traffic whether addressed to him or not*) + sees1_Says "sees1 A (Says A' B X) = (if A:{B,Spy} then {X} else {})" + +consts + sees :: [agent set, agent, event list] => msg set + +primrec sees list + sees_Nil "sees lost A [] = initState lost A" + sees_Cons "sees lost A (ev#evs) = sees1 A ev Un sees lost A evs" + + +(*Agents generate "random" nonces. These are uniquely determined by + the length of their argument, a trace.*) +consts + newN :: "event list => nat" + +rules + + (*Public keys are disjoint, and never clash with private keys*) + inj_pubK "inj pubK" + priK_neq_pubK "priK A ~= pubK B" + + newN_length "(newN evs = newN evt) ==> (length evs = length evt)" + +end