Theory Network_Assumptions
section‹Network Assumptions used for authorized segments.›
theory Network_Assumptions
imports
"Network_Model"
begin
locale network_assums_generic = network_model _ auth_seg0 for
auth_seg0 :: "('ainfo × 'aahi ahi_scheme list) set" +
assumes
ASM_if_valid: "(info, l) ∈ auth_seg0 ⟹ ifs_valid_None l" and
ASM_empty [simp, intro!]: "(info, []) ∈ auth_seg0" and
ASM_rooted: "(info, l) ∈ auth_seg0 ⟹ rooted l" and
ASM_terminated: "(info, l) ∈ auth_seg0 ⟹ terminated l"
locale network_assums_undirect = network_assums_generic _ _ +
assumes
ASM_adversary: "⟦⋀hf. hf ∈ set hfs ⟹ ASID hf ∈ bad⟧ ⟹ (info, hfs) ∈ auth_seg0"
locale network_assums_direct = network_assums_generic _ _ +
assumes
ASM_singleton: "⟦ASID hf ∈ bad⟧ ⟹ (info, [hf]) ∈ auth_seg0" and
ASM_extension: "⟦(info, hf2#ys) ∈ auth_seg0; ASID hf2 ∈ bad; ASID hf1 ∈ bad⟧
⟹ (info, hf1#hf2#ys) ∈ auth_seg0" and
ASM_modify: "⟦(info, hf#ys) ∈ auth_seg0; ASID hf = a; ASID hf' = a; UpIF hf' = UpIF hf; a ∈ bad⟧
⟹ (info, hf'#ys) ∈ auth_seg0" and
ASM_cutoff: "⟦(info, zs@hf#ys) ∈ auth_seg0; ASID hf = a; a ∈ bad⟧ ⟹ (info, hf#ys) ∈ auth_seg0"
begin
lemma auth_seg0_non_empty [simp, intro!]: "auth_seg0 ≠ {}"
by auto
lemma auth_seg0_non_empty_frag [simp, intro!]: "∃ info . pfragment info [] auth_seg0"
apply(auto simp add: pfragment_def)
by (metis append_Nil2 ASM_empty)
text ‹This lemma applies the extendability assumptions on @{text "auth_seg0"} to pfragments of
@{text "auth_seg0"}.›
lemma extend_pfragment0:
assumes "pfragment ainfo (hf2#xs) auth_seg0"
assumes "ASID hf1 ∈ bad"
assumes "ASID hf2 ∈ bad"
shows "pfragment ainfo (hf1#hf2#xs) auth_seg0"
using assms
by(auto intro!: pfragmentI[of _ "[]" _ _] elim!: pfragmentE intro: ASM_cutoff intro!: ASM_extension)
text‹This lemma shows that the above assumptions imply that of the undirected setting›
lemma "⟦⋀hf. hf ∈ set hfs ⟹ ASID hf ∈ bad⟧ ⟹ (info, hfs) ∈ auth_seg0"
apply(induction hfs)
using ASM_empty apply blast
subgoal for a hfs
apply(cases hfs)
by(auto intro!: ASM_singleton ASM_extension)
done
end
end