# HG changeset patch # User paulson # Date 1252314257 -3600 # Node ID 1beb4275eb6456e5988161302795b445649b2f02 # Parent bfe7573a239b89da6c9f31a11206f40efc2ccf6f# Parent d703a76acc08accba383756f41dbbdabcd71e096 conflict resolution possibly diff -r bfe7573a239b -r 1beb4275eb64 src/HOL/Auth/NS_Shared.thy --- a/src/HOL/Auth/NS_Shared.thy Fri Sep 04 10:58:50 2009 +0200 +++ b/src/HOL/Auth/NS_Shared.thy Mon Sep 07 10:04:17 2009 +0100 @@ -318,9 +318,7 @@ @{term "Crypt K (Nonce NB) \ parts (spies evs2)"} *} apply (force dest!: Crypt_imp_keysFor) txt{*NS4*} -apply (blast dest: B_trusts_NS3 - Says_imp_knows_Spy [THEN analz.Inj] - Crypt_Spy_analz_bad unique_session_keys) +apply (metis B_trusts_NS3 Crypt_Spy_analz_bad Says_imp_analz_Spy Says_imp_parts_knows_Spy analz.Fst unique_session_keys) done text{*This version no longer assumes that K is secure*} @@ -349,9 +347,7 @@ txt{*NS2*} apply (blast dest!: new_keys_not_used Crypt_imp_keysFor) txt{*NS4*} -apply (blast dest: B_trusts_NS3 - dest: Says_imp_knows_Spy [THEN analz.Inj] - unique_session_keys Crypt_Spy_analz_bad) +apply (metis B_trusts_NS3 Crypt_Spy_analz_bad Says_imp_analz_Spy Says_imp_parts_knows_Spy analz.Fst unique_session_keys) done @@ -475,18 +471,15 @@ apply (erule rev_mp) apply (erule rev_mp) apply (erule ns_shared.induct, analz_mono_contra) -apply (frule_tac [5] Says_S_message_form) apply (simp_all) txt{*Fake*} apply blast txt{*NS2*} apply (force dest!: Crypt_imp_keysFor) -txt{*NS3, much quicker having installed @{term Says_S_message_form} before simplication*} -apply fastsimp +txt{*NS3*} +apply (metis NS3_msg_in_parts_spies parts_cut_eq) txt{*NS5, the most important case, can be solved by unicity*} -apply (case_tac "Aa \ bad") -apply (force dest!: Says_imp_spies [THEN analz.Inj, THEN analz.Decrypt, THEN analz.Snd, THEN analz.Snd, THEN analz.Fst]) -apply (blast dest: A_trusts_NS2 unique_session_keys) +apply (metis A_trusts_NS2 Crypt_Spy_analz_bad Says_imp_analz_Spy Says_imp_parts_knows_Spy analz.Fst analz.Snd unique_session_keys) done lemma A_Issues_B: diff -r bfe7573a239b -r 1beb4275eb64 src/HOL/Tools/metis_tools.ML diff -r bfe7573a239b -r 1beb4275eb64 src/HOL/Tools/res_hol_clause.ML --- a/src/HOL/Tools/res_hol_clause.ML Fri Sep 04 10:58:50 2009 +0200 +++ b/src/HOL/Tools/res_hol_clause.ML Mon Sep 07 10:04:17 2009 +0100 @@ -23,6 +23,7 @@ datatype literal = Literal of polarity * combterm datatype clause = Clause of {clause_id: clause_id, axiom_name: axiom_name, th: thm, kind: ResClause.kind,literals: literal list, ctypes_sorts: typ list} + val type_of_combterm: combterm -> ResClause.fol_type val strip_comb: combterm -> combterm * combterm list val literals_of_term: theory -> term -> literal list * typ list exception TOO_TRIVIAL