--- /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";
+
--- /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
--- /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
+*)
+
+
+
--- /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
--- /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;
--- /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