# HG changeset patch # User paulson # Date 837091822 -7200 # Node ID 289ce6cb5c84a2b1d3abf7a81f475a99ea0942fa # Parent 7b1e1c298e50d667d4577a44eecdec3e89cfcacd Added Msg 3; works up to Says_Server_imp_Key_newK diff -r 7b1e1c298e50 -r 289ce6cb5c84 src/HOL/Auth/Event.ML --- a/src/HOL/Auth/Event.ML Thu Jul 11 15:28:10 1996 +0200 +++ b/src/HOL/Auth/Event.ML Thu Jul 11 15:30:22 1996 +0200 @@ -5,31 +5,39 @@ Datatype of events; inductive relation "traces" for Needham-Schroeder (shared keys) + +Rewrites should not refer to initState (Friend i) -- not in normal form *) open Event; +(*Rewrite using {a} Un A = insert a A *) +Addsimps [insert_is_Un RS sym]; + + +(*** Basic properties of serverKey and newK ***) + (* invKey (serverKey A) = serverKey A *) bind_thm ("invKey_serverKey", rewrite_rule [isSymKey_def] isSym_serverKey); -(* invKey (newK(A,evs)) = newK(A,evs) *) +(* invKey (newK evs) = newK evs *) bind_thm ("invKey_newK", rewrite_rule [isSymKey_def] isSym_newK); Addsimps [invKey_serverKey, invKey_newK]; (*New keys and nonces are fresh*) val serverKey_inject = inj_serverKey RS injD; -val newN_inject = inj_newN RS injD RS Pair_inject -and newK_inject = inj_newK RS injD RS Pair_inject; +val newN_inject = inj_newN RS injD +and newK_inject = inj_newK RS injD; AddSEs [serverKey_inject, newN_inject, newK_inject, fresh_newK RS notE, fresh_newN RS notE]; Addsimps [inj_serverKey RS inj_eq, inj_newN RS inj_eq, inj_newK RS inj_eq]; Addsimps [fresh_newN, fresh_newK]; -goal thy "newK (A,evs) ~= serverKey B"; -by (subgoal_tac "newK (A,evs) = serverKey B --> \ -\ Key (newK(A,evs)) : parts (initState B)" 1); +goal thy "newK evs ~= serverKey B"; +by (subgoal_tac "newK evs = serverKey B --> \ +\ Key (newK evs) : parts (initState B)" 1); by (Fast_tac 1); by (agent.induct_tac "B" 1); by (auto_tac (!claset addIs [range_eqI], !simpset)); @@ -79,7 +87,6 @@ goal thy "sees A (Says A B X # evs) = insert X (sees A evs)"; by (Simp_tac 1); -by (Fast_tac 1); qed "sees_own"; goal thy "!!A. Server ~= A ==> \ @@ -94,13 +101,17 @@ goal thy "sees Enemy (Says A B X # evs) = insert X (sees Enemy evs)"; by (Simp_tac 1); -by (Fast_tac 1); qed "sees_Enemy"; goal thy "sees A (Says A' B X # evs) <= insert X (sees A evs)"; by (simp_tac (!simpset setloop split_tac [expand_if]) 1); by (Fast_tac 1); -qed "sees_subset"; +qed "sees_Says_subset_insert"; + +goal thy "sees A evs <= sees 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 A's equals B, and thus sees Y*) goal thy "(UN A. parts (sees A (Says B C Y # evs))) = \ @@ -114,7 +125,7 @@ Addsimps [UN_parts_sees_Says, sees_own, sees_Server, sees_Friend, sees_Enemy]; -Delsimps [sees_Cons]; +Delsimps [sees_Cons]; (**** NOTE REMOVAL -- laws above are cleaner ****) (**** Inductive proofs about traces ****) @@ -124,47 +135,50 @@ "!!evs. evs : traces ==> \ \ sees A evs <= initState A Un sees Enemy evs"; be traces.induct 1; -be subst 4; (*simply DISCARD evsa = Says A Server... as irrelevant!*) -by (ALLGOALS (fast_tac (!claset addDs [sees_subset RS subsetD] +be subst 4; (*NS2: discard evsa = Says A Server... as irrelevant!*) +be subst 5; (*NS3: discard evsa = Says S Aa... as irrelevant!*) +by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD] addss (!simpset)))); qed "sees_agent_subset_sees_Enemy"; +goal thy "!!evs. evs : traces ==> ALL A X. Says A A X ~: setOfList evs"; +be traces.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)]; + + (*** Server keys are not betrayed ***) -(*No Enemy will ever see a Friend's server key - -- even if another friend's key is compromised. - The UN is essential to handle the Fake rule in the induction.*) +(*Enemy never sees another agent's server key!*) goal thy - "!!evs. [| evs : traces; i~=j |] ==> \ -\ Key (serverKey (Friend i)) ~: \ -\ parts (initState (Friend j) Un sees Enemy evs)"; + "!!evs. [| evs : traces; A ~= Enemy |] ==> \ +\ Key (serverKey A) ~: parts (sees Enemy evs)"; be traces.induct 1; -be subst 4; (*DISCARD evsa = Says A Server...#evs'a as irrelevant!*) -by (Auto_tac()); +be subst 4; (*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*) +by (auto_tac(!claset, !simpset addsimps [parts_insert2])); (*Deals with Faked messages*) -by (best_tac (!claset addDs [imp_of_subset analyze_subset_parts, - imp_of_subset parts_insert_subset_Un] +by (best_tac (!claset addDs [impOfSubs analyze_subset_parts, + impOfSubs parts_insert_subset_Un] addss (!simpset)) 1); qed "Enemy_not_see_serverKey"; -(*No Friend will ever see another Friend's server key.*) -goal thy - "!!evs. [| evs : traces; i~=j |] ==> \ -\ Key (serverKey (Friend i)) ~: parts (sees (Friend j) evs)"; -br (sees_agent_subset_sees_Enemy RS parts_mono RS contra_subsetD) 1; -by (REPEAT (ares_tac [Enemy_not_see_serverKey] 1)); -qed "Friend_not_see_serverKey"; +bind_thm ("Enemy_not_analyze_serverKey", + [analyze_subset_parts, Enemy_not_see_serverKey] MRS contra_subsetD); + +Addsimps [Enemy_not_see_serverKey, Enemy_not_analyze_serverKey]; + -(*Variant needed for the theorem below*) +(*No Friend will ever see another agent's server key + (excluding the Enemy, who might transmit his).*) goal thy - "!!evs. evs : traces ==> \ -\ Key (serverKey (Friend i)) ~: analyze (sees Enemy evs)"; -bd Enemy_not_see_serverKey 1; -br n_not_Suc_n 1; -by (Full_simp_tac 1); -by (fast_tac (!claset addDs [imp_of_subset analyze_subset_parts]) 1); -qed "serverKeys_not_analyzed"; + "!!evs. [| evs : traces; A ~= Enemy; A ~= Friend j |] ==> \ +\ Key (serverKey A) ~: parts (sees (Friend j) evs)"; +br (sees_agent_subset_sees_Enemy RS parts_mono RS contra_subsetD) 1; +by (ALLGOALS Asm_simp_tac); +qed "Friend_not_see_serverKey"; (*** Future keys can't be seen or used! ***) @@ -177,9 +191,9 @@ induction! *) goal thy "!!evs. evs : traces ==> \ \ length evs <= length evs' --> \ -\ Key (newK (A,evs')) ~: (UN C. parts (sees C evs))"; +\ Key (newK evs') ~: (UN C. parts (sees C evs))"; be traces.induct 1; -be subst 4; (*DISCARD evsa = Says A Server...#evs'a as irrelevant!*) +be subst 4; (*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*) by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [de_Morgan_disj,Suc_le_eq]))); (*Initial state? New keys cannot clash*) @@ -188,9 +202,11 @@ by (fast_tac (!claset addDs [less_imp_le]) 2); (*Rule NS2 in protocol*) by (fast_tac (!claset addIs [less_imp_le] addss (!simpset)) 2); +(*Rule NS3 in protocol*) +by (fast_tac (!claset addIs [less_imp_le] addss (!simpset)) 2); (*Rule Fake: where an Enemy agent can say practically anything*) -by (best_tac (!claset addDs [imp_of_subset analyze_subset_parts, - imp_of_subset parts_insert_subset_Un, +by (best_tac (!claset addDs [impOfSubs analyze_subset_parts, + impOfSubs parts_insert_subset_Un, less_imp_le] addss (!simpset)) 1); val lemma = result(); @@ -198,22 +214,25 @@ (*Variant needed for the main theorem below*) goal thy "!!evs. [| evs : traces; length evs <= length evs' |] ==> \ -\ Key (newK (A,evs')) ~: parts (sees C evs)"; +\ Key (newK evs') ~: parts (sees C evs)"; by (fast_tac (!claset addDs [lemma]) 1); qed "new_keys_not_seen"; -goal thy "!!K. newK(A,evs) = invKey K ==> newK(A,evs) = K"; +goal thy "!!K. newK evs = invKey K ==> newK evs = K"; br (invKey_eq RS iffD1) 1; by (Simp_tac 1); val newK_invKey = result(); + +val keysFor_parts_mono = parts_mono RS keysFor_mono; + (*Nobody can have USED keys that will be generated in the future. ...very like new_keys_not_seen*) goal thy "!!evs. evs : traces ==> \ \ length evs <= length evs' --> \ -\ newK (A,evs') ~: keysFor (UN C. parts (sees C evs))"; +\ newK evs' ~: keysFor (UN C. parts (sees C evs))"; be traces.induct 1; -be subst 4; (*DISCARD evsa = Says A Server...#evs'a as irrelevant!*) +be subst 4; (*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*) by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [de_Morgan_disj,Suc_le_eq]))); (*Rule NS1 in protocol*) @@ -223,24 +242,52 @@ (*Rule Fake: where an Enemy agent can say practically anything*) by (best_tac (!claset addSDs [newK_invKey] - addDs [imp_of_subset (analyze_subset_parts RS keysFor_mono), - imp_of_subset (parts_insert_subset_Un RS keysFor_mono), + addDs [impOfSubs (analyze_subset_parts RS keysFor_mono), + impOfSubs (parts_insert_subset_Un RS keysFor_mono), less_imp_le] addEs [new_keys_not_seen RS not_parts_not_analyze RSN (2,rev_notE)] addss (!simpset)) 1); +(*Rule NS3: quite messy...*) +by (hyp_subst_tac 1); +by (full_simp_tac (!simpset addcongs [conj_cong]) 1); +br impI 1; +bd mp 1; +by (fast_tac (!claset addDs [less_imp_le]) 1); +by (best_tac (!claset addIs + [impOfSubs (sees_subset_sees_Says RS keysFor_parts_mono), + impOfSubs (sees_own RS equalityD2 RS keysFor_parts_mono), + impOfSubs (empty_subsetI RS insert_mono RS keysFor_parts_mono)] + addss (!simpset)) 1); val lemma = result(); goal thy "!!evs. [| evs : traces; length evs <= length evs' |] ==> \ -\ newK (A,evs') ~: keysFor (parts (sees C evs))"; +\ newK evs' ~: keysFor (parts (sees C evs))"; by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1); qed "new_keys_not_used"; +Addsimps [new_keys_not_used]; -bind_thm ("new_keys_not_used_analyze", +bind_thm ("new_keys_not_analyzed", [analyze_subset_parts RS keysFor_mono, new_keys_not_used] MRS contra_subsetD); +(*Maybe too specific to be of much use...*) +goal thy + "!!evs. [| Says Server A (Crypt {|Nonce NA, Agent B, Key K, X|} \ +\ (serverKey A)) \ +\ : setOfList evs; \ +\ evs : traces \ +\ |] ==> (EX evs'. X = (Crypt {|Key(newK evs'), Agent A|} (serverKey B)))"; +be rev_mp 1; +be traces.induct 1; +be subst 4; (*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*) +be subst 5; (*NS3: discard evsa = Says S Aa... as irrelevant!*) +by (ALLGOALS Asm_full_simp_tac); +by (Fast_tac 1); (*Proves the NS2 case*) +qed "Says_Server_imp_X_eq_Crypt"; + + (*Pushes Crypt events in so that others might be pulled out*) goal thy "insert (Crypt X K) (insert y evs) = \ \ insert y (insert (Crypt X K) evs)"; @@ -252,157 +299,336 @@ by (Fast_tac 1); qed "insert_Key_delay"; + (** Lemmas concerning the form of items passed in messages **) (*Describes the form *and age* of K when the following message is sent*) goal thy - "!!evs. [| Says Server A (Crypt {|Agent A, Agent B, K, N|} K') \ + "!!evs. [| Says Server A (Crypt {|N, Agent B, K, X|} K') \ \ : setOfList evs; \ \ evs : traces \ -\ |] ==> (EX evs'. K = Key (newK(Server,evs')) & \ -\ length evs' < length evs)"; +\ |] ==> (EX evs'. K = Key (newK evs') & length evs' < length evs)"; be rev_mp 1; be traces.induct 1; -be subst 4; (*DISCARD evsa = Says A Server...#evs'a as irrelevant!*) +be subst 4; (*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*) by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset)))); qed "Says_Server_imp_Key_newK"; -Addsimps [serverKeys_not_analyzed, - new_keys_not_seen RS not_parts_not_analyze, - new_keys_not_used_analyze]; +(* c ~: keysFor (parts H) ==> c ~: keysFor (analyze H) *) +bind_thm ("not_parts_not_keysFor_analyze", + analyze_subset_parts RS keysFor_mono RS contra_subsetD); + + +XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX; +ZZZZZZZZZZZZZZZZ; + + +(*Fake case below may need something like this...*) +goal thy + "!!evs. evs : traces ==> \ +\ ALL B X. Crypt X (serverKey B) : analyze (sees Enemy evs) --> \ +\ (EX A A'. Says A A' (Crypt X (serverKey B)) : setOfList evs"; goal thy - "!!evs. evs : traces ==> \ -\ Says Server (Friend i) \ -\ (Crypt {|Agent(Friend i), Agent B, K, N|} K') : setOfList evs \ -\ --> K ~: analyze (sees Enemy evs)"; + "!!evs. evs : traces ==> \ +\ ALL NA B K X. Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey B) : + analyze (sees Enemy evs) --> \ +\ (EX A A'. Says A A' (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey B)) : setOfList evs"; + + + +(*Describes the form of X when the following message is sent*) +goal thy + "!!evs. evs : traces ==> \ +\ ALL S A NA B K X. \ +\ Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) \ +\ : setOfList evs --> \ +\ (EX evs'. X = (Crypt {|Key(newK evs'), Agent A|} (serverKey B)))"; be traces.induct 1; -be subst 4; (*simply DISCARD evsa = Says A Server... as irrelevant!*) +be subst 4; (*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*) +by (Step_tac 1); +by (ALLGOALS Asm_full_simp_tac); +(*Remaining cases are Fake, NS2 and NS3*) +by (Fast_tac 2); (*Solves the NS2 case*) +(*The NS3 case needs the induction hypothesis twice! + One application is to the X component of the most recent message.*) +by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 2); +be conjE 2; +by (subgoal_tac "? evs'. X = Crypt {|Key (newK evs'), Agent (Friend i)|} (serverKey B)" 2); +by (eres_inst_tac [("V","?P|?Q")] thin_rl 3); (*speeds the following step*) +by (Fast_tac 3); +(*DELETE the first quantified formula: it's now useless*) +by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2); +by (fast_tac (!claset addss (!simpset)) 2); +(*Now for the Fake case*) +be disjE 1; +(*The subcase of Fake, where the message in question is NOT the most recent*) +by (Best_tac 2); +(*The subcase of Fake proved because server keys are kept secret*) +by (REPEAT_FIRST (etac conjE ORELSE' hyp_subst_tac)); +be Crypt_synthesize 1; +be Key_synthesize 2; +by (Asm_full_simp_tac 2); + + + + 1. !!evs B X evsa S A NA Ba K Xa. + [| evsa : traces; + ! S A NA B K X. + Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) : + setOfList evsa --> + (? evs'. X = Crypt {|Key (newK evs'), Agent A|} (serverKey B)); + B ~= Enemy; + Crypt {|Nonce NA, Agent Ba, Key K, Xa|} (serverKey B) : + analyze (sees Enemy evsa) |] ==> + ? evs'. Xa = Crypt {|Key (newK evs'), Agent B|} (serverKey Ba) + + +(*Split up the possibilities of that message being synthesized...*) +by (Step_tac 1); +by (Best_tac 6); + + + + +by (Safe_step_tac 1); +by (Safe_step_tac 2); by (ALLGOALS Asm_full_simp_tac); -(*We infer that K has the form "Key (newK(Server,evs')" ... *) +by (REPEAT_FIRST (etac disjE)); +by (REPEAT_FIRST (etac conjE ORELSE' hyp_subst_tac)); + + +by (hyp_subst_tac 5); + + + + + +by (REPEAT (dtac spec 3)); +fe conjE; +fe mp ; +by (REPEAT (resolve_tac [refl, conjI] 3)); +by (REPEAT_FIRST (etac conjE)); +by (REPEAT_FIRST (etac conjE ORELSE' hyp_subst_tac)); + + +by (subgoal_tac "? evs'. Xa = Crypt {|Key (newK evs'), Agent Aa|} (serverKey Ba)" 2); +by (Fast_tac 3); + + + +be subst 5; (*NS3: discard evsa = Says S Aa... as irrelevant!*) + + +auto(); +by (ALLGOALS + (asm_full_simp_tac (!simpset addsimps [de_Morgan_disj,de_Morgan_conj]))); +by (REPEAT_FIRST (etac conjE ORELSE' hyp_subst_tac)); + +by (REPEAT (Safe_step_tac 1)); + +qed "Says_Crypt_Nonce_imp_msg_Crypt"; + +goal thy + "!!evs. [| Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} (serverKey A)) \ +\ : setOfList evs; \ +\ evs : traces \ +\ |] ==> (EX evs'. X = (Crypt {|Key(newK evs'), Agent A|} (serverKey B)))"; + + +YYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYY; + + +WWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWW; + +(*If a message is sent, encrypted with a Friend's server key, then either + that Friend or the Server originally sent it.*) +goal thy + "!!evs. evs : traces ==> \ +\ ALL A B X i. Says A B (Crypt X (serverKey (Friend i))) \ +\ : setOfList evs --> \ +\ (EX B'. Says Server B' (Crypt X (serverKey (Friend i))) : setOfList evs | \ +\ Says (Friend i) B' (Crypt X (serverKey (Friend i))) : setOfList evs)"; +be traces.induct 1; +be subst 4; (*NS2: discard evsa = Says A Server...#evs'a as irrelevant!*) +by (Step_tac 1); +by (ALLGOALS Asm_full_simp_tac); +(*Remaining cases are Fake, NS2 and NS3*) +by (Fast_tac 2); (*Proves the NS2 case*) + +by (REPEAT (dtac spec 2)); +fe conjE; +bd mp 2; + +by (REPEAT (resolve_tac [refl, conjI] 2)); +by (ALLGOALS Asm_full_simp_tac); + + + + +by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 2); +be conjE 2; +by ((dtac spec THEN' dtac spec THEN' dtac spec THEN' dtac spec)2); + +(*The NS3 case needs the induction hypothesis twice! + One application is to the X component of the most recent message.*) +by (subgoal_tac "? evs'. X = Crypt {|Key (newK evs'), Agent A|} (serverKey B)" 2); +by (Fast_tac 3); +by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 2); +be conjE 2; +(*DELETE the first quantified formula: it's now useless*) +by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 2); +by (fast_tac (!claset addss (!simpset)) 2); +(*Now for the Fake case*) +be disjE 1; +(*The subcase of Fake, where the message in question is NOT the most recent*) +by (Best_tac 2); + +by (REPEAT_FIRST (etac conjE ORELSE' hyp_subst_tac)); +be Crypt_synthesize 1; +be Key_synthesize 2; + +(*Split up the possibilities of that message being synthesized...*) +by (Step_tac 1); +by (Best_tac 6); + + + + + + (*The NS3 case needs the induction hypothesis twice! + One application is to the X component of the most recent message.*) + +???????????????????????????????????????????????????????????????? +by (subgoal_tac "? evs'. X = Crypt {|Key (newK evs'), Agent A|} (serverKey B)" 1); +by (Fast_tac 2); + +by (full_simp_tac (!simpset addsimps [all_conj_distrib]) 1); + +be conjE 1; +(*DELETE the first quantified formula: it's now useless*) +by (eres_inst_tac [("V","ALL S.?P(S)")] thin_rl 1); +by (fast_tac (!claset addss (!simpset)) 1); + + +(*Now for the Fake case*) +be disjE 1; +(*The subcase of Fake, where the message in question is NOT the most recent*) +by (Best_tac 2); + +WWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWW; + + +Addsimps [new_keys_not_seen]; + +(*Crucial security property: Enemy does not see the keys sent in msg NS2 + -- even if another friend's key is compromised*) +goal thy + "!!evs. [| Says Server (Friend i) \ +\ (Crypt {|N, Agent B, K, X|} K') : setOfList evs; \ +\ evs : traces; i~=j |] ==> \ +\ \ +\ K ~: analyze (insert (Key (serverKey (Friend j))) (sees Enemy evs))"; +be rev_mp 1; +be traces.induct 1; +be subst 4; (*NS2: discard evsa = Says A Server... as irrelevant!*) +by (ALLGOALS Asm_full_simp_tac); +(*The two simplifications cannot be combined -- they loop!*) +by (ALLGOALS (full_simp_tac (!simpset addsimps [insert_Key_delay]))); +(*Next 3 steps infer that K has the form "Key (newK evs'" ... *) br conjI 3; by (REPEAT_FIRST (resolve_tac [impI])); by (TRYALL (forward_tac [Says_Server_imp_Key_newK] THEN' assume_tac)); (*NS1, subgoal concerns "(Says A Server - {|Agent A, Agent B, Nonce (newN (A, evsa))|}"*) + {|Agent A, Agent B, Nonce (newN evsa)|}"*) (*... thus it cannot equal any components of A's message above.*) by (fast_tac (!claset addss (!simpset)) 2); (*NS2, the subcase where that message was the most recently sent; - it holds because here K' = serverKey(Friend i), which Enemies can't see*) -by (fast_tac (!claset addss (!simpset)) 2); -(*NS2, other subcase!*) + it holds because here K' = serverKey(Friend i), which Enemies can't see, + AND because nobody can know about a brand new key*) +by (fast_tac (!claset addss (!simpset addsimps [not_parts_not_analyze])) 2); +(*NS2, other subcase. K is an old key, and thus not in the latest message.*) by (fast_tac (!claset addSEs [less_irrefl] - addDs [imp_of_subset analyze_insert_Crypt_subset] - addss (!simpset addsimps [new_keys_not_used_analyze])) 2); + addDs [impOfSubs analyze_insert_Crypt_subset] + addss (!simpset addsimps [not_parts_not_keysFor_analyze])) 2); (*Now for the Fake case*) be exE 1; br notI 1; by (REPEAT (etac conjE 1)); by (REPEAT (hyp_subst_tac 1)); -by (subgoal_tac "Key (newK (Server, evs')) : analyze (synthesize (analyze (sees Enemy evsa)))" 1); -be (imp_of_subset analyze_mono) 2; +by (subgoal_tac + "Key (newK evs') : \ +\ analyze (synthesize (analyze (insert (Key (serverKey (Friend j))) \ +\ (sees Enemy evsa))))" 1); +be (impOfSubs analyze_mono) 2; by (best_tac (!claset addIs [analyze_mono RS synthesize_mono RSN (2,rev_subsetD), - imp_of_subset synthesize_increasing, - imp_of_subset analyze_increasing]) 2); + impOfSubs synthesize_increasing, + impOfSubs analyze_increasing]) 2); (*Proves the Fake goal*) by (Auto_tac()); -qed "encrypted_key_not_seen"; +qed "Enemy_not_see_encrypted_key"; + + +goal thy + "!!evs. [| Says Server (Friend i) \ +\ (Crypt {|N, Agent B, K|} K') : setOfList evs; \ +\ evs : traces; i~=j \ +\ |] ==> K ~: analyze (sees (Friend j) evs)"; +br (sees_agent_subset_sees_Enemy RS analyze_mono RS contra_subsetD) 1; +by (ALLGOALS (asm_simp_tac (!simpset addsimps [Enemy_not_see_encrypted_key]))); +qed "Friend_not_see_encrypted_key"; + +goal thy + "!!evs. [| Says Server (Friend i) \ +\ (Crypt {|N, Agent B, K|} K') : setOfList evs; \ +\ A ~: {Friend i, Server}; \ +\ evs : traces \ +\ |] ==> K ~: analyze (sees A evs)"; +by (eres_inst_tac [("P", "A~:?X")] rev_mp 1); +by (agent.induct_tac "A" 1); +by (ALLGOALS Simp_tac); +by (asm_simp_tac (!simpset addsimps [eq_sym_conv, + Friend_not_see_encrypted_key]) 1); +br ([analyze_mono, Enemy_not_see_encrypted_key] MRS contra_subsetD) 1; +(* hyp_subst_tac would deletes the equality assumption... *) +by (ALLGOALS (rtac n_not_Suc_n ORELSE' Fast_tac)); +qed "Agent_not_see_encrypted_key"; + + +(*Neatly packaged, perhaps in a useless form*) +goalw thy [knownBy_def] + "!!evs. [| Says Server (Friend i) \ +\ (Crypt {|N, Agent B, K|} K') : setOfList evs; \ +\ evs : traces \ +\ |] ==> knownBy evs K <= {Friend i, Server}"; + +by (Step_tac 1); +br ccontr 1; +by (fast_tac (!claset addDs [Agent_not_see_encrypted_key]) 1); +qed "knownBy_encrypted_key"; + XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX; -(*Nobody can have SEEN keys that will be generated in the future. - This has to be proved anew for each protocol description, - but should go by similar reasoning every time. Hardest case is the - standard Fake rule. - The length comparison, and Union over C, are essential for the - induction! *) -goal thy "!!evs. evs : traces ==> \ -\ length evs <= length evs' --> \ -\ Key (newK (A,evs')) ~: (UN C. parts (sees C evs))"; -be traces.induct 1; -be subst 4; (*DISCARD evsa = Says A Server...#evs'a as irrelevant!*) -by (ALLGOALS (asm_full_simp_tac - (!simpset addsimps [de_Morgan_disj,Suc_le_eq]))); -(*Initial state? New keys cannot clash*) -by (Fast_tac 1); -(*Rule NS1 in protocol*) -by (fast_tac (!claset addDs [less_imp_le]) 2); -(*Rule NS2 in protocol*) -by (fast_tac (!claset addIs [less_imp_le] addss (!simpset)) 2); -(*Rule Fake: where an Enemy agent can say practically anything*) -by (best_tac (!claset addDs [imp_of_subset analyze_subset_parts, - imp_of_subset parts_insert_subset_Un, - less_imp_le] - addss (!simpset)) 1); -val lemma = result(); + goal thy - "!!evs. [| evs : traces; i~=j |] ==> \ -\ Says Server (Friend i) \ -\ (Crypt {|Agent(Friend i), Agent B, K, N|} K') : setOfList evs \ -\ --> K ~: analyze (initState (Friend j) Un sees Enemy evs)"; + "!!evs. evs : traces ==> \ +\ Says Server A \ +\ (Crypt {|Agent A, Agent B, K, N|} K') : setOfList evs \ +\ --> (EX evs'. N = Nonce (newN evs'))"; be traces.induct 1; -be subst 4; (*simply DISCARD evsa = Says A Server... as irrelevant!*) -by (ALLGOALS Asm_full_simp_tac); -(*We infer that K has the form "Key (newK(Server,evs')" ... *) -br conjI 3; -by (REPEAT_FIRST (resolve_tac [impI])); -by (TRYALL (forward_tac [Says_Server_imp_Key_newK] THEN' assume_tac)); -(*NS1, subgoal concerns "(Says A Server - {|Agent A, Agent B, Nonce (newN (A, evsa))|}"*) -(*... thus it cannot equal any components of A's message above.*) - -by (full_simp_tac (!simpset addsimps [insert_Key_delay, insert_is_Un RS sym]) 2); - -by (fast_tac (!claset addss (!simpset)) 2); -(*NS2, the subcase where that message was the most recently sent; - it holds because here K' = serverKey(Friend i), which Enemies can't see*) -by (full_simp_tac (!simpset addsimps [insert_Key_delay, insert_is_Un RS sym]) 2); -by (Safe_step_tac 2); - -by (stac analyze_insert_Crypt 2); - -by (fast_tac (!claset addss (!simpset)) 2); -(*NS2, other subcase!*) +by (ALLGOALS Asm_simp_tac); +by (Fast_tac 1); +val Says_Server_lemma = result(); -by (full_simp_tac (!simpset addsimps [insert_Key_delay, insert_is_Un RS sym]) 2); -by (fast_tac - (!claset addSEs [less_irrefl] - addDs [imp_of_subset analyze_insert_Crypt_subset] - addss (!simpset addsimps [new_keys_not_used_analyze])) 2); -(*Now for the Fake case*) -be exE 1; -br notI 1; -by (REPEAT (etac conjE 1)); -by (REPEAT (hyp_subst_tac 1)); -by (subgoal_tac "Key (newK (Server, evs')) : analyze (synthesize (analyze (sees Enemy evsa)))" 1); -be (imp_of_subset analyze_mono) 2; -by (best_tac (!claset addIs [analyze_mono RS synthesize_mono RSN - (2,rev_subsetD), - imp_of_subset synthesize_increasing, - imp_of_subset analyze_increasing]) 2); -(*Proves the Fake goal*) -by (Auto_tac()); -qed "encrypted_key_not_seen"; - - - - -(*Bet this requires the premise A = Friend i *) -goal thy "[| evs : traces; \ -\ (Says Server A (Crypt {|Agent A, Agent B, K, N|} K')) \ -\ : setOfList evs \ -\ |] ==> knownBy evs K <= {A,Server}"; - - -XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX; (*NEEDED??*) @@ -419,20 +645,11 @@ by (asm_simp_tac (!simpset addsimps [parts_Un]) 1); qed "in_parts_sees_Says"; -goal thy "!!evs. length evs < length evs' ==> newK (A,evs) ~= newK (A',evs')"; +goal thy "!!evs. length evs < length evs' ==> newK evs ~= newK (A',evs')"; by (fast_tac (!claset addSEs [less_irrefl]) 1); qed "length_less_newK_neq"; -(*Initially -goal thy "knownBy [] X = \ -\ {A. X = Key (invKey (serverKey A)) | (? i. X = Key (serverKey i))}"; -by (simp_tac (!simpset addsimps [knownBy_def, analyze_trivial, range_def]) 1); -qed "knownBy_Nil"; - -goal thy "!!X. knownBy (x#l) X = ?F(knownBy l X)"; -by (simp_tac (!simpset addsimps [knownBy_def, analyze_trivial, range_def]) 1); -********************) goal thy "insert (Crypt x) (insert {|X,Y|} evs) = \ \ insert {|X,Y|} (insert (Crypt x) evs)"; @@ -441,39 +658,6 @@ -WWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWWW; - -goal thy - "!!evs. evs : traces ==> \ -\ Says Server A \ -\ (Crypt {|Agent A, Agent B, K, N|} K') : setOfList evs \ -\ --> (EX evs'. K = Key (newK(Server,evs')))"; -be traces.induct 1; -by (ALLGOALS Asm_simp_tac); -by (Fast_tac 1); -val Says_Server_lemma = result(); - -goal thy - "!!evs. [| Says Server A (Crypt {|Agent A, Agent B, K, N|} K') \ -\ : setOfList evs; \ -\ evs : traces \ -\ |] ==> (EX evs'. K = Key (newK(Server,evs')))"; -bd Says_Server_lemma 1; -by (Fast_tac 1); -qed "Says_Server_imp_Key_newK"; - - -goal thy - "!!evs. evs : traces ==> \ -\ Says Server A \ -\ (Crypt {|Agent A, Agent B, K, N|} K') : setOfList evs \ -\ --> (EX evs'. N = Nonce (newN(A,evs')))"; -be traces.induct 1; -by (ALLGOALS Asm_simp_tac); -by (Fast_tac 1); -val Says_Server_lemma = result(); - - YYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYYY; goalw thy [keysFor_def] diff -r 7b1e1c298e50 -r 289ce6cb5c84 src/HOL/Auth/Event.thy --- a/src/HOL/Auth/Event.thy Thu Jul 11 15:28:10 1996 +0200 +++ b/src/HOL/Auth/Event.thy Thu Jul 11 15:30:22 1996 +0200 @@ -6,6 +6,8 @@ Datatype of events; inductive relation "traces" for Needham-Schroeder (shared keys) +INTERLEAVING? See defn of "traces" + WHAT ABOUT ASYMMETRIC KEYS? NOBODY'S PRIVATE KEY CAN EQUAL SOMEBODY ELSE'S PUBLIC KEY... *) @@ -14,16 +16,16 @@ consts publicKey :: agent => key - serverKey :: agent => key (*symmetric keys*) + serverKey :: agent => key (*symmetric keys*) rules isSym_serverKey "isSymKey (serverKey A)" -consts (*Initial states of agents -- parameter of the construction*) +consts (*Initial states of agents -- parameter of the construction*) initState :: agent => msg set primrec initState agent - (*Server knows all keys; other agents know only their own*) + (*Server knows all keys; other agents know only their own*) initState_Server "initState Server = range (Key o serverKey)" initState_Friend "initState (Friend i) = {Key (serverKey (Friend i))}" initState_Enemy "initState Enemy = {Key (serverKey Enemy)}" @@ -51,7 +53,7 @@ sees :: [agent, event list] => msg set primrec sees list - (*Initial knowledge includes all public keys and own private key*) + (*Initial knowledge includes all public keys and own private key*) sees_Nil "sees A [] = initState A" sees_Cons "sees A (ev#evs) = sees1 A ev Un sees A evs" @@ -61,25 +63,29 @@ "knownBy evs X == {A. X: analyze (sees A evs)}" -(*Agents generate "random" nonces. Different agents always generate - different nonces. Different traces also yield different nonces. Same - applies for keys.*) -(*newK NEEDS AN ARGUMENT TO ALLOW ASYMMETRIC KEYS. REMOVE AGENT ARGUMENT? +(*Agents generate "random" nonces. Different traces always yield + different nonces. Same applies for keys.*) +(*newK NEEDS AN ARGUMENT TO ALLOW ASYMMETRIC KEYS. NEED AXIOM SAYING THAT NEW KEYS CANNOT EQUAL THE INVERSE OF A PREVIOUS KEY*) consts - newN :: "agent * event list => nat" - newK :: "agent * event list => key" + newN :: "event list => nat" + newK :: "event list => key" rules inj_serverKey "inj serverKey" inj_newN "inj(newN)" - fresh_newN "Nonce (newN(A,evs)) ~: parts (initState B)" + fresh_newN "Nonce (newN evs) ~: parts (initState B)" inj_newK "inj(newK)" - fresh_newK "Key (newK(A,evs)) ~: parts (initState B)" - isSym_newK "isSymKey (newK(A,evs))" + fresh_newK "Key (newK evs) ~: parts (initState B)" + isSym_newK "isSymKey (newK evs)" + +(*NS1 AND NS2 DON'T ALLOW INTERLEAVING -- that is, they only respond to the + MOST RECENT message. Does this mean we can't model middleperson attacks? + We don't need the most recent restriction in order to handle interception + by the Enemy, as agents are not forced to respond anyway.*) consts traces :: "event list set" inductive traces @@ -88,17 +94,39 @@ (*The enemy MAY say anything he CAN say. We do not expect him to invent new nonces here, but he can also use NS1.*) - Fake "[| evs: traces; X: synthesize(analyze(sees Enemy evs)) + Fake "[| evs: traces; B ~= Enemy; + X: synthesize(analyze(sees Enemy evs)) |] ==> (Says Enemy B X) # evs : traces" NS1 "[| evs: traces; A ~= Server - |] ==> (Says A Server {|Agent A, Agent B, Nonce (newN(A,evs))|}) + |] ==> (Says A Server {|Agent A, Agent B, Nonce (newN evs)|}) # evs : traces" - NS2 "[| evs: traces; + (*We can't trust the sender field: change that A to A'? *) + NS2 "[| evs: traces; A ~= B; evs = (Says A Server {|Agent A, Agent B, Nonce NA|}) # evs' |] ==> (Says Server A - (Crypt {|Agent A, Agent B, - Key (newK(Server,evs)), Nonce NA|} - (serverKey A))) # evs : traces" + (Crypt {|Nonce NA, Agent B, Key (newK evs), + (Crypt {|Key (newK evs), Agent A|} (serverKey B))|} + (serverKey A))) # evs : traces" + + (*We can't assume S=Server. Agent A "remembers" her nonce. + May assume WLOG that she is NOT the Enemy, as the Fake rule. + covers this case. Can inductively show A ~= Server*) + NS3 "[| evs: traces; A ~= B; + evs = (Says S A (Crypt {|Nonce NA, Agent B, Key K, X|} + (serverKey A))) + # evs'; + A = Friend i; + (Says A Server {|Agent A, Agent B, Nonce NA|}) : setOfList evs' + |] ==> (Says A B X) # evs : traces" + +(*Initial version of NS2 had + + {|Agent A, Agent B, Key (newK evs), Nonce NA|} + + for the encrypted part; the version above is LESS transparent, hence + maybe HARDER to prove. Also it is precisely as in the BAN paper. +*) + end diff -r 7b1e1c298e50 -r 289ce6cb5c84 src/HOL/Auth/Message.ML --- a/src/HOL/Auth/Message.ML Thu Jul 11 15:28:10 1996 +0200 +++ b/src/HOL/Auth/Message.ML Thu Jul 11 15:30:22 1996 +0200 @@ -22,7 +22,7 @@ fun auto() = by (Auto_tac()); -fun imp_of_subset th = th RSN (2, rev_subsetD); +fun impOfSubs th = th RSN (2, rev_subsetD); (**************** INSTALL CENTRALLY SOMEWHERE? ****************) @@ -141,6 +141,13 @@ by (REPEAT (ares_tac [equalityI, parts_Un_subset1, parts_Un_subset2] 1)); qed "parts_Un"; +(*TWO inserts to avoid looping. This rewrite is better than nothing...*) +goal thy "parts (insert X (insert Y H)) = parts {X} Un parts {Y} Un parts H"; +by (stac (read_instantiate [("A","H")] insert_is_Un) 1); +by (stac (read_instantiate [("A","{Y} Un H")] insert_is_Un) 1); +by (simp_tac (HOL_ss addsimps [parts_Un, Un_assoc]) 1); +qed "parts_insert2"; + goal thy "(UN x:A. parts(H x)) <= parts(UN x:A. H x)"; by (REPEAT (ares_tac [UN_least, parts_mono, UN_upper] 1)); val parts_UN_subset1 = result(); @@ -163,7 +170,7 @@ Addsimps [parts_Un, parts_UN, parts_UN1]; goal thy "insert X (parts H) <= parts(insert X H)"; -by (fast_tac (!claset addEs [imp_of_subset parts_mono]) 1); +by (fast_tac (!claset addEs [impOfSubs parts_mono]) 1); qed "parts_insert_subset"; (*Especially for reasoning about the Fake rule in traces*) @@ -304,7 +311,7 @@ qed "analyze_Un"; goal thy "insert X (analyze H) <= analyze(insert X H)"; -by (fast_tac (!claset addEs [imp_of_subset analyze_mono]) 1); +by (fast_tac (!claset addEs [impOfSubs analyze_mono]) 1); qed "analyze_insert"; (** Rewrite rules for pulling out atomic messages **) @@ -400,7 +407,7 @@ \ insert {|Agent agt,Y|} (insert (Agent agt) (analyze (insert Y H)))"; by (rtac equalityI 1); by (best_tac (!claset addIs [analyze.Fst, - imp_of_subset analyze_insert_subset_MPair2]) 2); + impOfSubs analyze_insert_subset_MPair2]) 2); br subsetI 1; be analyze.induct 1; by (ALLGOALS (fast_tac (!claset addss (!simpset)))); @@ -410,7 +417,7 @@ \ insert {|Nonce N,Y|} (insert (Nonce N) (analyze (insert Y H)))"; by (rtac equalityI 1); by (best_tac (!claset addIs [analyze.Fst, - imp_of_subset analyze_insert_subset_MPair2]) 2); + impOfSubs analyze_insert_subset_MPair2]) 2); br subsetI 1; be analyze.induct 1; by (ALLGOALS (fast_tac (!claset addss (!simpset)))); @@ -423,7 +430,7 @@ \ insert {|Key K, Y|} (insert (Key K) (analyze (insert Y H)))"; by (rtac equalityI 1); by (best_tac (!claset addIs [analyze.Fst, - imp_of_subset analyze_insert_subset_MPair2]) 2); + impOfSubs analyze_insert_subset_MPair2]) 2); br subsetI 1; be analyze.induct 1; by (ALLGOALS (fast_tac (!claset addss (!simpset)))); @@ -471,12 +478,12 @@ (*Helps to prove Fake cases*) goal thy "!!X. X: analyze (UN i. analyze (H i)) ==> X: analyze (UN i. H i)"; be analyze.induct 1; -by (ALLGOALS (fast_tac (!claset addEs [imp_of_subset analyze_mono]))); +by (ALLGOALS (fast_tac (!claset addEs [impOfSubs analyze_mono]))); val lemma = result(); goal thy "analyze (UN i. analyze (H i)) = analyze (UN i. H i)"; by (fast_tac (!claset addIs [lemma] - addEs [imp_of_subset analyze_mono]) 1); + addEs [impOfSubs analyze_mono]) 1); qed "analyze_UN_analyze"; Addsimps [analyze_UN_analyze]; @@ -595,8 +602,8 @@ br subsetI 1; be analyze.induct 1; by (best_tac - (!claset addEs [imp_of_subset synthesize_increasing, - imp_of_subset analyze_mono]) 5); + (!claset addEs [impOfSubs synthesize_increasing, + impOfSubs analyze_mono]) 5); by (Best_tac 1); by (deepen_tac (!claset addIs [analyze.Fst]) 0 1); by (deepen_tac (!claset addIs [analyze.Snd]) 0 1);