# HG changeset patch # User paulson # Date 842613417 -7200 # Node ID c80e58e78d9c017f50c38e9f1584f8bf0ca2995c # Parent 4ddfafdeefa4b2f0adef3d7302232d479586023a Addition of Yahalom protocol diff -r 4ddfafdeefa4 -r c80e58e78d9c src/HOL/Auth/ROOT.ML --- a/src/HOL/Auth/ROOT.ML Fri Sep 13 13:15:48 1996 +0200 +++ b/src/HOL/Auth/ROOT.ML Fri Sep 13 13:16:57 1996 +0200 @@ -14,4 +14,5 @@ use_thy "Shared"; use_thy "NS_Shared"; use_thy "OtwayRees"; +use_thy "Yahalom"; diff -r 4ddfafdeefa4 -r c80e58e78d9c src/HOL/Auth/Yahalom.ML --- a/src/HOL/Auth/Yahalom.ML Fri Sep 13 13:15:48 1996 +0200 +++ b/src/HOL/Auth/Yahalom.ML Fri Sep 13 13:16:57 1996 +0200 @@ -1,4 +1,4 @@ -(* Title: HOL/Auth/OtwayRees +(* Title: HOL/Auth/Yahalom ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1996 University of Cambridge @@ -10,11 +10,25 @@ Proc. Royal Soc. 426 (1989) *) -open OtwayRees; +open Yahalom; proof_timing:=true; HOL_quantifiers := false; + +(** Weak liveness: there are traces that reach the end **) + +goal thy + "!!A B. [| A ~= B; A ~= Server; B ~= Server |] \ +\ ==> EX X NB K. EX evs: yahalom. \ +\ Says A B {|X, Crypt (Nonce NB) K|} : set_of_list evs"; +by (REPEAT (resolve_tac [exI,bexI] 1)); +br (yahalom.Nil RS yahalom.YM1 RS yahalom.YM2 RS yahalom.YM3 RS yahalom.YM4) 2; +by (ALLGOALS (simp_tac (!simpset setsolver safe_solver))); +by (ALLGOALS Fast_tac); +qed "weak_liveness"; + + (**** Inductive proofs about yahalom ****) (*The Enemy can see more than anybody else, except for their initial state*) @@ -45,30 +59,19 @@ (** 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 "YM2_analz_sees_Enemy"; - -goal thy "!!evs. (Says S B {|N, X, X'|}) : set_of_list evs ==> \ +(*Lets us treat YM4 using a similar argument as for the Fake case.*) +goal thy "!!evs. Says S A {|Crypt Y (shrK A), X|} : set_of_list evs ==> \ \ X : analz (sees Enemy evs)"; by (fast_tac (!claset addSDs [Says_imp_sees_Enemy RS analz.Inj]) 1); qed "YM4_analz_sees_Enemy"; -goal thy "!!evs. (Says B' A {|N, Crypt {|N,K|} K'|}) : set_of_list evs ==> \ +goal thy "!!evs. Says S A {|Crypt {|B, K, NA, NB|} (shrK A), X|} \ +\ : 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 "YM5_parts_sees_Enemy"; +qed "YM4_parts_sees_Enemy"; -(*YM2_analz... and YM4_analz... let us treat those cases using the same - argument as for the Fake case. This is possible for most, but not all, - proofs: Fake does not invent new nonces (as in YM2), and of course Fake - messages originate from the Enemy. *) - -val YM2_YM4_tac = - dtac (YM2_analz_sees_Enemy RS (impOfSubs analz_subset_parts)) 4 THEN - dtac (YM4_analz_sees_Enemy RS (impOfSubs analz_subset_parts)) 6; (*** Shared keys are not betrayed ***) @@ -78,11 +81,13 @@ "!!evs. [| evs : yahalom; A ~: bad |] ==> \ \ Key (shrK A) ~: parts (sees Enemy evs)"; be yahalom.induct 1; -by YM2_YM4_tac; +bd (YM4_analz_sees_Enemy RS synth.Inj) 6; +by (ALLGOALS Asm_simp_tac); +by (stac insert_commute 3); by (Auto_tac()); -(*Deals with Fake message*) -by (best_tac (!claset addDs [impOfSubs analz_subset_parts, - impOfSubs Fake_parts_insert]) 1); +(*Fake and YM4 are similar*) +by (ALLGOALS (best_tac (!claset addSDs [impOfSubs analz_subset_parts, + impOfSubs Fake_parts_insert]))); qed "Enemy_not_see_shrK"; bind_thm ("Enemy_not_analz_shrK", @@ -94,7 +99,7 @@ As usual fast_tac cannot be used because it uses the equalities too soon*) val major::prems = goal thy "[| Key (shrK A) : parts (sees Enemy evs); \ -\ evs : yahalom; \ +\ evs : yahalom; \ \ A:bad ==> R \ \ |] ==> R"; br ccontr 1; @@ -121,13 +126,11 @@ \ length evs <= length evs' --> \ \ Key (newK evs') ~: (UN C. parts (sees C evs))"; be yahalom.induct 1; -by YM2_YM4_tac; -(*auto_tac does not work here, as it performs safe_tac first*) -by (ALLGOALS Asm_simp_tac); +bd (YM4_analz_sees_Enemy RS synth.Inj) 6; by (REPEAT_FIRST (best_tac (!claset addDs [impOfSubs analz_subset_parts, - impOfSubs parts_insert_subset_Un, - Suc_leD] - addss (!simpset)))); + impOfSubs parts_insert_subset_Un, + Suc_leD] + addss (!simpset)))); val lemma = result(); (*Variant needed for the main theorem below*) @@ -156,27 +159,24 @@ \ length evs <= length evs' --> \ \ newK evs' ~: keysFor (UN C. parts (sees C evs))"; be yahalom.induct 1; -by YM2_YM4_tac; -bd YM5_parts_sees_Enemy 7; -by (ALLGOALS Asm_simp_tac); -(*YM1 and YM3*) -by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,2])); -(*Fake, YM2, YM4: these messages send unknown (X) components*) -by (EVERY - (map +by (forward_tac [YM4_parts_sees_Enemy] 6); +bd (YM4_analz_sees_Enemy RS synth.Inj) 6; +by (ALLGOALS Asm_full_simp_tac); +(*YM1, YM2 and YM3*) +by (EVERY (map (fast_tac (!claset addDs [Suc_leD] addss (!simpset))) [4,3,2])); +(*Fake and YM4: these messages send unknown (X) components*) +by (stac insert_commute 2); +by (Simp_tac 2); +(*YM4: the only way K could have been used is if it had been seen, + contradicting new_keys_not_seen*) +by (ALLGOALS (best_tac - (!claset addSDs [newK_invKey] - addDs [impOfSubs (analz_subset_parts RS keysFor_mono), + (!claset 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])); -(*YM5: 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); + addDs [impOfSubs analz_subset_parts] + addEs [new_keys_not_seen RSN(2,rev_notE)] + addss (!simpset)))); val lemma = result(); goal thy @@ -214,14 +214,16 @@ \ (Crypt X (newK evt)) : parts (sees Enemy evs) & \ \ Key K : parts {X} --> Key K : parts (sees Enemy evs)"; be yahalom.induct 1; -by YM2_YM4_tac; +bd (YM4_analz_sees_Enemy RS synth.Inj) 6; 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)) 2); -(*Base case and YM5*) +by (EVERY + (map (best_tac (!claset addSEs partsEs + addDs [impOfSubs analz_subset_parts, + impOfSubs parts_insert_subset_Un] + addss (!simpset))) + [3,2])); +(*Base case*) by (Auto_tac()); result(); @@ -259,19 +261,6 @@ (** 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 (Key``nE Un sEe)) --> \ @@ -286,34 +275,23 @@ \ ALL K E. (Key K : analz (Key``(newK``E) Un (sees Enemy evs))) = \ \ (K : newK``E | Key K : analz (sees Enemy evs))"; be yahalom.induct 1; -bd YM2_analz_sees_Enemy 4; bd YM4_analz_sees_Enemy 6; by (REPEAT_FIRST (resolve_tac [allI, lemma])); -by (ALLGOALS (*Takes 35 secs*) +by (ALLGOALS (asm_simp_tac (!simpset addsimps ([insert_Key_singleton, insert_Key_image, pushKey_newK] @ pushes) setloop split_tac [expand_if]))); (*YM4*) -by (enemy_analz_tac 5); +by (enemy_analz_tac 4); (*YM3*) -by (Fast_tac 4); -(*YM2*) (** LEVEL 7 **) -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 11 **) -by (res_inst_tac [("y1","X"), ("A1", "?G Un (?H::msg set)")] - (insert_commute RS ssubst) 2); +by (Fast_tac 3); +(*Fake case*) 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 : yahalom ==> \ \ Key K : analz (insert (Key (newK evt)) (sees Enemy evs)) = \ @@ -326,29 +304,28 @@ (*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. [| Says Server A \ +\ {|Crypt {|Agent B, K, NA, NB|} (shrK A), \ +\ Crypt {|Agent A, K|} (shrK B)|} : set_of_list evs; \ \ evs : yahalom |] \ -\ ==> (EX evt:yahalom. K = Key(newK evt) & \ -\ length evt < length evs) & \ -\ (EX i. NA = Nonce i)"; +\ ==> (EX evt:yahalom. K = Key(newK evt) & \ +\ length evt < length evs)"; be rev_mp 1; be yahalom.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 YM3*) +(*Crucial secrecy property: Enemy does not see the keys sent in msg YM3 + As with Otway-Rees, proof does not need uniqueness of session keys.*) goal thy "!!evs. [| Says Server A \ -\ {|NA, Crypt {|NA, K|} (shrK B), \ -\ Crypt {|NB, K|} (shrK A)|} : set_of_list evs; \ -\ A ~: bad; B ~: bad; evs : yahalom |] ==> \ +\ {|Crypt {|Agent B, K, NA, NB|} (shrK A), \ +\ Crypt {|Agent A, K|} (shrK B)|} : set_of_list evs; \ +\ A ~: bad; B ~: bad; evs : yahalom |] ==> \ \ K ~: analz (sees Enemy evs)"; be rev_mp 1; be yahalom.induct 1; -bd YM2_analz_sees_Enemy 4; bd YM4_analz_sees_Enemy 6; by (ALLGOALS Asm_simp_tac); (*Next 3 steps infer that K has the form "Key (newK evs'" ... *) @@ -360,87 +337,10 @@ (!simpset addsimps ([analz_subset_parts RS contra_subsetD, analz_insert_Key_newK] @ pushes) setloop split_tac [expand_if]))); +(*YM4*) +by (enemy_analz_tac 3); (*YM3*) -by (fast_tac (!claset addSEs [less_irrefl]) 3); +by (fast_tac (!claset addSEs [less_irrefl]) 2); (*Fake*) (** LEVEL 10 **) -by (res_inst_tac [("y1","X"), ("x1", "Key ?K")] (insert_commute RS ssubst) 1); -by (enemy_analz_tac 1); -(*YM4*) -by (mp_tac 2); -by (enemy_analz_tac 2); -(*YM2*) -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"; - - - -(*** Session keys are issued at most once, and identify the principals ***) - -(** First, two lemmas for the Fake, YM2 and YM4 cases **) - -goal thy - "!!evs. [| X : synth (analz (sees Enemy evs)); \ -\ Crypt X' (shrK C) : parts{X}; \ -\ C ~: bad; evs : yahalom |] \ -\ ==> 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 : yahalom |] \ -\ ==> 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 : yahalom ==> \ -\ EX A B. ALL C. \ -\ C ~: bad --> \ -\ (ALL S S' X. Says S S' X : set_of_list evs --> \ -\ (EX NA. Crypt {|NA, Key K|} (shrK C) : parts{X}) --> C=A | C=B)"; -by (Simp_tac 1); -be yahalom.induct 1; -bd YM2_analz_sees_Enemy 4; -bd YM4_analz_sees_Enemy 6; -by (ALLGOALS - (asm_simp_tac (!simpset addsimps [all_conj_distrib, imp_conj_distrib]))); -by (REPEAT_FIRST (etac exE)); -(*YM4*) -by (ex_strip_tac 4); -by (fast_tac (!claset addSDs [synth.Inj RS Crypt_Fake_parts, - Crypt_parts_singleton]) 4); -(*YM3: 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); -(*YM2*) (** 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"; - -(*It seems strange but this theorem is NOT needed to prove the main result!*) diff -r 4ddfafdeefa4 -r c80e58e78d9c src/HOL/Auth/Yahalom.thy --- a/src/HOL/Auth/Yahalom.thy Fri Sep 13 13:15:48 1996 +0200 +++ b/src/HOL/Auth/Yahalom.thy Fri Sep 13 13:16:57 1996 +0200 @@ -1,4 +1,4 @@ -(* Title: HOL/Auth/OtwayRees +(* Title: HOL/Auth/Yahalom ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1996 University of Cambridge @@ -10,7 +10,7 @@ Proc. Royal Soc. 426 (1989) *) -OtwayRees = Shared + +Yahalom = Shared + consts yahalom :: "event list set" inductive yahalom @@ -26,13 +26,12 @@ (*Alice initiates a protocol run*) YM1 "[| evs: yahalom; A ~= B |] - ==> Says A B {|Nonce (newN evs), Agent A |} # evs : yahalom" + ==> Says A B {|Agent A, Nonce (newN evs)|} # evs : yahalom" (*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.*) + the sender is, hence the A' in the sender field.*) YM2 "[| evs: yahalom; B ~= Server; - Says A' B {|Nonce NA, Agent A|} : set_of_list evs |] + Says A' B {|Agent A, Nonce NA|} : set_of_list evs |] ==> Says B Server {|Agent B, Crypt {|Agent A, Nonce NA, Nonce (newN evs)|} (shrK B)|} @@ -40,34 +39,23 @@ (*The Server receives Bob's message. He responds by sending a new session key to Alice, with a packet for forwarding to Bob.*) - YM3 "[| evs: yahalom; B ~= Server; + YM3 "[| evs: yahalom; A ~= 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)|} + {|Agent B, Crypt {|Agent A, Nonce NA, Nonce NB|} (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)|} + ==> Says Server A + {|Crypt {|Agent B, Key (newK evs), + Nonce NA, Nonce NB|} (shrK A), + Crypt {|Agent A, Key (newK evs)|} (shrK B)|} # evs : yahalom" - (*Bob receives the Server's (?) message and compares the Nonces with - those in the message he previously sent the Server.*) + (*Alice receives the Server's (?) message, checks her Nonce, and + uses the new session key to send Bob his Nonce.*) YM4 "[| evs: yahalom; A ~= B; - Says S B {|Nonce NA, X, Crypt {|Nonce NB, Key K|} (shrK B)|} + Says S A {|Crypt {|Agent B, Key K, Nonce NA, Nonce NB|} (shrK A), + X|} : 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 : yahalom" - - (*Alice checks her Nonce, then sends a dummy message to Bob, - using the new session key.*) - YM5 "[| evs: yahalom; - 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 : yahalom" + Says A B {|Agent A, Nonce NA|} : set_of_list evs |] + ==> Says A B {|X, Crypt (Nonce NB) K|} # evs : yahalom" end