theory Spi_Mgrs imports Spi_Bitrace begin consts (* set of most general respectful substitutions refining f, for atomic keys - see ex_mgrs_resp *) mgrs_rtc :: "'n msg io list => ('n => 'n msg) => ('n => 'n msg) set" mgrs1 :: "'n msg io list => ('n => 'n msg) => ('n => 'n msg) set" mgrs1cp :: "'n msg io list => (('n => 'n msg) * ('n => 'n msg)) set" mgrs_final :: "'n msg io list => ('n => 'n msg) => ('n => 'n msg) set" mgrs_resp :: "'n msg io list => ('n => 'n msg) => ('n => 'n msg) set" (* in Spi_Theory.thy fsatcm :: "('a => 'b set set) => ('a => 'c set) => 'a set => ('a => ('b * 'c) set) => bool" sat_unifs :: "('a => 'b set set) => ('a => 'c set) => 'a set => ('b * 'c) set set" *) types ('a,'n) Fg = "(('n => 'n msg) => 'a => 'n msg set set)" ('a,'n) Gg = "(('n => 'n msg) => 'a => 'n msg set)" consts gmgrs1 :: "('a,'n) Fg => ('a,'n) Gg => 'a set => ('n => 'n msg) => ('n => 'n msg) set" gmgrs1cp :: "('a,'n) Fg => ('a,'n) Gg => 'a set => (('n => 'n msg) * ('n => 'n msg)) set" gmgrs_rtc :: "('a => 'b set set) => ('a => 'c set) => 'a set => ('n => 'n msg) => ('n => 'n msg) set" gmgrs_final :: "('a => 'b set set) => ('a => 'c set) => 'a set => ('n => 'n msg) => ('n => 'n msg) set" gmgrs_resp :: "('a => 'b set set) => ('a => 'c set) => 'a set => ('n => 'n msg) => ('n => 'n msg) set" consts kaF :: "('a1 * 'n msg, 'n) Fg" kaG :: "('n msg set * 'a2, 'n) Gg" primrec defn : "kaF g (ss, n) = idv_ss_sets (subst_msg g n)" primrec defn : "kaG g (ss, n) = subst_msg g ` (reduce_ss ss - range Name)" defs (* set of further substitutions after g, to try to make it respectful *) gmgrs1_def : "gmgrs1 F G smcs g == Some -` mgu ` (sat_unifs (F g) (G g) smcs)" (* effective single step, ie, h does more than g *) inductive "gmgrs1cp F G smcs" intros I : "k : gmgrs1 F G smcs g ==> domain k ~= {} ==> h = comp_subst k g ==> (h, g) : gmgrs1cp F G smcs" (* similar for general keys, see ex_umgrs_resp *) consts umgrs1 :: "'n msg io list => ('n => 'n msg) => ('n => 'n msg) set" umgrs1cp :: "'n msg io list => (('n => 'n msg) * ('n => 'n msg)) set" umgrs_final :: "'n msg io list => ('n => 'n msg) => ('n => 'n msg) set" umgrs_resp :: "'n msg io list => ('n => 'n msg) => ('n => 'n msg) set" defs (* use set of further substitutions after g, to try to make it respectful *) umgrs1_def : "umgrs1 st g == Some -` mgu ` unif_ch_st g st" inductive "umgrs1cp st" intros I : "k : umgrs1 st g ==> domain k ~= {} ==> h = comp_subst k g ==> (h, g) : umgrs1cp st" defs umgrs_final_def : "umgrs_final st g == {h. (h, g) : (umgrs1cp st)^* & (ALL f. (f, h) ~: umgrs1cp st)}" umgrs_resp_def : "umgrs_resp st g == {h. (h, g) : (umgrs1cp st)^* & (EX k: umgrs1 st h. domain k = {})}" (* property that f selects a solution to each constraint, which is a necessary condition for a respectful substitution, by ext_constrs_idv_ss_match *) consts fsatc :: "('n msg set * 'n msg) set => ('n => 'n msg) => ('n msg set * 'n msg => ('n msg * 'n msg) set) => bool" defs fsatc_def : "fsatc smcs g f == ALL (ss, n) : smcs. f (ss, n) : match_sets (idv_ss_sets (subst_msg g n)) (subst_msg g ` (reduce_ss ss - range Name))" defs (* set of further substitutions after g, to try to make it respectful *) mgrs1_def : "mgrs1 st g == let \ \ unifs = sat_unifs (%(ss,n). idv_ss_sets (subst_msg g n)) \ \ (%(ss,n). (subst_msg g ` (reduce_ss ss - range Name))) (sm_constrs st) ; \ \ mgus = Some -` mgu ` unifs in mgus" (* effective single step, ie, h does more than g *) inductive "mgrs1cp st" intros I : "k : mgrs1 st g ==> domain k ~= {} ==> h = comp_subst k g ==> (h, g) : mgrs1cp st" (* result of taking any number of mgrs1 steps, thus "((h, g) : (mgrs1cp st)^* ) = (h : mgrs_rtc st g)" *) inductive "mgrs_rtc st f" intros refl : "f : mgrs_rtc st f" I : "g : mgrs_rtc st f ==> (h, g) : mgrs1cp st ==> h : mgrs_rtc st f" defs (* the set of mgrs1cp-minimal substitutions got from g *) mgrs_final_def : "mgrs_final st g == {h : mgrs_rtc st g. ALL f. (f, h) ~: mgrs1cp st}" mgrs_resp_def : "mgrs_resp st g == {h : mgrs_rtc st g. EX k: mgrs1 st h. domain k = {}}" (* recdef "mgrs" "inv_image {(S, S'). S < S'} (% (xs, f). UN x:xs. fn_msg x)" "mgrs ms = (if f : sm_resp ms then {f} else *) axioms (* to be proved *) fn_sm_constrs : "(S, M) : sm_constrs st ==> (UN s : S. fn_msg s) Un fn_msg M <= (UN s : rem_io ` set st. fn_msg s)" consts (* as defined in dbc paper *) Phi :: "'n msg io list => 'n msg => ('n => 'n msg) set" Theta :: "'n msg io list => 'n msg => ('n => 'n msg) set" inductive "Phi st M" intros I : "u : unif_ch1_ss Name (rem_io ` set st) M ==> mgu u = Some g ==> f : umgrs_resp st g ==> f : Phi st M" inductive "Theta st M" intros I : "st : sm_resp th ==> ((subst_msg th ` rem_io ` set st, subst_msg th M) : derrec smpsc {}) ==> th : Theta st M" consts red_mgrs :: "'n msg set => 'n msg set * (('n msg set * 'n msg) set) => 'n msg io list => ('n => 'n msg) set" primrec red_mgrs_def : "red_mgrs G (H, Vs) st = UNION (Some -` mgu ` red_unifs_ss Vs) (umgrs_resp st)" end