# HG changeset patch # User paulson # Date 843495643 -7200 # Node ID 4b7a432fb3ed24cfeea5dbb41f5049cbfe160168 # Parent 1b234f1fd9c74fd42ec3c0c3118b541813406ba2 Proof of Says_imp_old_keys is now more robust diff -r 1b234f1fd9c7 -r 4b7a432fb3ed src/HOL/Auth/Yahalom.ML --- a/src/HOL/Auth/Yahalom.ML Mon Sep 23 18:19:38 1996 +0200 +++ b/src/HOL/Auth/Yahalom.ML Mon Sep 23 18:20:43 1996 +0200 @@ -16,7 +16,7 @@ HOL_quantifiers := false; -(** Weak liveness: there are traces that reach the end **) +(*Weak liveness: there are traces that reach the end*) goal thy "!!A B. [| A ~= B; A ~= Server; B ~= Server |] \ @@ -26,7 +26,7 @@ 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"; +result(); (**** Inductive proofs about yahalom ****) @@ -49,13 +49,6 @@ Addsimps [not_Says_to_self]; AddSEs [not_Says_to_self RSN (2, rev_notE)]; -goal thy "!!evs. evs : yahalom ==> Notes A X ~: set_of_list evs"; -be yahalom.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 **) @@ -74,7 +67,8 @@ -(*** Shared keys are not betrayed ***) +(** Theorems of the form X ~: parts (sees Enemy evs) imply that NOBODY + sends messages containing X! **) (*Enemy never sees another agent's shared key! (unless it is leaked at start)*) goal thy @@ -148,8 +142,9 @@ \ evs : yahalom \ \ |] ==> length evt < length evs"; br ccontr 1; +bd leI 1; by (fast_tac (!claset addSDs [new_keys_not_seen, Says_imp_sees_Enemy] - addIs [impOfSubs parts_mono, leI]) 1); + addIs [impOfSubs parts_mono]) 1); qed "Says_imp_old_keys"; @@ -302,71 +297,83 @@ qed "analz_insert_Key_newK"; -(*Describes the form *and age* of K when the following message is sent*) +(*Describes the form of K when the Server sends this message.*) goal thy "!!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 evt:yahalom. K = Key(newK evt))"; be rev_mp 1; be yahalom.induct 1; -by (ALLGOALS (fast_tac (!claset addIs [less_SucI] addss (!simpset)))); +by (ALLGOALS (fast_tac (!claset addss (!simpset)))); qed "Says_Server_message_form"; -(*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.*) +(** 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. [| A ~: bad; B ~: bad; evs : yahalom; evt : yahalom |] \ +\ ==> Says Server A \ +\ {|Crypt {|Agent B, Key(newK evt), NA, NB|} (shrK A), \ +\ Crypt {|Agent A, Key(newK evt)|} (shrK B)|} \ +\ : set_of_list evs --> \ +\ Key(newK evt) ~: analz (sees Enemy evs)"; +be yahalom.induct 1; +bd YM4_analz_sees_Enemy 6; +by (ALLGOALS + (asm_simp_tac + (!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 addIs [parts_insertI] + addEs [Says_imp_old_keys RS less_irrefl] + addss (!simpset)) 2); +(*Fake*) (** LEVEL 10 **) +by (enemy_analz_tac 1); +val lemma = result() RS mp RSN(2,rev_notE); + + +(*Final version: Server's message in the most abstract form*) goal thy "!!evs. [| Says Server A \ \ {|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 YM4_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]))); -(*YM4*) -by (enemy_analz_tac 3); -(*YM3*) -by (fast_tac (!claset addSEs [less_irrefl]) 2); -(*Fake*) (** LEVEL 10 **) -by (enemy_analz_tac 1); +by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1); +by (fast_tac (!claset addSEs [lemma]) 1); qed "Enemy_not_see_encrypted_key"; +(** Towards proofs of stronger authenticity properties **) + goal thy - "!!evs. [| Crypt {|Agent A, Key K|} (shrK B) : analz (sees Enemy evs); \ + "!!evs. [| Crypt {|Agent A, Key K|} (shrK B) : parts (sees Enemy evs); \ \ B ~: bad; evs : yahalom |] \ \ ==> EX NA NB. Says Server A \ -\ {|Crypt {|Agent B, Key K, \ -\ Nonce NA, Nonce NB|} (shrK A), \ -\ Crypt {|Agent A, Key K|} (shrK B)|} \ -\ : set_of_list evs"; +\ {|Crypt {|Agent B, Key K, \ +\ Nonce NA, Nonce NB|} (shrK A), \ +\ Crypt {|Agent A, Key K|} (shrK B)|} \ +\ : set_of_list evs"; be rev_mp 1; be yahalom.induct 1; -by (forward_tac [YM4_analz_sees_Enemy] 6); -by (ALLGOALS (asm_simp_tac (!simpset setloop split_tac [expand_if]))); -(*YM4*) -by (enemy_analz_tac 4); +bd (YM4_analz_sees_Enemy RS synth.Inj) 6; +by (ALLGOALS Asm_simp_tac); (*YM3*) by (Fast_tac 3); -(*Fake*) -by (enemy_analz_tac 2); (*Base case*) by (fast_tac (!claset addss (!simpset)) 1); -qed "Enemy_analz_Server_msg"; +(*Prepare YM4*) +by (stac insert_commute 2 THEN Simp_tac 2); +(*Fake and YM4 are similar*) +by (ALLGOALS (best_tac (!claset addSDs [impOfSubs analz_subset_parts, + impOfSubs Fake_parts_insert]))); +qed "Crypt_imp_Server_msg"; (*What can B deduce from receipt of YM4? @@ -383,14 +390,10 @@ \ : set_of_list evs"; be rev_mp 1; be yahalom.induct 1; -by (forward_tac [YM4_analz_sees_Enemy] 6); +by (dresolve_tac [YM4_analz_sees_Enemy] 6); by (ALLGOALS Asm_simp_tac); -(*YM4*) -by (fast_tac (!claset addSDs [Enemy_analz_Server_msg]) 3); -(*YM3*) -by (Fast_tac 2); -(*Fake*) -by (fast_tac (!claset addSDs [Enemy_analz_Server_msg]) 1); +by (ALLGOALS (fast_tac (!claset addSDs [impOfSubs analz_subset_parts RS + Crypt_imp_Server_msg]))); qed "YM4_imp_Says_Server_A";