# HG changeset patch # User paulson # Date 841761811 -7200 # Node ID f97a6e5b6375c80ab8b26f0758466600d2298200 # Parent 9bd1c8826f5c6d487c230833cea0df635fd4077c Initial working proof of Otway-Rees protocol diff -r 9bd1c8826f5c -r f97a6e5b6375 src/HOL/Auth/OtwayRees.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Auth/OtwayRees.ML Tue Sep 03 16:43:31 1996 +0200 @@ -0,0 +1,481 @@ +(* Title: HOL/Auth/OtwayRees + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1996 University of Cambridge + +Inductive relation "otway" for the Otway-Rees protocol. + +From page 244 of + Burrows, Abadi and Needham. A Logic of Authentication. + Proc. Royal Soc. 426 (1989) +*) + +open OtwayRees; + +proof_timing:=true; +HOL_quantifiers := false; + +(**** Inductive proofs about otway ****) + +(*The Enemy can see more than anybody else, except for their initial state*) +goal thy + "!!evs. evs : otway ==> \ +\ sees A evs <= initState A Un sees Enemy evs"; +be otway.induct 1; +by (ALLGOALS (fast_tac (!claset addDs [sees_Says_subset_insert RS subsetD] + addss (!simpset)))); +qed "sees_agent_subset_sees_Enemy"; + + +(*Nobody sends themselves messages*) +goal thy "!!evs. evs : otway ==> ALL A X. Says A A X ~: set_of_list evs"; +be otway.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)]; + +goal thy "!!evs. evs : otway ==> Notes A X ~: set_of_list evs"; +be otway.induct 1; +by (Auto_tac()); +qed "not_Notes"; +Addsimps [not_Notes]; +AddSEs [not_Notes RSN (2, rev_notE)]; + + +(** For reasoning about the encrypted portion of messages **) + +goal thy "!!evs. (Says A' B {|N, Agent A, Agent B, X|}) : set_of_list evs ==> \ +\ X : analz (sees Enemy evs)"; +by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]) 1); +qed "OR2_analz_sees_Enemy"; + +goal thy "!!evs. (Says S B {|N, X, X'|}) : set_of_list evs ==> \ +\ X : analz (sees Enemy evs)"; +by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]) 1); +qed "OR4_analz_sees_Enemy"; + +goal thy "!!evs. (Says B' A {|N, Crypt {|N,K|} K'|}) : set_of_list evs ==> \ +\ K : parts (sees Enemy evs)"; +by (fast_tac (!claset addSEs partsEs + addSDs [Says_imp_sees_Enemy RS parts.Inj]) 1); +qed "OR5_parts_sees_Enemy"; + +(*OR2_analz... and OR4_analz... let us treat those cases using the same + argument as for the Fake case.*) +val OR2_OR4_tac = + dtac (OR2_analz_sees_Enemy RS (impOfSubs analz_subset_parts)) 4 THEN + dtac (OR4_analz_sees_Enemy RS (impOfSubs analz_subset_parts)) 6; + + +(*** Shared keys are not betrayed ***) + +(*Enemy never sees another agent's shared key!*) +goal thy + "!!evs. [| evs : otway; A ~= Enemy |] ==> \ +\ Key (shrK A) ~: parts (sees Enemy evs)"; +be otway.induct 1; +by OR2_OR4_tac; +by (Auto_tac()); +(*Deals with Fake message*) +by (best_tac (!claset addDs [impOfSubs analz_subset_parts, + impOfSubs Fake_parts_insert]) 1); +qed "Enemy_not_see_shrK"; + +bind_thm ("Enemy_not_analz_shrK", + [analz_subset_parts, Enemy_not_see_shrK] MRS contra_subsetD); + +Addsimps [Enemy_not_see_shrK, + not_sym RSN (2, Enemy_not_see_shrK), + Enemy_not_analz_shrK, + not_sym RSN (2, Enemy_not_analz_shrK)]; + +(*We go to some trouble to preserve R in the 3rd subgoal*) +val major::prems = +goal thy "[| Key (shrK A) : parts (sees Enemy evs); \ +\ evs : otway; \ +\ A=Enemy ==> R \ +\ |] ==> R"; +br ccontr 1; +br ([major, Enemy_not_see_shrK] MRS rev_notE) 1; +by (swap_res_tac prems 2); +by (ALLGOALS (fast_tac (!claset addIs prems))); +qed "Enemy_see_shrK_E"; + +bind_thm ("Enemy_analz_shrK_E", + analz_subset_parts RS subsetD RS Enemy_see_shrK_E); + +(*Classical reasoner doesn't need the not_sym versions (with swapped ~=) *) +AddSEs [Enemy_see_shrK_E, Enemy_analz_shrK_E]; + + +(*No Friend will ever see another agent's shared key + (excluding the Enemy, who might transmit his). + The Server, of course, knows all shared keys.*) +goal thy + "!!evs. [| evs : otway; A ~= Enemy; A ~= Friend j |] ==> \ +\ Key (shrK 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_shrK"; + + +(*Not for Addsimps -- it can cause goals to blow up!*) +goal thy + "!!evs. evs : otway ==> \ +\ (Key (shrK A) : analz (insert (Key (shrK B)) (sees Enemy evs))) = \ +\ (A=B | A=Enemy)"; +by (best_tac (!claset addDs [impOfSubs analz_subset_parts] + addIs [impOfSubs (subset_insertI RS analz_mono)] + addss (!simpset)) 1); +qed "shrK_mem_analz"; + + +(*** Future keys can't be seen or used! ***) + +(*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 : otway ==> \ +\ length evs <= length evs' --> \ +\ Key (newK evs') ~: (UN C. parts (sees C evs))"; +be otway.induct 1; +by OR2_OR4_tac; +(*auto_tac does not work here, as it performs safe_tac first*) +by (ALLGOALS Asm_simp_tac); +by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts, + impOfSubs parts_insert_subset_Un, + Suc_leD] + addss (!simpset)))); +val lemma = result(); + +(*Variant needed for the main theorem below*) +goal thy + "!!evs. [| evs : otway; length evs <= length evs' |] ==> \ +\ Key (newK evs') ~: parts (sees C evs)"; +by (fast_tac (!claset addDs [lemma]) 1); +qed "new_keys_not_seen"; +Addsimps [new_keys_not_seen]; + +(*Another variant: old messages must contain old keys!*) +goal thy + "!!evs. [| Says A B X : set_of_list evs; \ +\ Key (newK evt) : parts {X}; \ +\ evs : otway \ +\ |] ==> length evt < length evs"; +br ccontr 1; +by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Enemy] + addIs [impOfSubs parts_mono, leI]) 1); +qed "Says_imp_old_keys"; + + +(*Nobody can have USED keys that will be generated in the future. + ...very like new_keys_not_seen*) +goal thy "!!evs. evs : otway ==> \ +\ length evs <= length evs' --> \ +\ newK evs' ~: keysFor (UN C. parts (sees C evs))"; +be otway.induct 1; +by OR2_OR4_tac; +bd OR5_parts_sees_Enemy 7; +by (ALLGOALS Asm_simp_tac); +(*OR1 and OR3*) +by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,2])); +(*Fake, OR2, OR4: these messages send unknown (X) components*) +by (EVERY + (map + (best_tac + (!claset addSDs [newK_invKey] + addDs [impOfSubs (analz_subset_parts RS keysFor_mono), + impOfSubs (parts_insert_subset_Un RS keysFor_mono), + Suc_leD] + addEs [new_keys_not_seen RS not_parts_not_analz RSN(2,rev_notE)] + addss (!simpset))) + [3,2,1])); +(*OR5: dummy message*) +by (best_tac (!claset addSDs [newK_invKey] + addEs [new_keys_not_seen RSN(2,rev_notE)] + addIs [less_SucI, impOfSubs keysFor_mono] + addss (!simpset addsimps [le_def])) 1); +val lemma = result(); + +goal thy + "!!evs. [| evs : otway; length evs <= length evs' |] ==> \ +\ newK evs' ~: keysFor (parts (sees C evs))"; +by (fast_tac (!claset addSDs [lemma] addss (!simpset)) 1); +qed "new_keys_not_used"; + +bind_thm ("new_keys_not_analzd", + [analz_subset_parts RS keysFor_mono, + new_keys_not_used] MRS contra_subsetD); + +Addsimps [new_keys_not_used, new_keys_not_analzd]; + + +(** Lemmas concerning the form of items passed in messages **) + + +(**** + The following is to prove theorems of the form + + Key K : analz (insert (Key (newK evt)) + (insert (Key (shrK C)) (sees Enemy evs))) ==> + Key K : analz (insert (Key (shrK C)) (sees Enemy evs)) + + A more general formula must be proved inductively. + +****) + + +(*NOT useful in this form, but it says that session keys are not used + to encrypt messages containing other keys, in the actual protocol. + We require that agents should behave like this subsequently also.*) +goal thy + "!!evs. evs : otway ==> \ +\ (Crypt X (newK evt)) : parts (sees Enemy evs) & \ +\ Key K : parts {X} --> Key K : parts (sees Enemy evs)"; +be otway.induct 1; +by OR2_OR4_tac; +by (ALLGOALS (asm_simp_tac (!simpset addsimps pushes))); +(*Deals with Faked messages*) +by (best_tac (!claset addSEs partsEs + addDs [impOfSubs analz_subset_parts, + impOfSubs parts_insert_subset_Un] + addss (!simpset)) 1); +(*OR5*) +by (fast_tac (!claset addss (!simpset)) 1); +result(); + + +(** Specialized rewriting for this proof **) + +Delsimps [image_insert]; +Addsimps [image_insert RS sym]; + +goal thy "insert (Key (newK x)) (sees A evs) = \ +\ Key `` (newK``{x}) Un (sees A evs)"; +by (Fast_tac 1); +val insert_Key_singleton = result(); + +goal thy "insert (Key (f x)) (Key``(f``E) Un C) = \ +\ Key `` (f `` (insert x E)) Un C"; +by (Fast_tac 1); +val insert_Key_image = result(); + + +(*This lets us avoid analyzing the new message -- unless we have to!*) +(*NEEDED??*) +goal thy "synth (analz (sees Enemy evs)) <= \ +\ synth (analz (sees Enemy (Says A B X # evs)))"; +by (Simp_tac 1); +br (subset_insertI RS analz_mono RS synth_mono) 1; +qed "synth_analz_thin"; + +AddIs [impOfSubs synth_analz_thin]; + + + +(** Session keys are not used to encrypt other session keys **) + +(*Could generalize this so that the X component doesn't have to be first + in the message?*) +val enemy_analz_tac = + SELECT_GOAL + (EVERY [REPEAT (resolve_tac [impI,notI] 1), + dtac (impOfSubs Fake_analz_insert) 1, + eresolve_tac [asm_rl, synth.Inj] 1, + Fast_tac 1, + Asm_full_simp_tac 1, + IF_UNSOLVED (deepen_tac (!claset addIs [impOfSubs analz_mono]) 0 1) + ]); + + +(*Lemma for the trivial direction of the if-and-only-if*) +goal thy + "!!evs. (Key K : analz (insert KsC (Key``nE Un sEe))) --> \ +\ (K : nE | Key K : analz (insert KsC sEe)) ==> \ +\ (Key K : analz (insert KsC (Key``nE Un sEe))) = \ +\ (K : nE | Key K : analz (insert KsC sEe))"; +by (fast_tac (!claset addSEs [impOfSubs analz_mono]) 1); +val lemma = result(); + +goal thy + "!!evs. evs : otway ==> \ +\ ALL K E. (Key K : analz (insert (Key (shrK C)) \ +\ (Key``(newK``E) Un (sees Enemy evs)))) = \ +\ (K : newK``E | \ +\ Key K : analz (insert (Key (shrK C)) \ +\ (sees Enemy evs)))"; +be otway.induct 1; +bd OR2_analz_sees_Enemy 4; +bd OR4_analz_sees_Enemy 6; +by (REPEAT_FIRST (resolve_tac [allI, lemma])); +by (ALLGOALS (*Takes 40 secs*) + (asm_simp_tac + (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK] + @ pushes) + setloop split_tac [expand_if]))); +(*OR4*) +by (enemy_analz_tac 5); +(*OR3*) +by (Fast_tac 4); +(*OR2*) (** LEVEL 11 **) +by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")] + (insert_commute RS ssubst) 3); +by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")] + (insert_commute RS ssubst) 3); +by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 3); +by (enemy_analz_tac 3); +(*Fake case*) (** LEVEL 6 **) +by (res_inst_tac [("y1","X"), ("A1", "?G Un (?H::msg set)")] + (insert_commute RS ssubst) 2); +by (enemy_analz_tac 2); +(*Base case*) +by (fast_tac (!claset addIs [image_eqI] addss (!simpset)) 1); +qed_spec_mp "analz_image_newK"; + + +goal thy + "!!evs. evs : otway ==> \ +\ Key K : analz (insert (Key (newK evt)) \ +\ (insert (Key (shrK C)) \ +\ (sees Enemy evs))) = \ +\ (K = newK evt | \ +\ Key K : analz (insert (Key (shrK C)) \ +\ (sees Enemy evs)))"; +by (asm_simp_tac (HOL_ss addsimps [pushKey_newK, analz_image_newK, + insert_Key_singleton]) 1); +by (Fast_tac 1); +qed "analz_insert_Key_newK"; + + +(*** Session keys are issued at most once, and identify the principals ***) + +(*NOW WE HAVE... + Says S B + {|Nonce NA, Crypt {|Nonce NA, Key (newK evta)|} (shrK A), + Crypt {|Nonce NB, Key (newK evta)|} (shrK B)|} +AND + Says Server (Friend j) + {|Ni, Crypt {|Ni, Key (newK evta)|} (shrK (Friend i)), + Crypt {|Nj, Key (newK evta)|} (shrK (Friend j))|} +THUS + A = Friend i | A = Friend j +AND THIS LETS US PROVE IT!! +*) + +goal thy + "!!evs. [| X : synth (analz (sees Enemy evs)); \ +\ Crypt X' (shrK C) : parts{X}; \ +\ C ~= Enemy; evs : otway |] \ +\ ==> Crypt X' (shrK C) : parts (sees Enemy evs)"; +by (best_tac (!claset addSEs [impOfSubs analz_subset_parts] + addDs [impOfSubs parts_insert_subset_Un] + addss (!simpset)) 1); +qed "Crypt_Fake_parts"; + +goal thy + "!!evs. [| Crypt X' K : parts (sees A evs); evs : otway |] \ +\ ==> EX S S' Y. Says S S' Y : set_of_list evs & \ +\ Crypt X' K : parts {Y}"; +bd parts_singleton 1; +by (fast_tac (!claset addSDs [seesD] addss (!simpset)) 1); +qed "Crypt_parts_singleton"; + +fun ex_strip_tac i = REPEAT (ares_tac [exI, conjI] i) THEN assume_tac (i+1); + +(*The Key K uniquely identifies a pair of senders in the message encrypted by + C, but if C=Enemy then he could send all sorts of nonsense.*) +goal thy + "!!evs. evs : otway ==> \ +\ EX A B. ALL C S S' X NA. \ +\ C ~= Enemy --> \ +\ Says S S' X : set_of_list evs --> \ +\ (Crypt {|NA, Key K|} (shrK C) : parts{X} --> C=A | C=B)"; +be otway.induct 1; +bd OR2_analz_sees_Enemy 4; +bd OR4_analz_sees_Enemy 6; +by (ALLGOALS + (asm_simp_tac (!simpset addsimps [all_conj_distrib, imp_conj_distrib]))); +by (REPEAT_FIRST (etac exE)); +(*OR4*) +by (ex_strip_tac 4); +by (fast_tac (!claset addSDs [synth.Inj RS Crypt_Fake_parts, + Crypt_parts_singleton]) 4); +(*OR3: Case split propagates some context to other subgoal...*) + (** LEVEL 8 **) +by (excluded_middle_tac "K = newK evsa" 3); +by (Asm_simp_tac 3); +by (REPEAT (ares_tac [exI] 3)); +(*...we prove this case by contradiction: the key is too new!*) +by (fast_tac (!claset addIs [impOfSubs (subset_insertI RS parts_mono)] + addSEs partsEs + addEs [Says_imp_old_keys RS less_irrefl] + addss (!simpset)) 3); +(*OR2*) (** LEVEL 12 **) +by (ex_strip_tac 2); +by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")] + (insert_commute RS ssubst) 2); +by (Simp_tac 2); +by (fast_tac (!claset addSDs [synth.Inj RS Crypt_Fake_parts, + Crypt_parts_singleton]) 2); +(*Fake*) (** LEVEL 16 **) +by (ex_strip_tac 1); +by (fast_tac (!claset addSDs [Crypt_Fake_parts, Crypt_parts_singleton]) 1); +qed "unique_session_keys"; + + +(*Describes the form *and age* of K when the following message is sent*) +goal thy + "!!evs. [| Says Server B \ +\ {|NA, Crypt {|NA, K|} (shrK A), \ +\ Crypt {|NB, K|} (shrK B)|} : set_of_list evs; \ +\ evs : otway |] \ +\ ==> (EX evt:otway. K = Key(newK evt) & \ +\ length evt < length evs) & \ +\ (EX i. NA = Nonce i)"; +be rev_mp 1; +be otway.induct 1; +by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset)))); +qed "Says_Server_message_form"; + + +(*Crucial secrecy property: Enemy does not see the keys sent in msg OR3*) +goal thy + "!!evs. [| Says Server (Friend j) \ +\ {|Ni, Crypt {|Ni, K|} (shrK (Friend i)), \ +\ Crypt {|Nj, K|} (shrK (Friend j))|} : set_of_list evs; \ +\ evs : otway; Friend i ~= C; Friend j ~= C \ +\ |] ==> \ +\ K ~: analz (insert (Key (shrK C)) (sees Enemy evs))"; +be rev_mp 1; +be otway.induct 1; +bd OR2_analz_sees_Enemy 4; +bd OR4_analz_sees_Enemy 6; +by (ALLGOALS Asm_simp_tac); +(*Next 3 steps infer that K has the form "Key (newK evs'" ... *) +by (REPEAT_FIRST (resolve_tac [conjI, impI])); +by (TRYALL (forward_tac [Says_Server_message_form] THEN' assume_tac)); +by (REPEAT_FIRST (eresolve_tac [bexE, exE, conjE] ORELSE' hyp_subst_tac)); +by (ALLGOALS + (asm_full_simp_tac + (!simpset addsimps ([analz_subset_parts RS contra_subsetD, + analz_insert_Key_newK] @ pushes) + setloop split_tac [expand_if]))); +(*OR3*) +by (fast_tac (!claset addSEs [less_irrefl]) 3); +(*Fake*) (** LEVEL 8 **) +by (res_inst_tac [("y1","X"), ("x1", "Key ?K")] (insert_commute RS ssubst) 1); +by (enemy_analz_tac 1); +(*OR4*) +by (mp_tac 2); +by (enemy_analz_tac 2); +(*OR2*) +by (mp_tac 1); +by (res_inst_tac [("x1","X"), ("y1", "{|?XX,?YY|}")] + (insert_commute RS ssubst) 1); +by (asm_simp_tac (!simpset setloop split_tac [expand_if]) 1); +by (enemy_analz_tac 1); +qed "Enemy_not_see_encrypted_key"; diff -r 9bd1c8826f5c -r f97a6e5b6375 src/HOL/Auth/OtwayRees.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Auth/OtwayRees.thy Tue Sep 03 16:43:31 1996 +0200 @@ -0,0 +1,77 @@ +(* Title: HOL/Auth/OtwayRees + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1996 University of Cambridge + +Inductive relation "otway" for the Otway-Rees protocol. + +From page 244 of + Burrows, Abadi and Needham. A Logic of Authentication. + Proc. Royal Soc. 426 (1989) +*) + +OtwayRees = Shared + + +consts otway :: "event list set" +inductive otway + intrs + (*Initial trace is empty*) + Nil "[]: otway" + + (*The enemy 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: otway; B ~= Enemy; X: synth (analz (sees Enemy evs)) + |] ==> Says Enemy B X # evs : otway" + + (*Alice initiates a protocol run*) + OR1 "[| evs: otway; A ~= B + |] ==> Says A B {|Nonce (newN evs), Agent A, Agent B, + Crypt {|Nonce (newN evs), Agent A, Agent B|} + (shrK A) |} + # evs : otway" + + (*Bob's response to Alice's message. Bob doesn't know who + the sender is, hence the A' in the sender field. + We modify the published protocol by NOT encrypting NB.*) + OR2 "[| evs: otway; B ~= Server; + Says A' B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs + |] ==> Says B Server + {|Nonce NA, Agent A, Agent B, X, Nonce (newN evs), + Crypt {|Nonce NA, Agent A, Agent B|} (shrK B)|} + # evs : otway" + + (*The Server receives Bob's message and checks that the three NAs + match. Then he sends a new session key to Bob with a packet for + forwarding to Alice.*) + OR3 "[| evs: otway; B ~= Server; + Says B' Server + {|Nonce NA, Agent A, Agent B, + Crypt {|Nonce NA, Agent A, Agent B|} (shrK A), + Nonce NB, + Crypt {|Nonce NA, Agent A, Agent B|} (shrK B)|} + : set_of_list evs + |] ==> Says Server B + {|Nonce NA, + Crypt {|Nonce NA, Key (newK evs)|} (shrK A), + Crypt {|Nonce NB, Key (newK evs)|} (shrK B)|} + # evs : otway" + + (*Bob receives the Server's (?) message and compares the Nonces with + those in the message he previously sent the Server.*) + OR4 "[| evs: otway; A ~= B; + Says S B {|Nonce NA, X, Crypt {|Nonce NB, Key K|} (shrK B)|} + : set_of_list evs; + Says B Server {|Nonce NA, Agent A, Agent B, X', Nonce NB, X''|} + : set_of_list evs + |] ==> (Says B A {|Nonce NA, X|}) # evs : otway" + + (*Alice checks her Nonce, then sends a dummy message to Bob, + using the new session key.*) + OR5 "[| evs: otway; + Says B' A {|Nonce NA, Crypt {|Nonce NA, Key K|} (shrK A)|} + : set_of_list evs; + Says A B {|Nonce NA, Agent A, Agent B, X|} : set_of_list evs + |] ==> Says A B (Crypt (Agent A) K) # evs : otway" + +end