# HG changeset patch # User paulson # Date 983535511 -3600 # Node ID 1ea763a5d1867f6a5b53fd1d8b0752b3137da898 # Parent 5d539f1682c3ab2ae93845ce883c8c3d50586d45 conversion of Message.thy to Isar format diff -r 5d539f1682c3 -r 1ea763a5d186 src/HOL/Auth/Event.thy --- a/src/HOL/Auth/Event.thy Fri Mar 02 13:14:37 2001 +0100 +++ b/src/HOL/Auth/Event.thy Fri Mar 02 13:18:31 2001 +0100 @@ -14,12 +14,6 @@ theory Event = Message files ("Event_lemmas.ML"): -(*from Message.ML*) -method_setup spy_analz = {* - Method.no_args (Method.METHOD (fn facts => spy_analz_tac 1)) *} - "for proving the Fake case when analz is involved" - - consts (*Initial states of agents -- parameter of the construction*) initState :: "agent => msg set" diff -r 5d539f1682c3 -r 1ea763a5d186 src/HOL/Auth/Event_lemmas.ML --- a/src/HOL/Auth/Event_lemmas.ML Fri Mar 02 13:14:37 2001 +0100 +++ b/src/HOL/Auth/Event_lemmas.ML Fri Mar 02 13:18:31 2001 +0100 @@ -1,4 +1,4 @@ -(* Title: HOL/Auth/Event +(* Title: HOL/Auth/Event_lemmas ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1996 University of Cambridge @@ -20,8 +20,7 @@ = parts {X} Un parts (knows Spy evs) -- since general case loops*) bind_thm ("parts_insert_knows_Spy", - parts_insert |> - read_instantiate_sg (sign_of thy) [("H", "knows Spy evs")]); + inst "H" "knows Spy evs" parts_insert); val expand_event_case = thm "event.split"; diff -r 5d539f1682c3 -r 1ea763a5d186 src/HOL/Auth/Message.ML --- a/src/HOL/Auth/Message.ML Fri Mar 02 13:14:37 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,912 +0,0 @@ -(* Title: HOL/Auth/Message - ID: $Id$ - Author: Lawrence C Paulson, Cambridge University Computer Laboratory - Copyright 1996 University of Cambridge - -Datatypes of agents and messages; -Inductive relations "parts", "analz" and "synth" -*) - - -(*Eliminates a commonly-occurring expression*) -goal HOL.thy "~ (ALL x. x~=y)"; -by (Blast_tac 1); -Addsimps [result()]; - -AddIffs msg.inject; - -(*Equations hold because constructors are injective; cannot prove for all f*) -Goal "(Friend x : Friend`A) = (x:A)"; -by Auto_tac; -qed "Friend_image_eq"; - -Goal "(Key x : Key`A) = (x:A)"; -by Auto_tac; -qed "Key_image_eq"; - -Goal "(Nonce x ~: Key`A)"; -by Auto_tac; -qed "Nonce_Key_image_eq"; -Addsimps [Friend_image_eq, Key_image_eq, Nonce_Key_image_eq]; - - -(** Inverse of keys **) - -Goal "(invKey K = invKey K') = (K=K')"; -by Safe_tac; -by (rtac box_equals 1); -by (REPEAT (rtac invKey 2)); -by (Asm_simp_tac 1); -qed "invKey_eq"; - -Addsimps [invKey, invKey_eq]; - - -(**** keysFor operator ****) - -Goalw [keysFor_def] "keysFor {} = {}"; -by (Blast_tac 1); -qed "keysFor_empty"; - -Goalw [keysFor_def] "keysFor (H Un H') = keysFor H Un keysFor H'"; -by (Blast_tac 1); -qed "keysFor_Un"; - -Goalw [keysFor_def] "keysFor (UN i:A. H i) = (UN i:A. keysFor (H i))"; -by (Blast_tac 1); -qed "keysFor_UN"; - -(*Monotonicity*) -Goalw [keysFor_def] "G<=H ==> keysFor(G) <= keysFor(H)"; -by (Blast_tac 1); -qed "keysFor_mono"; - -Goalw [keysFor_def] "keysFor (insert (Agent A) H) = keysFor H"; -by Auto_tac; -qed "keysFor_insert_Agent"; - -Goalw [keysFor_def] "keysFor (insert (Nonce N) H) = keysFor H"; -by Auto_tac; -qed "keysFor_insert_Nonce"; - -Goalw [keysFor_def] "keysFor (insert (Number N) H) = keysFor H"; -by Auto_tac; -qed "keysFor_insert_Number"; - -Goalw [keysFor_def] "keysFor (insert (Key K) H) = keysFor H"; -by Auto_tac; -qed "keysFor_insert_Key"; - -Goalw [keysFor_def] "keysFor (insert (Hash X) H) = keysFor H"; -by Auto_tac; -qed "keysFor_insert_Hash"; - -Goalw [keysFor_def] "keysFor (insert {|X,Y|} H) = keysFor H"; -by Auto_tac; -qed "keysFor_insert_MPair"; - -Goalw [keysFor_def] - "keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)"; -by Auto_tac; -qed "keysFor_insert_Crypt"; - -Addsimps [keysFor_empty, keysFor_Un, keysFor_UN, - keysFor_insert_Agent, keysFor_insert_Nonce, - keysFor_insert_Number, keysFor_insert_Key, - keysFor_insert_Hash, keysFor_insert_MPair, keysFor_insert_Crypt]; -AddSEs [keysFor_Un RS equalityD1 RS subsetD RS UnE, - keysFor_UN RS equalityD1 RS subsetD RS UN_E]; - -Goalw [keysFor_def] "keysFor (Key`E) = {}"; -by Auto_tac; -qed "keysFor_image_Key"; -Addsimps [keysFor_image_Key]; - -Goalw [keysFor_def] "Crypt K X : H ==> invKey K : keysFor H"; -by (Blast_tac 1); -qed "Crypt_imp_invKey_keysFor"; - - -(**** Inductive relation "parts" ****) - -val major::prems = -Goal "[| {|X,Y|} : parts H; \ -\ [| X : parts H; Y : parts H |] ==> P \ -\ |] ==> P"; -by (cut_facts_tac [major] 1); -by (resolve_tac prems 1); -by (REPEAT (eresolve_tac [asm_rl, parts.Fst, parts.Snd] 1)); -qed "MPair_parts"; - -AddIs [parts.Inj]; - -AddSEs [MPair_parts, make_elim parts.Body]; -(*NB These two rules are UNSAFE in the formal sense, as they discard the - compound message. They work well on THIS FILE. - MPair_parts is left as SAFE because it speeds up proofs. - The Crypt rule is normally kept UNSAFE to avoid breaking up certificates.*) - -Goal "H <= parts(H)"; -by (Blast_tac 1); -qed "parts_increasing"; - -(*Monotonicity*) -Goalw parts.defs "G<=H ==> parts(G) <= parts(H)"; -by (rtac lfp_mono 1); -by (REPEAT (ares_tac basic_monos 1)); -qed "parts_mono"; - -val parts_insertI = impOfSubs (subset_insertI RS parts_mono); - -Goal "parts{} = {}"; -by Safe_tac; -by (etac parts.induct 1); -by (ALLGOALS Blast_tac); -qed "parts_empty"; -Addsimps [parts_empty]; - -Goal "X: parts{} ==> P"; -by (Asm_full_simp_tac 1); -qed "parts_emptyE"; -AddSEs [parts_emptyE]; - -(*WARNING: loops if H = {Y}, therefore must not be repeated!*) -Goal "X: parts H ==> EX Y:H. X: parts {Y}"; -by (etac parts.induct 1); -by (ALLGOALS Blast_tac); -qed "parts_singleton"; - - -(** Unions **) - -Goal "parts(G) Un parts(H) <= parts(G Un H)"; -by (REPEAT (ares_tac [Un_least, parts_mono, Un_upper1, Un_upper2] 1)); -val parts_Un_subset1 = result(); - -Goal "parts(G Un H) <= parts(G) Un parts(H)"; -by (rtac subsetI 1); -by (etac parts.induct 1); -by (ALLGOALS Blast_tac); -val parts_Un_subset2 = result(); - -Goal "parts(G Un H) = parts(G) Un parts(H)"; -by (REPEAT (ares_tac [equalityI, parts_Un_subset1, parts_Un_subset2] 1)); -qed "parts_Un"; - -Goal "parts (insert X H) = parts {X} Un parts H"; -by (stac (read_instantiate [("A","H")] insert_is_Un) 1); -by (simp_tac (HOL_ss addsimps [parts_Un]) 1); -qed "parts_insert"; - -(*TWO inserts to avoid looping. This rewrite is better than nothing. - Not suitable for Addsimps: its behaviour can be strange.*) -Goal "parts (insert X (insert Y H)) = parts {X} Un parts {Y} Un parts H"; -by (simp_tac (simpset() addsimps [Un_assoc]) 1); -by (simp_tac (simpset() addsimps [parts_insert RS sym]) 1); -qed "parts_insert2"; - -Goal "(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(); - -Goal "parts(UN x:A. H x) <= (UN x:A. parts(H x))"; -by (rtac subsetI 1); -by (etac parts.induct 1); -by (ALLGOALS Blast_tac); -val parts_UN_subset2 = result(); - -Goal "parts(UN x:A. H x) = (UN x:A. parts(H x))"; -by (REPEAT (ares_tac [equalityI, parts_UN_subset1, parts_UN_subset2] 1)); -qed "parts_UN"; - -(*Added to simplify arguments to parts, analz and synth. - NOTE: the UN versions are no longer used!*) -Addsimps [parts_Un, parts_UN]; -AddSEs [parts_Un RS equalityD1 RS subsetD RS UnE, - parts_UN RS equalityD1 RS subsetD RS UN_E]; - -Goal "insert X (parts H) <= parts(insert X H)"; -by (blast_tac (claset() addIs [impOfSubs parts_mono]) 1); -qed "parts_insert_subset"; - -(** Idempotence and transitivity **) - -Goal "X: parts (parts H) ==> X: parts H"; -by (etac parts.induct 1); -by (ALLGOALS Blast_tac); -qed "parts_partsD"; -AddSDs [parts_partsD]; - -Goal "parts (parts H) = parts H"; -by (Blast_tac 1); -qed "parts_idem"; -Addsimps [parts_idem]; - -Goal "[| X: parts G; G <= parts H |] ==> X: parts H"; -by (dtac parts_mono 1); -by (Blast_tac 1); -qed "parts_trans"; - -(*Cut*) -Goal "[| Y: parts (insert X G); X: parts H |] \ -\ ==> Y: parts (G Un H)"; -by (etac parts_trans 1); -by Auto_tac; -qed "parts_cut"; - -Goal "X: parts H ==> parts (insert X H) = parts H"; -by (fast_tac (claset() addSDs [parts_cut] - addIs [parts_insertI] - addss (simpset())) 1); -qed "parts_cut_eq"; - -Addsimps [parts_cut_eq]; - - -(** Rewrite rules for pulling out atomic messages **) - -fun parts_tac i = - EVERY [rtac ([subsetI, parts_insert_subset] MRS equalityI) i, - etac parts.induct i, - Auto_tac]; - -Goal "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)"; -by (parts_tac 1); -qed "parts_insert_Agent"; - -Goal "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)"; -by (parts_tac 1); -qed "parts_insert_Nonce"; - -Goal "parts (insert (Number N) H) = insert (Number N) (parts H)"; -by (parts_tac 1); -qed "parts_insert_Number"; - -Goal "parts (insert (Key K) H) = insert (Key K) (parts H)"; -by (parts_tac 1); -qed "parts_insert_Key"; - -Goal "parts (insert (Hash X) H) = insert (Hash X) (parts H)"; -by (parts_tac 1); -qed "parts_insert_Hash"; - -Goal "parts (insert (Crypt K X) H) = \ -\ insert (Crypt K X) (parts (insert X H))"; -by (rtac equalityI 1); -by (rtac subsetI 1); -by (etac parts.induct 1); -by Auto_tac; -by (etac parts.induct 1); -by (ALLGOALS (blast_tac (claset() addIs [parts.Body]))); -qed "parts_insert_Crypt"; - -Goal "parts (insert {|X,Y|} H) = \ -\ insert {|X,Y|} (parts (insert X (insert Y H)))"; -by (rtac equalityI 1); -by (rtac subsetI 1); -by (etac parts.induct 1); -by Auto_tac; -by (etac parts.induct 1); -by (ALLGOALS (blast_tac (claset() addIs [parts.Fst, parts.Snd]))); -qed "parts_insert_MPair"; - -Addsimps [parts_insert_Agent, parts_insert_Nonce, - parts_insert_Number, parts_insert_Key, - parts_insert_Hash, parts_insert_Crypt, parts_insert_MPair]; - - -Goal "parts (Key`N) = Key`N"; -by Auto_tac; -by (etac parts.induct 1); -by Auto_tac; -qed "parts_image_Key"; -Addsimps [parts_image_Key]; - - -(*In any message, there is an upper bound N on its greatest nonce.*) -Goal "EX N. ALL n. N<=n --> Nonce n ~: parts {msg}"; -by (induct_tac "msg" 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps [exI, parts_insert2]))); -(*MPair case: blast_tac works out the necessary sum itself!*) -by (blast_tac (claset() addSEs [add_leE]) 2); -(*Nonce case*) -by (res_inst_tac [("x","N + Suc nat")] exI 1); -by (auto_tac (claset() addSEs [add_leE], simpset())); -qed "msg_Nonce_supply"; - - -(**** Inductive relation "analz" ****) - -val major::prems = -Goal "[| {|X,Y|} : analz H; \ -\ [| X : analz H; Y : analz H |] ==> P \ -\ |] ==> P"; -by (cut_facts_tac [major] 1); -by (resolve_tac prems 1); -by (REPEAT (eresolve_tac [asm_rl, analz.Fst, analz.Snd] 1)); -qed "MPair_analz"; - -AddSEs [MPair_analz]; (*Making it safe speeds up proofs*) -AddDs [analz.Decrypt]; (*Unsafe: we don't want to split up certificates!*) -AddIs [analz.Inj]; - -Addsimps [analz.Inj]; - -Goal "H <= analz(H)"; -by (Blast_tac 1); -qed "analz_increasing"; - -Goal "analz H <= parts H"; -by (rtac subsetI 1); -by (etac analz.induct 1); -by (ALLGOALS Blast_tac); -qed "analz_subset_parts"; - -bind_thm ("not_parts_not_analz", analz_subset_parts RS contra_subsetD); - - -Goal "parts (analz H) = parts H"; -by (rtac equalityI 1); -by (rtac (analz_subset_parts RS parts_mono RS subset_trans) 1); -by (Simp_tac 1); -by (blast_tac (claset() addIs [analz_increasing RS parts_mono RS subsetD]) 1); -qed "parts_analz"; -Addsimps [parts_analz]; - -Goal "analz (parts H) = parts H"; -by Auto_tac; -by (etac analz.induct 1); -by Auto_tac; -qed "analz_parts"; -Addsimps [analz_parts]; - -(*Monotonicity; Lemma 1 of Lowe*) -Goalw analz.defs "G<=H ==> analz(G) <= analz(H)"; -by (rtac lfp_mono 1); -by (REPEAT (ares_tac basic_monos 1)); -qed "analz_mono"; - -bind_thm ("analz_insertI", impOfSubs (subset_insertI RS analz_mono)); - -(** General equational properties **) - -Goal "analz{} = {}"; -by Safe_tac; -by (etac analz.induct 1); -by (ALLGOALS Blast_tac); -qed "analz_empty"; -Addsimps [analz_empty]; - -(*Converse fails: we can analz more from the union than from the - separate parts, as a key in one might decrypt a message in the other*) -Goal "analz(G) Un analz(H) <= analz(G Un H)"; -by (REPEAT (ares_tac [Un_least, analz_mono, Un_upper1, Un_upper2] 1)); -qed "analz_Un"; - -Goal "insert X (analz H) <= analz(insert X H)"; -by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1); -qed "analz_insert"; - -(** Rewrite rules for pulling out atomic messages **) - -fun analz_tac i = - EVERY [rtac ([subsetI, analz_insert] MRS equalityI) i, - etac analz.induct i, - Auto_tac]; - -Goal "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)"; -by (analz_tac 1); -qed "analz_insert_Agent"; - -Goal "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)"; -by (analz_tac 1); -qed "analz_insert_Nonce"; - -Goal "analz (insert (Number N) H) = insert (Number N) (analz H)"; -by (analz_tac 1); -qed "analz_insert_Number"; - -Goal "analz (insert (Hash X) H) = insert (Hash X) (analz H)"; -by (analz_tac 1); -qed "analz_insert_Hash"; - -(*Can only pull out Keys if they are not needed to decrypt the rest*) -Goalw [keysFor_def] - "K ~: keysFor (analz H) ==> \ -\ analz (insert (Key K) H) = insert (Key K) (analz H)"; -by (analz_tac 1); -qed "analz_insert_Key"; - -Goal "analz (insert {|X,Y|} H) = \ -\ insert {|X,Y|} (analz (insert X (insert Y H)))"; -by (rtac equalityI 1); -by (rtac subsetI 1); -by (etac analz.induct 1); -by Auto_tac; -by (etac analz.induct 1); -by (ALLGOALS (blast_tac (claset() addIs [analz.Fst, analz.Snd]))); -qed "analz_insert_MPair"; - -(*Can pull out enCrypted message if the Key is not known*) -Goal "Key (invKey K) ~: analz H ==> \ -\ analz (insert (Crypt K X) H) = \ -\ insert (Crypt K X) (analz H)"; -by (analz_tac 1); -qed "analz_insert_Crypt"; - -Goal "Key (invKey K) : analz H ==> \ -\ analz (insert (Crypt K X) H) <= \ -\ insert (Crypt K X) (analz (insert X H))"; -by (rtac subsetI 1); -by (eres_inst_tac [("xa","x")] analz.induct 1); -by Auto_tac; -val lemma1 = result(); - -Goal "Key (invKey K) : analz H ==> \ -\ insert (Crypt K X) (analz (insert X H)) <= \ -\ analz (insert (Crypt K X) H)"; -by Auto_tac; -by (eres_inst_tac [("xa","x")] analz.induct 1); -by Auto_tac; -by (blast_tac (claset() addIs [analz_insertI, analz.Decrypt]) 1); -val lemma2 = result(); - -Goal "Key (invKey K) : analz H ==> \ -\ analz (insert (Crypt K X) H) = \ -\ insert (Crypt K X) (analz (insert X H))"; -by (REPEAT (ares_tac [equalityI, lemma1, lemma2] 1)); -qed "analz_insert_Decrypt"; - -(*Case analysis: either the message is secure, or it is not! - Effective, but can cause subgoals to blow up! - Use with split_if; apparently split_tac does not cope with patterns - such as "analz (insert (Crypt K X) H)" *) -Goal "analz (insert (Crypt K X) H) = \ -\ (if (Key (invKey K) : analz H) \ -\ then insert (Crypt K X) (analz (insert X H)) \ -\ else insert (Crypt K X) (analz H))"; -by (case_tac "Key (invKey K) : analz H " 1); -by (ALLGOALS (asm_simp_tac (simpset() addsimps [analz_insert_Crypt, - analz_insert_Decrypt]))); -qed "analz_Crypt_if"; - -Addsimps [analz_insert_Agent, analz_insert_Nonce, - analz_insert_Number, analz_insert_Key, - analz_insert_Hash, analz_insert_MPair, analz_Crypt_if]; - -(*This rule supposes "for the sake of argument" that we have the key.*) -Goal "analz (insert (Crypt K X) H) <= \ -\ insert (Crypt K X) (analz (insert X H))"; -by (rtac subsetI 1); -by (etac analz.induct 1); -by Auto_tac; -qed "analz_insert_Crypt_subset"; - - -Goal "analz (Key`N) = Key`N"; -by Auto_tac; -by (etac analz.induct 1); -by Auto_tac; -qed "analz_image_Key"; - -Addsimps [analz_image_Key]; - - -(** Idempotence and transitivity **) - -Goal "X: analz (analz H) ==> X: analz H"; -by (etac analz.induct 1); -by (ALLGOALS Blast_tac); -qed "analz_analzD"; -AddSDs [analz_analzD]; - -Goal "analz (analz H) = analz H"; -by (Blast_tac 1); -qed "analz_idem"; -Addsimps [analz_idem]; - -Goal "[| X: analz G; G <= analz H |] ==> X: analz H"; -by (dtac analz_mono 1); -by (Blast_tac 1); -qed "analz_trans"; - -(*Cut; Lemma 2 of Lowe*) -Goal "[| Y: analz (insert X H); X: analz H |] ==> Y: analz H"; -by (etac analz_trans 1); -by (Blast_tac 1); -qed "analz_cut"; - -(*Cut can be proved easily by induction on - "Y: analz (insert X H) ==> X: analz H --> Y: analz H" -*) - -(*This rewrite rule helps in the simplification of messages that involve - the forwarding of unknown components (X). Without it, removing occurrences - of X can be very complicated. *) -Goal "X: analz H ==> analz (insert X H) = analz H"; -by (blast_tac (claset() addIs [analz_cut, analz_insertI]) 1); -qed "analz_insert_eq"; - - -(** A congruence rule for "analz" **) - -Goal "[| analz G <= analz G'; analz H <= analz H' \ -\ |] ==> analz (G Un H) <= analz (G' Un H')"; -by (Clarify_tac 1); -by (etac analz.induct 1); -by (ALLGOALS (best_tac (claset() addIs [analz_mono RS subsetD]))); -qed "analz_subset_cong"; - -Goal "[| analz G = analz G'; analz H = analz H' \ -\ |] ==> analz (G Un H) = analz (G' Un H')"; -by (REPEAT_FIRST (ares_tac [equalityI, analz_subset_cong] - ORELSE' etac equalityE)); -qed "analz_cong"; - - -Goal "analz H = analz H' ==> analz(insert X H) = analz(insert X H')"; -by (asm_simp_tac (simpset() addsimps [insert_def] delsimps [singleton_conv] - setloop (rtac analz_cong)) 1); -qed "analz_insert_cong"; - -(*If there are no pairs or encryptions then analz does nothing*) -Goal "[| ALL X Y. {|X,Y|} ~: H; ALL X K. Crypt K X ~: H |] ==> \ -\ analz H = H"; -by Safe_tac; -by (etac analz.induct 1); -by (ALLGOALS Blast_tac); -qed "analz_trivial"; - -(*These two are obsolete (with a single Spy) but cost little to prove...*) -Goal "X: analz (UN i:A. analz (H i)) ==> X: analz (UN i:A. H i)"; -by (etac analz.induct 1); -by (ALLGOALS (blast_tac (claset() addIs [impOfSubs analz_mono]))); -val lemma = result(); - -Goal "analz (UN i:A. analz (H i)) = analz (UN i:A. H i)"; -by (blast_tac (claset() addIs [lemma, impOfSubs analz_mono]) 1); -qed "analz_UN_analz"; -Addsimps [analz_UN_analz]; - - -(**** Inductive relation "synth" ****) - -AddIs synth.intrs; - -(*NO Agent_synth, as any Agent name can be synthesized. Ditto for Number*) -val Nonce_synth = synth.mk_cases "Nonce n : synth H"; -val Key_synth = synth.mk_cases "Key K : synth H"; -val Hash_synth = synth.mk_cases "Hash X : synth H"; -val MPair_synth = synth.mk_cases "{|X,Y|} : synth H"; -val Crypt_synth = synth.mk_cases "Crypt K X : synth H"; - -AddSEs [Nonce_synth, Key_synth, Hash_synth, MPair_synth, Crypt_synth]; - -Goal "H <= synth(H)"; -by (Blast_tac 1); -qed "synth_increasing"; - -(*Monotonicity*) -Goalw synth.defs "G<=H ==> synth(G) <= synth(H)"; -by (rtac lfp_mono 1); -by (REPEAT (ares_tac basic_monos 1)); -qed "synth_mono"; - -(** Unions **) - -(*Converse fails: we can synth more from the union than from the - separate parts, building a compound message using elements of each.*) -Goal "synth(G) Un synth(H) <= synth(G Un H)"; -by (REPEAT (ares_tac [Un_least, synth_mono, Un_upper1, Un_upper2] 1)); -qed "synth_Un"; - -Goal "insert X (synth H) <= synth(insert X H)"; -by (blast_tac (claset() addIs [impOfSubs synth_mono]) 1); -qed "synth_insert"; - -(** Idempotence and transitivity **) - -Goal "X: synth (synth H) ==> X: synth H"; -by (etac synth.induct 1); -by (ALLGOALS Blast_tac); -qed "synth_synthD"; -AddSDs [synth_synthD]; - -Goal "synth (synth H) = synth H"; -by (Blast_tac 1); -qed "synth_idem"; - -Goal "[| X: synth G; G <= synth H |] ==> X: synth H"; -by (dtac synth_mono 1); -by (Blast_tac 1); -qed "synth_trans"; - -(*Cut; Lemma 2 of Lowe*) -Goal "[| Y: synth (insert X H); X: synth H |] ==> Y: synth H"; -by (etac synth_trans 1); -by (Blast_tac 1); -qed "synth_cut"; - -Goal "Agent A : synth H"; -by (Blast_tac 1); -qed "Agent_synth"; - -Goal "Number n : synth H"; -by (Blast_tac 1); -qed "Number_synth"; - -Goal "(Nonce N : synth H) = (Nonce N : H)"; -by (Blast_tac 1); -qed "Nonce_synth_eq"; - -Goal "(Key K : synth H) = (Key K : H)"; -by (Blast_tac 1); -qed "Key_synth_eq"; - -Goal "Key K ~: H ==> (Crypt K X : synth H) = (Crypt K X : H)"; -by (Blast_tac 1); -qed "Crypt_synth_eq"; - -Addsimps [Agent_synth, Number_synth, - Nonce_synth_eq, Key_synth_eq, Crypt_synth_eq]; - - -Goalw [keysFor_def] - "keysFor (synth H) = keysFor H Un invKey`{K. Key K : H}"; -by (Blast_tac 1); -qed "keysFor_synth"; -Addsimps [keysFor_synth]; - - -(*** Combinations of parts, analz and synth ***) - -Goal "parts (synth H) = parts H Un synth H"; -by (rtac equalityI 1); -by (rtac subsetI 1); -by (etac parts.induct 1); -by (ALLGOALS - (blast_tac (claset() addIs ((synth_increasing RS parts_mono RS subsetD) - ::parts.intrs)))); -qed "parts_synth"; -Addsimps [parts_synth]; - -Goal "analz (analz G Un H) = analz (G Un H)"; -by (REPEAT_FIRST (resolve_tac [equalityI, analz_subset_cong])); -by (ALLGOALS Simp_tac); -qed "analz_analz_Un"; - -Goal "analz (synth G Un H) = analz (G Un H) Un synth G"; -by (rtac equalityI 1); -by (rtac subsetI 1); -by (etac analz.induct 1); -by (blast_tac (claset() addIs [impOfSubs analz_mono]) 5); -by (ALLGOALS (blast_tac (claset() addIs analz.intrs))); -qed "analz_synth_Un"; - -Goal "analz (synth H) = analz H Un synth H"; -by (cut_inst_tac [("H","{}")] analz_synth_Un 1); -by (Full_simp_tac 1); -qed "analz_synth"; -Addsimps [analz_analz_Un, analz_synth_Un, analz_synth]; - - -(** For reasoning about the Fake rule in traces **) - -Goal "X: G ==> parts(insert X H) <= parts G Un parts H"; -by (rtac ([parts_mono, parts_Un_subset2] MRS subset_trans) 1); -by (Blast_tac 1); -qed "parts_insert_subset_Un"; - -(*More specifically for Fake. Very occasionally we could do with a version - of the form parts{X} <= synth (analz H) Un parts H *) -Goal "X: synth (analz H) ==> \ -\ parts (insert X H) <= synth (analz H) Un parts H"; -by (dtac parts_insert_subset_Un 1); -by (Full_simp_tac 1); -by (Blast_tac 1); -qed "Fake_parts_insert"; - -(*H is sometimes (Key ` KK Un spies evs), so can't put G=H*) -Goal "X: synth (analz G) ==> \ -\ analz (insert X H) <= synth (analz G) Un analz (G Un H)"; -by (rtac subsetI 1); -by (subgoal_tac "x : analz (synth (analz G) Un H)" 1); -by (blast_tac (claset() addIs [impOfSubs analz_mono, - impOfSubs (analz_mono RS synth_mono)]) 2); -by (Full_simp_tac 1); -by (Blast_tac 1); -qed "Fake_analz_insert"; - -Goal "(X: analz H & X: parts H) = (X: analz H)"; -by (blast_tac (claset() addIs [impOfSubs analz_subset_parts]) 1); -val analz_conj_parts = result(); - -Goal "(X: analz H | X: parts H) = (X: parts H)"; -by (blast_tac (claset() addIs [impOfSubs analz_subset_parts]) 1); -val analz_disj_parts = result(); - -AddIffs [analz_conj_parts, analz_disj_parts]; - -(*Without this equation, other rules for synth and analz would yield - redundant cases*) -Goal "({|X,Y|} : synth (analz H)) = \ -\ (X : synth (analz H) & Y : synth (analz H))"; -by (Blast_tac 1); -qed "MPair_synth_analz"; - -AddIffs [MPair_synth_analz]; - -Goal "[| Key K : analz H; Key (invKey K) : analz H |] \ -\ ==> (Crypt K X : synth (analz H)) = (X : synth (analz H))"; -by (Blast_tac 1); -qed "Crypt_synth_analz"; - - -Goal "X ~: synth (analz H) \ -\ ==> (Hash{|X,Y|} : synth (analz H)) = (Hash{|X,Y|} : analz H)"; -by (Blast_tac 1); -qed "Hash_synth_analz"; -Addsimps [Hash_synth_analz]; - - -(**** HPair: a combination of Hash and MPair ****) - -(*** Freeness ***) - -Goalw [HPair_def] "Agent A ~= Hash[X] Y"; -by (Simp_tac 1); -qed "Agent_neq_HPair"; - -Goalw [HPair_def] "Nonce N ~= Hash[X] Y"; -by (Simp_tac 1); -qed "Nonce_neq_HPair"; - -Goalw [HPair_def] "Number N ~= Hash[X] Y"; -by (Simp_tac 1); -qed "Number_neq_HPair"; - -Goalw [HPair_def] "Key K ~= Hash[X] Y"; -by (Simp_tac 1); -qed "Key_neq_HPair"; - -Goalw [HPair_def] "Hash Z ~= Hash[X] Y"; -by (Simp_tac 1); -qed "Hash_neq_HPair"; - -Goalw [HPair_def] "Crypt K X' ~= Hash[X] Y"; -by (Simp_tac 1); -qed "Crypt_neq_HPair"; - -val HPair_neqs = [Agent_neq_HPair, Nonce_neq_HPair, Number_neq_HPair, - Key_neq_HPair, Hash_neq_HPair, Crypt_neq_HPair]; - -AddIffs HPair_neqs; -AddIffs (HPair_neqs RL [not_sym]); - -Goalw [HPair_def] "(Hash[X'] Y' = Hash[X] Y) = (X' = X & Y'=Y)"; -by (Simp_tac 1); -qed "HPair_eq"; - -Goalw [HPair_def] "({|X',Y'|} = Hash[X] Y) = (X' = Hash{|X,Y|} & Y'=Y)"; -by (Simp_tac 1); -qed "MPair_eq_HPair"; - -Goalw [HPair_def] "(Hash[X] Y = {|X',Y'|}) = (X' = Hash{|X,Y|} & Y'=Y)"; -by Auto_tac; -qed "HPair_eq_MPair"; - -AddIffs [HPair_eq, MPair_eq_HPair, HPair_eq_MPair]; - - -(*** Specialized laws, proved in terms of those for Hash and MPair ***) - -Goalw [HPair_def] "keysFor (insert (Hash[X] Y) H) = keysFor H"; -by (Simp_tac 1); -qed "keysFor_insert_HPair"; - -Goalw [HPair_def] - "parts (insert (Hash[X] Y) H) = \ -\ insert (Hash[X] Y) (insert (Hash{|X,Y|}) (parts (insert Y H)))"; -by (Simp_tac 1); -qed "parts_insert_HPair"; - -Goalw [HPair_def] - "analz (insert (Hash[X] Y) H) = \ -\ insert (Hash[X] Y) (insert (Hash{|X,Y|}) (analz (insert Y H)))"; -by (Simp_tac 1); -qed "analz_insert_HPair"; - -Goalw [HPair_def] "X ~: synth (analz H) \ -\ ==> (Hash[X] Y : synth (analz H)) = \ -\ (Hash {|X, Y|} : analz H & Y : synth (analz H))"; -by (Simp_tac 1); -by (Blast_tac 1); -qed "HPair_synth_analz"; - -Addsimps [keysFor_insert_HPair, parts_insert_HPair, analz_insert_HPair, - HPair_synth_analz, HPair_synth_analz]; - - -(*We do NOT want Crypt... messages broken up in protocols!!*) -Delrules [make_elim parts.Body]; - - -(** Rewrites to push in Key and Crypt messages, so that other messages can - be pulled out using the analz_insert rules **) - -fun insComm thy x y = read_instantiate_sg (sign_of thy) [("x",x), ("y",y)] - insert_commute; - -val pushKeys = map (insComm thy "Key ?K") - ["Agent ?C", "Nonce ?N", "Number ?N", - "Hash ?X", "MPair ?X ?Y", "Crypt ?X ?K'"]; - -val pushCrypts = map (insComm thy "Crypt ?X ?K") - ["Agent ?C", "Nonce ?N", "Number ?N", - "Hash ?X'", "MPair ?X' ?Y"]; - -(*Cannot be added with Addsimps -- we don't always want to re-order messages*) -bind_thms ("pushes", pushKeys@pushCrypts); - - -(*** Tactics useful for many protocol proofs ***) - -(*Prove base case (subgoal i) and simplify others. A typical base case - concerns Crypt K X ~: Key`shrK`bad and cannot be proved by rewriting - alone.*) -fun prove_simple_subgoals_tac i = - force_tac (claset(), simpset() addsimps [image_eq_UN]) i THEN - ALLGOALS Asm_simp_tac; - -fun Fake_parts_insert_tac i = - blast_tac (claset() addIs [parts_insertI] - addDs [impOfSubs analz_subset_parts, - impOfSubs Fake_parts_insert]) i; - -(*Apply rules to break down assumptions of the form - Y : parts(insert X H) and Y : analz(insert X H) -*) -val Fake_insert_tac = - dresolve_tac [impOfSubs Fake_analz_insert, - impOfSubs Fake_parts_insert] THEN' - eresolve_tac [asm_rl, synth.Inj]; - -fun Fake_insert_simp_tac i = - REPEAT (Fake_insert_tac i) THEN Asm_full_simp_tac i; - - -(*Analysis of Fake cases. Also works for messages that forward unknown parts, - but this application is no longer necessary if analz_insert_eq is used. - Abstraction over i is ESSENTIAL: it delays the dereferencing of claset - DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *) - -val atomic_spy_analz_tac = SELECT_GOAL - (Fake_insert_simp_tac 1 - THEN - IF_UNSOLVED (Blast.depth_tac - (claset() addIs [analz_insertI, - impOfSubs analz_subset_parts]) 4 1)); - -fun spy_analz_tac i = - DETERM - (SELECT_GOAL - (EVERY - [ (*push in occurrences of X...*) - (REPEAT o CHANGED) - (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1), - (*...allowing further simplifications*) - Simp_tac 1, - REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])), - DEPTH_SOLVE (atomic_spy_analz_tac 1)]) i); - - -(*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*) -goal Set.thy "A Un (B Un A) = B Un A"; -by (Blast_tac 1); -val Un_absorb3 = result(); -Addsimps [Un_absorb3]; - -(*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]; diff -r 5d539f1682c3 -r 1ea763a5d186 src/HOL/Auth/Message.thy --- a/src/HOL/Auth/Message.thy Fri Mar 02 13:14:37 2001 +0100 +++ b/src/HOL/Auth/Message.thy Fri Mar 02 13:18:31 2001 +0100 @@ -7,22 +7,31 @@ Inductive relations "parts", "analz" and "synth" *) -Message = Main + +theory Message = Main +files ("Message_lemmas.ML"): + +(*Eliminates a commonly-occurring expression*) +lemma [simp] : "~ (ALL x. x~=y)" +by blast + +(*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*) +lemma [simp] : "A Un (B Un A) = B Un A" +by blast types key = nat consts - invKey :: key=>key + invKey :: "key=>key" -rules - invKey "invKey (invKey K) = K" +axioms + invKey [simp] : "invKey (invKey K) = K" (*The inverse of a symmetric key is itself; that of a public key is the private key and vice versa*) constdefs - isSymKey :: key=>bool + isSymKey :: "key=>bool" "isSymKey K == (invKey K = K)" datatype (*We allow any number of friendly agents*) @@ -43,7 +52,7 @@ "@MTuple" :: "['a, args] => 'a * 'b" ("(2{|_,/ _|})") syntax (xsymbols) - "@MTuple" :: "['a, args] => 'a * 'b" ("(2\\_,/ _\\)") + "@MTuple" :: "['a, args] => 'a * 'b" ("(2\_,/ _\)") translations "{|x, y, z|}" == "{|x, {|y, z|}|}" @@ -52,50 +61,86 @@ constdefs (*Message Y, paired with a MAC computed with the help of X*) - HPair :: "[msg,msg]=>msg" ("(4Hash[_] /_)" [0, 1000]) + HPair :: "[msg,msg] => msg" ("(4Hash[_] /_)" [0, 1000]) "Hash[X] Y == {| Hash{|X,Y|}, Y|}" (*Keys useful to decrypt elements of a message set*) - keysFor :: msg set => key set + keysFor :: "msg set => key set" "keysFor H == invKey ` {K. EX X. Crypt K X : H}" (** Inductive definition of all "parts" of a message. **) -consts parts :: msg set => msg set +consts parts :: "msg set => msg set" inductive "parts H" - intrs - Inj "X: H ==> X: parts H" - Fst "{|X,Y|} : parts H ==> X : parts H" - Snd "{|X,Y|} : parts H ==> Y : parts H" - Body "Crypt K X : parts H ==> X : parts H" + intros + Inj [intro] : "X: H ==> X : parts H" + Fst: "{|X,Y|} : parts H ==> X : parts H" + Snd: "{|X,Y|} : parts H ==> Y : parts H" + Body: "Crypt K X : parts H ==> X : parts H" + + +(*Monotonicity*) +lemma parts_mono: "G<=H ==> parts(G) <= parts(H)" +apply auto +apply (erule parts.induct) +apply (auto dest: Fst Snd Body) +done (** Inductive definition of "analz" -- what can be broken down from a set of messages, including keys. A form of downward closure. Pairs can be taken apart; messages decrypted with known keys. **) -consts analz :: msg set => msg set +consts analz :: "msg set => msg set" inductive "analz H" - intrs - Inj "X: H ==> X: analz H" - Fst "{|X,Y|} : analz H ==> X : analz H" - Snd "{|X,Y|} : analz H ==> Y : analz H" - Decrypt "[| Crypt K X : analz H; Key(invKey K): analz H |] ==> X : analz H" + intros + Inj [intro,simp] : "X: H ==> X: analz H" + Fst: "{|X,Y|} : analz H ==> X : analz H" + Snd: "{|X,Y|} : analz H ==> Y : analz H" + Decrypt [dest]: + "[|Crypt K X : analz H; Key(invKey K): analz H|] ==> X : analz H" +(*Monotonicity; Lemma 1 of Lowe's paper*) +lemma analz_mono: "G<=H ==> analz(G) <= analz(H)" +apply auto +apply (erule analz.induct) +apply (auto dest: Fst Snd) +done + (** Inductive definition of "synth" -- what can be built up from a set of messages. A form of upward closure. Pairs can be built, messages encrypted with known keys. Agent names are public domain. Numbers can be guessed, but Nonces cannot be. **) -consts synth :: msg set => msg set +consts synth :: "msg set => msg set" inductive "synth H" - intrs - Inj "X: H ==> X: synth H" - Agent "Agent agt : synth H" - Number "Number n : synth H" - Hash "X: synth H ==> Hash X : synth H" - MPair "[| X: synth H; Y: synth H |] ==> {|X,Y|} : synth H" - Crypt "[| X: synth H; Key(K) : H |] ==> Crypt K X : synth H" + intros + Inj [intro]: "X: H ==> X: synth H" + Agent [intro]: "Agent agt : synth H" + Number [intro]: "Number n : synth H" + Hash [intro]: "X: synth H ==> Hash X : synth H" + MPair [intro]: "[|X: synth H; Y: synth H|] ==> {|X,Y|} : synth H" + Crypt [intro]: "[|X: synth H; Key(K) : H|] ==> Crypt K X : synth H" + +(*Monotonicity*) +lemma synth_mono: "G<=H ==> synth(G) <= synth(H)" +apply auto +apply (erule synth.induct) +apply (auto dest: Fst Snd Body) +done + +(*NO Agent_synth, as any Agent name can be synthesized. Ditto for Number*) +inductive_cases Nonce_synth [elim!]: "Nonce n : synth H" +inductive_cases Key_synth [elim!]: "Key K : synth H" +inductive_cases Hash_synth [elim!]: "Hash X : synth H" +inductive_cases MPair_synth [elim!]: "{|X,Y|} : synth H" +inductive_cases Crypt_synth [elim!]: "Crypt K X : synth H" + +use "Message_lemmas.ML" + +method_setup spy_analz = {* + Method.no_args (Method.METHOD (fn facts => spy_analz_tac 1)) *} + "for proving the Fake case when analz is involved" end diff -r 5d539f1682c3 -r 1ea763a5d186 src/HOL/Auth/Message_lemmas.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Auth/Message_lemmas.ML Fri Mar 02 13:18:31 2001 +0100 @@ -0,0 +1,900 @@ +(* Title: HOL/Auth/Message + ID: $Id$ + Author: Lawrence C Paulson, Cambridge University Computer Laboratory + Copyright 1996 University of Cambridge + +Datatypes of agents and messages; +Inductive relations "parts", "analz" and "synth" +*) + +(*ML bindings for definitions and axioms*) +val invKey = thm "invKey"; +val keysFor_def = thm "keysFor_def"; +val parts_mono = thm "parts_mono"; +val analz_mono = thm "analz_mono"; +val synth_mono = thm "synth_mono"; +val HPair_def = thm "HPair_def"; +val isSymKey_def = thm "isSymKey_def"; + +structure parts = + struct + val induct = thm "parts.induct"; + val Inj = thm "parts.Inj"; + val Fst = thm "parts.Fst"; + val Snd = thm "parts.Snd"; + val Body = thm "parts.Body"; + end; + +structure analz = + struct + val induct = thm "analz.induct"; + val Inj = thm "analz.Inj"; + val Fst = thm "analz.Fst"; + val Snd = thm "analz.Snd"; + val Decrypt = thm "analz.Decrypt"; + end; + +structure synth = + struct + val induct = thm "synth.induct"; + val Inj = thm "synth.Inj"; + val Agent = thm "synth.Agent"; + val Number = thm "synth.Number"; + val Hash = thm "synth.Hash"; + val Crypt = thm "synth.Crypt"; + end; + + +(*Equations hold because constructors are injective; cannot prove for all f*) +Goal "(Friend x : Friend`A) = (x:A)"; +by Auto_tac; +qed "Friend_image_eq"; + +Goal "(Key x : Key`A) = (x:A)"; +by Auto_tac; +qed "Key_image_eq"; + +Goal "(Nonce x ~: Key`A)"; +by Auto_tac; +qed "Nonce_Key_image_eq"; +Addsimps [Friend_image_eq, Key_image_eq, Nonce_Key_image_eq]; + + +(** Inverse of keys **) + +Goal "(invKey K = invKey K') = (K=K')"; +by Safe_tac; +by (rtac box_equals 1); +by (REPEAT (rtac invKey 2)); +by (Asm_simp_tac 1); +qed "invKey_eq"; + +Addsimps [invKey_eq]; + + +(**** keysFor operator ****) + +Goalw [keysFor_def] "keysFor {} = {}"; +by (Blast_tac 1); +qed "keysFor_empty"; + +Goalw [keysFor_def] "keysFor (H Un H') = keysFor H Un keysFor H'"; +by (Blast_tac 1); +qed "keysFor_Un"; + +Goalw [keysFor_def] "keysFor (UN i:A. H i) = (UN i:A. keysFor (H i))"; +by (Blast_tac 1); +qed "keysFor_UN"; + +(*Monotonicity*) +Goalw [keysFor_def] "G<=H ==> keysFor(G) <= keysFor(H)"; +by (Blast_tac 1); +qed "keysFor_mono"; + +Goalw [keysFor_def] "keysFor (insert (Agent A) H) = keysFor H"; +by Auto_tac; +qed "keysFor_insert_Agent"; + +Goalw [keysFor_def] "keysFor (insert (Nonce N) H) = keysFor H"; +by Auto_tac; +qed "keysFor_insert_Nonce"; + +Goalw [keysFor_def] "keysFor (insert (Number N) H) = keysFor H"; +by Auto_tac; +qed "keysFor_insert_Number"; + +Goalw [keysFor_def] "keysFor (insert (Key K) H) = keysFor H"; +by Auto_tac; +qed "keysFor_insert_Key"; + +Goalw [keysFor_def] "keysFor (insert (Hash X) H) = keysFor H"; +by Auto_tac; +qed "keysFor_insert_Hash"; + +Goalw [keysFor_def] "keysFor (insert {|X,Y|} H) = keysFor H"; +by Auto_tac; +qed "keysFor_insert_MPair"; + +Goalw [keysFor_def] + "keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)"; +by Auto_tac; +qed "keysFor_insert_Crypt"; + +Addsimps [keysFor_empty, keysFor_Un, keysFor_UN, + keysFor_insert_Agent, keysFor_insert_Nonce, + keysFor_insert_Number, keysFor_insert_Key, + keysFor_insert_Hash, keysFor_insert_MPair, keysFor_insert_Crypt]; +AddSEs [keysFor_Un RS equalityD1 RS subsetD RS UnE, + keysFor_UN RS equalityD1 RS subsetD RS UN_E]; + +Goalw [keysFor_def] "keysFor (Key`E) = {}"; +by Auto_tac; +qed "keysFor_image_Key"; +Addsimps [keysFor_image_Key]; + +Goalw [keysFor_def] "Crypt K X : H ==> invKey K : keysFor H"; +by (Blast_tac 1); +qed "Crypt_imp_invKey_keysFor"; + + +(**** Inductive relation "parts" ****) + +val major::prems = +Goal "[| {|X,Y|} : parts H; \ +\ [| X : parts H; Y : parts H |] ==> P \ +\ |] ==> P"; +by (cut_facts_tac [major] 1); +by (resolve_tac prems 1); +by (REPEAT (eresolve_tac [asm_rl, parts.Fst, parts.Snd] 1)); +qed "MPair_parts"; + +AddSEs [MPair_parts, make_elim parts.Body]; +(*NB These two rules are UNSAFE in the formal sense, as they discard the + compound message. They work well on THIS FILE. + MPair_parts is left as SAFE because it speeds up proofs. + The Crypt rule is normally kept UNSAFE to avoid breaking up certificates.*) + +Goal "H <= parts(H)"; +by (Blast_tac 1); +qed "parts_increasing"; + +val parts_insertI = impOfSubs (subset_insertI RS parts_mono); + +Goal "parts{} = {}"; +by Safe_tac; +by (etac parts.induct 1); +by (ALLGOALS Blast_tac); +qed "parts_empty"; +Addsimps [parts_empty]; + +Goal "X: parts{} ==> P"; +by (Asm_full_simp_tac 1); +qed "parts_emptyE"; +AddSEs [parts_emptyE]; + +(*WARNING: loops if H = {Y}, therefore must not be repeated!*) +Goal "X: parts H ==> EX Y:H. X: parts {Y}"; +by (etac parts.induct 1); +by (ALLGOALS Blast_tac); +qed "parts_singleton"; + + +(** Unions **) + +Goal "parts(G) Un parts(H) <= parts(G Un H)"; +by (REPEAT (ares_tac [Un_least, parts_mono, Un_upper1, Un_upper2] 1)); +val parts_Un_subset1 = result(); + +Goal "parts(G Un H) <= parts(G) Un parts(H)"; +by (rtac subsetI 1); +by (etac parts.induct 1); +by (ALLGOALS Blast_tac); +val parts_Un_subset2 = result(); + +Goal "parts(G Un H) = parts(G) Un parts(H)"; +by (REPEAT (ares_tac [equalityI, parts_Un_subset1, parts_Un_subset2] 1)); +qed "parts_Un"; + +Goal "parts (insert X H) = parts {X} Un parts H"; +by (stac (read_instantiate [("A","H")] insert_is_Un) 1); +by (simp_tac (HOL_ss addsimps [parts_Un]) 1); +qed "parts_insert"; + +(*TWO inserts to avoid looping. This rewrite is better than nothing. + Not suitable for Addsimps: its behaviour can be strange.*) +Goal "parts (insert X (insert Y H)) = parts {X} Un parts {Y} Un parts H"; +by (simp_tac (simpset() addsimps [Un_assoc]) 1); +by (simp_tac (simpset() addsimps [parts_insert RS sym]) 1); +qed "parts_insert2"; + +Goal "(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(); + +Goal "parts(UN x:A. H x) <= (UN x:A. parts(H x))"; +by (rtac subsetI 1); +by (etac parts.induct 1); +by (ALLGOALS Blast_tac); +val parts_UN_subset2 = result(); + +Goal "parts(UN x:A. H x) = (UN x:A. parts(H x))"; +by (REPEAT (ares_tac [equalityI, parts_UN_subset1, parts_UN_subset2] 1)); +qed "parts_UN"; + +(*Added to simplify arguments to parts, analz and synth. + NOTE: the UN versions are no longer used!*) +Addsimps [parts_Un, parts_UN]; +AddSEs [parts_Un RS equalityD1 RS subsetD RS UnE, + parts_UN RS equalityD1 RS subsetD RS UN_E]; + +Goal "insert X (parts H) <= parts(insert X H)"; +by (blast_tac (claset() addIs [impOfSubs parts_mono]) 1); +qed "parts_insert_subset"; + +(** Idempotence and transitivity **) + +Goal "X: parts (parts H) ==> X: parts H"; +by (etac parts.induct 1); +by (ALLGOALS Blast_tac); +qed "parts_partsD"; +AddSDs [parts_partsD]; + +Goal "parts (parts H) = parts H"; +by (Blast_tac 1); +qed "parts_idem"; +Addsimps [parts_idem]; + +Goal "[| X: parts G; G <= parts H |] ==> X: parts H"; +by (dtac parts_mono 1); +by (Blast_tac 1); +qed "parts_trans"; + +(*Cut*) +Goal "[| Y: parts (insert X G); X: parts H |] \ +\ ==> Y: parts (G Un H)"; +by (etac parts_trans 1); +by Auto_tac; +qed "parts_cut"; + +Goal "X: parts H ==> parts (insert X H) = parts H"; +by (fast_tac (claset() addSDs [parts_cut] + addIs [parts_insertI] + addss (simpset())) 1); +qed "parts_cut_eq"; + +Addsimps [parts_cut_eq]; + + +(** Rewrite rules for pulling out atomic messages **) + +fun parts_tac i = + EVERY [rtac ([subsetI, parts_insert_subset] MRS equalityI) i, + etac parts.induct i, + Auto_tac]; + +Goal "parts (insert (Agent agt) H) = insert (Agent agt) (parts H)"; +by (parts_tac 1); +qed "parts_insert_Agent"; + +Goal "parts (insert (Nonce N) H) = insert (Nonce N) (parts H)"; +by (parts_tac 1); +qed "parts_insert_Nonce"; + +Goal "parts (insert (Number N) H) = insert (Number N) (parts H)"; +by (parts_tac 1); +qed "parts_insert_Number"; + +Goal "parts (insert (Key K) H) = insert (Key K) (parts H)"; +by (parts_tac 1); +qed "parts_insert_Key"; + +Goal "parts (insert (Hash X) H) = insert (Hash X) (parts H)"; +by (parts_tac 1); +qed "parts_insert_Hash"; + +Goal "parts (insert (Crypt K X) H) = \ +\ insert (Crypt K X) (parts (insert X H))"; +by (rtac equalityI 1); +by (rtac subsetI 1); +by (etac parts.induct 1); +by Auto_tac; +by (etac parts.induct 1); +by (ALLGOALS (blast_tac (claset() addIs [parts.Body]))); +qed "parts_insert_Crypt"; + +Goal "parts (insert {|X,Y|} H) = \ +\ insert {|X,Y|} (parts (insert X (insert Y H)))"; +by (rtac equalityI 1); +by (rtac subsetI 1); +by (etac parts.induct 1); +by Auto_tac; +by (etac parts.induct 1); +by (ALLGOALS (blast_tac (claset() addIs [parts.Fst, parts.Snd]))); +qed "parts_insert_MPair"; + +Addsimps [parts_insert_Agent, parts_insert_Nonce, + parts_insert_Number, parts_insert_Key, + parts_insert_Hash, parts_insert_Crypt, parts_insert_MPair]; + + +Goal "parts (Key`N) = Key`N"; +by Auto_tac; +by (etac parts.induct 1); +by Auto_tac; +qed "parts_image_Key"; +Addsimps [parts_image_Key]; + + +(*In any message, there is an upper bound N on its greatest nonce.*) +Goal "EX N. ALL n. N<=n --> Nonce n ~: parts {msg}"; +by (induct_tac "msg" 1); +by (ALLGOALS (asm_simp_tac (simpset() addsimps [exI, parts_insert2]))); +(*MPair case: blast_tac works out the necessary sum itself!*) +by (blast_tac (claset() addSEs [add_leE]) 2); +(*Nonce case*) +by (res_inst_tac [("x","N + Suc nat")] exI 1); +by (auto_tac (claset() addSEs [add_leE], simpset())); +qed "msg_Nonce_supply"; + + +(**** Inductive relation "analz" ****) + +val major::prems = +Goal "[| {|X,Y|} : analz H; \ +\ [| X : analz H; Y : analz H |] ==> P \ +\ |] ==> P"; +by (cut_facts_tac [major] 1); +by (resolve_tac prems 1); +by (REPEAT (eresolve_tac [asm_rl, analz.Fst, analz.Snd] 1)); +qed "MPair_analz"; + +AddSEs [MPair_analz]; (*Making it safe speeds up proofs*) + +Goal "H <= analz(H)"; +by (Blast_tac 1); +qed "analz_increasing"; + +Goal "analz H <= parts H"; +by (rtac subsetI 1); +by (etac analz.induct 1); +by (ALLGOALS Blast_tac); +qed "analz_subset_parts"; + +bind_thm ("not_parts_not_analz", analz_subset_parts RS contra_subsetD); + + +Goal "parts (analz H) = parts H"; +by (rtac equalityI 1); +by (rtac (analz_subset_parts RS parts_mono RS subset_trans) 1); +by (Simp_tac 1); +by (blast_tac (claset() addIs [analz_increasing RS parts_mono RS subsetD]) 1); +qed "parts_analz"; +Addsimps [parts_analz]; + +Goal "analz (parts H) = parts H"; +by Auto_tac; +by (etac analz.induct 1); +by Auto_tac; +qed "analz_parts"; +Addsimps [analz_parts]; + +bind_thm ("analz_insertI", impOfSubs (subset_insertI RS analz_mono)); + +(** General equational properties **) + +Goal "analz{} = {}"; +by Safe_tac; +by (etac analz.induct 1); +by (ALLGOALS Blast_tac); +qed "analz_empty"; +Addsimps [analz_empty]; + +(*Converse fails: we can analz more from the union than from the + separate parts, as a key in one might decrypt a message in the other*) +Goal "analz(G) Un analz(H) <= analz(G Un H)"; +by (REPEAT (ares_tac [Un_least, analz_mono, Un_upper1, Un_upper2] 1)); +qed "analz_Un"; + +Goal "insert X (analz H) <= analz(insert X H)"; +by (blast_tac (claset() addIs [impOfSubs analz_mono]) 1); +qed "analz_insert"; + +(** Rewrite rules for pulling out atomic messages **) + +fun analz_tac i = + EVERY [rtac ([subsetI, analz_insert] MRS equalityI) i, + etac analz.induct i, + Auto_tac]; + +Goal "analz (insert (Agent agt) H) = insert (Agent agt) (analz H)"; +by (analz_tac 1); +qed "analz_insert_Agent"; + +Goal "analz (insert (Nonce N) H) = insert (Nonce N) (analz H)"; +by (analz_tac 1); +qed "analz_insert_Nonce"; + +Goal "analz (insert (Number N) H) = insert (Number N) (analz H)"; +by (analz_tac 1); +qed "analz_insert_Number"; + +Goal "analz (insert (Hash X) H) = insert (Hash X) (analz H)"; +by (analz_tac 1); +qed "analz_insert_Hash"; + +(*Can only pull out Keys if they are not needed to decrypt the rest*) +Goalw [keysFor_def] + "K ~: keysFor (analz H) ==> \ +\ analz (insert (Key K) H) = insert (Key K) (analz H)"; +by (analz_tac 1); +qed "analz_insert_Key"; + +Goal "analz (insert {|X,Y|} H) = \ +\ insert {|X,Y|} (analz (insert X (insert Y H)))"; +by (rtac equalityI 1); +by (rtac subsetI 1); +by (etac analz.induct 1); +by Auto_tac; +by (etac analz.induct 1); +by (ALLGOALS (blast_tac (claset() addIs [analz.Fst, analz.Snd]))); +qed "analz_insert_MPair"; + +(*Can pull out enCrypted message if the Key is not known*) +Goal "Key (invKey K) ~: analz H ==> \ +\ analz (insert (Crypt K X) H) = \ +\ insert (Crypt K X) (analz H)"; +by (analz_tac 1); +qed "analz_insert_Crypt"; + +Goal "Key (invKey K) : analz H ==> \ +\ analz (insert (Crypt K X) H) <= \ +\ insert (Crypt K X) (analz (insert X H))"; +by (rtac subsetI 1); +by (eres_inst_tac [("xa","x")] analz.induct 1); +by Auto_tac; +val lemma1 = result(); + +Goal "Key (invKey K) : analz H ==> \ +\ insert (Crypt K X) (analz (insert X H)) <= \ +\ analz (insert (Crypt K X) H)"; +by Auto_tac; +by (eres_inst_tac [("xa","x")] analz.induct 1); +by Auto_tac; +by (blast_tac (claset() addIs [analz_insertI, analz.Decrypt]) 1); +val lemma2 = result(); + +Goal "Key (invKey K) : analz H ==> \ +\ analz (insert (Crypt K X) H) = \ +\ insert (Crypt K X) (analz (insert X H))"; +by (REPEAT (ares_tac [equalityI, lemma1, lemma2] 1)); +qed "analz_insert_Decrypt"; + +(*Case analysis: either the message is secure, or it is not! + Effective, but can cause subgoals to blow up! + Use with split_if; apparently split_tac does not cope with patterns + such as "analz (insert (Crypt K X) H)" *) +Goal "analz (insert (Crypt K X) H) = \ +\ (if (Key (invKey K) : analz H) \ +\ then insert (Crypt K X) (analz (insert X H)) \ +\ else insert (Crypt K X) (analz H))"; +by (case_tac "Key (invKey K) : analz H " 1); +by (ALLGOALS (asm_simp_tac (simpset() addsimps [analz_insert_Crypt, + analz_insert_Decrypt]))); +qed "analz_Crypt_if"; + +Addsimps [analz_insert_Agent, analz_insert_Nonce, + analz_insert_Number, analz_insert_Key, + analz_insert_Hash, analz_insert_MPair, analz_Crypt_if]; + +(*This rule supposes "for the sake of argument" that we have the key.*) +Goal "analz (insert (Crypt K X) H) <= \ +\ insert (Crypt K X) (analz (insert X H))"; +by (rtac subsetI 1); +by (etac analz.induct 1); +by Auto_tac; +qed "analz_insert_Crypt_subset"; + + +Goal "analz (Key`N) = Key`N"; +by Auto_tac; +by (etac analz.induct 1); +by Auto_tac; +qed "analz_image_Key"; + +Addsimps [analz_image_Key]; + + +(** Idempotence and transitivity **) + +Goal "X: analz (analz H) ==> X: analz H"; +by (etac analz.induct 1); +by (ALLGOALS Blast_tac); +qed "analz_analzD"; +AddSDs [analz_analzD]; + +Goal "analz (analz H) = analz H"; +by (Blast_tac 1); +qed "analz_idem"; +Addsimps [analz_idem]; + +Goal "[| X: analz G; G <= analz H |] ==> X: analz H"; +by (dtac analz_mono 1); +by (Blast_tac 1); +qed "analz_trans"; + +(*Cut; Lemma 2 of Lowe*) +Goal "[| Y: analz (insert X H); X: analz H |] ==> Y: analz H"; +by (etac analz_trans 1); +by (Blast_tac 1); +qed "analz_cut"; + +(*Cut can be proved easily by induction on + "Y: analz (insert X H) ==> X: analz H --> Y: analz H" +*) + +(*This rewrite rule helps in the simplification of messages that involve + the forwarding of unknown components (X). Without it, removing occurrences + of X can be very complicated. *) +Goal "X: analz H ==> analz (insert X H) = analz H"; +by (blast_tac (claset() addIs [analz_cut, analz_insertI]) 1); +qed "analz_insert_eq"; + + +(** A congruence rule for "analz" **) + +Goal "[| analz G <= analz G'; analz H <= analz H' \ +\ |] ==> analz (G Un H) <= analz (G' Un H')"; +by (Clarify_tac 1); +by (etac analz.induct 1); +by (ALLGOALS (best_tac (claset() addIs [analz_mono RS subsetD]))); +qed "analz_subset_cong"; + +Goal "[| analz G = analz G'; analz H = analz H' \ +\ |] ==> analz (G Un H) = analz (G' Un H')"; +by (REPEAT_FIRST (ares_tac [equalityI, analz_subset_cong] + ORELSE' etac equalityE)); +qed "analz_cong"; + + +Goal "analz H = analz H' ==> analz(insert X H) = analz(insert X H')"; +by (asm_simp_tac (simpset() addsimps [insert_def] delsimps [singleton_conv] + setloop (rtac analz_cong)) 1); +qed "analz_insert_cong"; + +(*If there are no pairs or encryptions then analz does nothing*) +Goal "[| ALL X Y. {|X,Y|} ~: H; ALL X K. Crypt K X ~: H |] ==> \ +\ analz H = H"; +by Safe_tac; +by (etac analz.induct 1); +by (ALLGOALS Blast_tac); +qed "analz_trivial"; + +(*These two are obsolete (with a single Spy) but cost little to prove...*) +Goal "X: analz (UN i:A. analz (H i)) ==> X: analz (UN i:A. H i)"; +by (etac analz.induct 1); +by (ALLGOALS (blast_tac (claset() addIs [impOfSubs analz_mono]))); +val lemma = result(); + +Goal "analz (UN i:A. analz (H i)) = analz (UN i:A. H i)"; +by (blast_tac (claset() addIs [lemma, impOfSubs analz_mono]) 1); +qed "analz_UN_analz"; +Addsimps [analz_UN_analz]; + + +(**** Inductive relation "synth" ****) + +Goal "H <= synth(H)"; +by (Blast_tac 1); +qed "synth_increasing"; + +(** Unions **) + +(*Converse fails: we can synth more from the union than from the + separate parts, building a compound message using elements of each.*) +Goal "synth(G) Un synth(H) <= synth(G Un H)"; +by (REPEAT (ares_tac [Un_least, synth_mono, Un_upper1, Un_upper2] 1)); +qed "synth_Un"; + +Goal "insert X (synth H) <= synth(insert X H)"; +by (blast_tac (claset() addIs [impOfSubs synth_mono]) 1); +qed "synth_insert"; + +(** Idempotence and transitivity **) + +Goal "X: synth (synth H) ==> X: synth H"; +by (etac synth.induct 1); +by (ALLGOALS Blast_tac); +qed "synth_synthD"; +AddSDs [synth_synthD]; + +Goal "synth (synth H) = synth H"; +by (Blast_tac 1); +qed "synth_idem"; + +Goal "[| X: synth G; G <= synth H |] ==> X: synth H"; +by (dtac synth_mono 1); +by (Blast_tac 1); +qed "synth_trans"; + +(*Cut; Lemma 2 of Lowe*) +Goal "[| Y: synth (insert X H); X: synth H |] ==> Y: synth H"; +by (etac synth_trans 1); +by (Blast_tac 1); +qed "synth_cut"; + +Goal "Agent A : synth H"; +by (Blast_tac 1); +qed "Agent_synth"; + +Goal "Number n : synth H"; +by (Blast_tac 1); +qed "Number_synth"; + +Goal "(Nonce N : synth H) = (Nonce N : H)"; +by (Blast_tac 1); +qed "Nonce_synth_eq"; + +Goal "(Key K : synth H) = (Key K : H)"; +by (Blast_tac 1); +qed "Key_synth_eq"; + +Goal "Key K ~: H ==> (Crypt K X : synth H) = (Crypt K X : H)"; +by (Blast_tac 1); +qed "Crypt_synth_eq"; + +Addsimps [Agent_synth, Number_synth, + Nonce_synth_eq, Key_synth_eq, Crypt_synth_eq]; + + +Goalw [keysFor_def] + "keysFor (synth H) = keysFor H Un invKey`{K. Key K : H}"; +by (Blast_tac 1); +qed "keysFor_synth"; +Addsimps [keysFor_synth]; + + +(*** Combinations of parts, analz and synth ***) + +Goal "parts (synth H) = parts H Un synth H"; +by (rtac equalityI 1); +by (rtac subsetI 1); +by (etac parts.induct 1); +by (ALLGOALS + (blast_tac (claset() addIs [synth_increasing RS parts_mono RS subsetD, + parts.Fst, parts.Snd, parts.Body]))); +qed "parts_synth"; +Addsimps [parts_synth]; + +Goal "analz (analz G Un H) = analz (G Un H)"; +by (REPEAT_FIRST (resolve_tac [equalityI, analz_subset_cong])); +by (ALLGOALS Simp_tac); +qed "analz_analz_Un"; + +Goal "analz (synth G Un H) = analz (G Un H) Un synth G"; +by (rtac equalityI 1); +by (rtac subsetI 1); +by (etac analz.induct 1); +by (blast_tac (claset() addIs [impOfSubs analz_mono]) 5); +by (ALLGOALS + (blast_tac (claset() addIs [analz.Fst, analz.Snd, analz.Decrypt]))); +qed "analz_synth_Un"; + +Goal "analz (synth H) = analz H Un synth H"; +by (cut_inst_tac [("H","{}")] analz_synth_Un 1); +by (Full_simp_tac 1); +qed "analz_synth"; +Addsimps [analz_analz_Un, analz_synth_Un, analz_synth]; + + +(** For reasoning about the Fake rule in traces **) + +Goal "X: G ==> parts(insert X H) <= parts G Un parts H"; +by (rtac ([parts_mono, parts_Un_subset2] MRS subset_trans) 1); +by (Blast_tac 1); +qed "parts_insert_subset_Un"; + +(*More specifically for Fake. Very occasionally we could do with a version + of the form parts{X} <= synth (analz H) Un parts H *) +Goal "X: synth (analz H) ==> \ +\ parts (insert X H) <= synth (analz H) Un parts H"; +by (dtac parts_insert_subset_Un 1); +by (Full_simp_tac 1); +by (Blast_tac 1); +qed "Fake_parts_insert"; + +(*H is sometimes (Key ` KK Un spies evs), so can't put G=H*) +Goal "X: synth (analz G) ==> \ +\ analz (insert X H) <= synth (analz G) Un analz (G Un H)"; +by (rtac subsetI 1); +by (subgoal_tac "x : analz (synth (analz G) Un H)" 1); +by (blast_tac (claset() addIs [impOfSubs analz_mono, + impOfSubs (analz_mono RS synth_mono)]) 2); +by (Full_simp_tac 1); +by (Blast_tac 1); +qed "Fake_analz_insert"; + +Goal "(X: analz H & X: parts H) = (X: analz H)"; +by (blast_tac (claset() addIs [impOfSubs analz_subset_parts]) 1); +val analz_conj_parts = result(); + +Goal "(X: analz H | X: parts H) = (X: parts H)"; +by (blast_tac (claset() addIs [impOfSubs analz_subset_parts]) 1); +val analz_disj_parts = result(); + +AddIffs [analz_conj_parts, analz_disj_parts]; + +(*Without this equation, other rules for synth and analz would yield + redundant cases*) +Goal "({|X,Y|} : synth (analz H)) = \ +\ (X : synth (analz H) & Y : synth (analz H))"; +by (Blast_tac 1); +qed "MPair_synth_analz"; + +AddIffs [MPair_synth_analz]; + +Goal "[| Key K : analz H; Key (invKey K) : analz H |] \ +\ ==> (Crypt K X : synth (analz H)) = (X : synth (analz H))"; +by (Blast_tac 1); +qed "Crypt_synth_analz"; + + +Goal "X ~: synth (analz H) \ +\ ==> (Hash{|X,Y|} : synth (analz H)) = (Hash{|X,Y|} : analz H)"; +by (Blast_tac 1); +qed "Hash_synth_analz"; +Addsimps [Hash_synth_analz]; + + +(**** HPair: a combination of Hash and MPair ****) + +(*** Freeness ***) + +Goalw [HPair_def] "Agent A ~= Hash[X] Y"; +by (Simp_tac 1); +qed "Agent_neq_HPair"; + +Goalw [HPair_def] "Nonce N ~= Hash[X] Y"; +by (Simp_tac 1); +qed "Nonce_neq_HPair"; + +Goalw [HPair_def] "Number N ~= Hash[X] Y"; +by (Simp_tac 1); +qed "Number_neq_HPair"; + +Goalw [HPair_def] "Key K ~= Hash[X] Y"; +by (Simp_tac 1); +qed "Key_neq_HPair"; + +Goalw [HPair_def] "Hash Z ~= Hash[X] Y"; +by (Simp_tac 1); +qed "Hash_neq_HPair"; + +Goalw [HPair_def] "Crypt K X' ~= Hash[X] Y"; +by (Simp_tac 1); +qed "Crypt_neq_HPair"; + +val HPair_neqs = [Agent_neq_HPair, Nonce_neq_HPair, Number_neq_HPair, + Key_neq_HPair, Hash_neq_HPair, Crypt_neq_HPair]; + +AddIffs HPair_neqs; +AddIffs (HPair_neqs RL [not_sym]); + +Goalw [HPair_def] "(Hash[X'] Y' = Hash[X] Y) = (X' = X & Y'=Y)"; +by (Simp_tac 1); +qed "HPair_eq"; + +Goalw [HPair_def] "({|X',Y'|} = Hash[X] Y) = (X' = Hash{|X,Y|} & Y'=Y)"; +by (Simp_tac 1); +qed "MPair_eq_HPair"; + +Goalw [HPair_def] "(Hash[X] Y = {|X',Y'|}) = (X' = Hash{|X,Y|} & Y'=Y)"; +by Auto_tac; +qed "HPair_eq_MPair"; + +AddIffs [HPair_eq, MPair_eq_HPair, HPair_eq_MPair]; + + +(*** Specialized laws, proved in terms of those for Hash and MPair ***) + +Goalw [HPair_def] "keysFor (insert (Hash[X] Y) H) = keysFor H"; +by (Simp_tac 1); +qed "keysFor_insert_HPair"; + +Goalw [HPair_def] + "parts (insert (Hash[X] Y) H) = \ +\ insert (Hash[X] Y) (insert (Hash{|X,Y|}) (parts (insert Y H)))"; +by (Simp_tac 1); +qed "parts_insert_HPair"; + +Goalw [HPair_def] + "analz (insert (Hash[X] Y) H) = \ +\ insert (Hash[X] Y) (insert (Hash{|X,Y|}) (analz (insert Y H)))"; +by (Simp_tac 1); +qed "analz_insert_HPair"; + +Goalw [HPair_def] "X ~: synth (analz H) \ +\ ==> (Hash[X] Y : synth (analz H)) = \ +\ (Hash {|X, Y|} : analz H & Y : synth (analz H))"; +by (Simp_tac 1); +by (Blast_tac 1); +qed "HPair_synth_analz"; + +Addsimps [keysFor_insert_HPair, parts_insert_HPair, analz_insert_HPair, + HPair_synth_analz, HPair_synth_analz]; + + +(*We do NOT want Crypt... messages broken up in protocols!!*) +Delrules [make_elim parts.Body]; + + +(** Rewrites to push in Key and Crypt messages, so that other messages can + be pulled out using the analz_insert rules **) + +fun insComm x y = inst "x" x (inst "y" y insert_commute); + +val pushKeys = map (insComm "Key ?K") + ["Agent ?C", "Nonce ?N", "Number ?N", + "Hash ?X", "MPair ?X ?Y", "Crypt ?X ?K'"]; + +val pushCrypts = map (insComm "Crypt ?X ?K") + ["Agent ?C", "Nonce ?N", "Number ?N", + "Hash ?X'", "MPair ?X' ?Y"]; + +(*Cannot be added with Addsimps -- we don't always want to re-order messages*) +bind_thms ("pushes", pushKeys@pushCrypts); + + +(*** Tactics useful for many protocol proofs ***) + +(*Prove base case (subgoal i) and simplify others. A typical base case + concerns Crypt K X ~: Key`shrK`bad and cannot be proved by rewriting + alone.*) +fun prove_simple_subgoals_tac i = + force_tac (claset(), simpset() addsimps [image_eq_UN]) i THEN + ALLGOALS Asm_simp_tac; + +fun Fake_parts_insert_tac i = + blast_tac (claset() addIs [parts_insertI] + addDs [impOfSubs analz_subset_parts, + impOfSubs Fake_parts_insert]) i; + +(*Apply rules to break down assumptions of the form + Y : parts(insert X H) and Y : analz(insert X H) +*) +val Fake_insert_tac = + dresolve_tac [impOfSubs Fake_analz_insert, + impOfSubs Fake_parts_insert] THEN' + eresolve_tac [asm_rl, synth.Inj]; + +fun Fake_insert_simp_tac i = + REPEAT (Fake_insert_tac i) THEN Asm_full_simp_tac i; + + +(*Analysis of Fake cases. Also works for messages that forward unknown parts, + but this application is no longer necessary if analz_insert_eq is used. + Abstraction over i is ESSENTIAL: it delays the dereferencing of claset + DEPENDS UPON "X" REFERRING TO THE FRADULENT MESSAGE *) + +val atomic_spy_analz_tac = SELECT_GOAL + (Fake_insert_simp_tac 1 + THEN + IF_UNSOLVED (Blast.depth_tac + (claset() addIs [analz_insertI, + impOfSubs analz_subset_parts]) 4 1)); + +fun spy_analz_tac i = + DETERM + (SELECT_GOAL + (EVERY + [ (*push in occurrences of X...*) + (REPEAT o CHANGED) + (res_inst_tac [("x1","X")] (insert_commute RS ssubst) 1), + (*...allowing further simplifications*) + Simp_tac 1, + REPEAT (FIRSTGOAL (resolve_tac [allI,impI,notI,conjI,iffI])), + DEPTH_SOLVE (atomic_spy_analz_tac 1)]) i); + +(*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];