Theory Parametrized_Dataplane_3_undirected
section‹Parametrized dataplane protocol for undirected protocols›
text‹This is an instance of the @{text "Parametrized_Dataplane_2"} model, specifically for protocols
that authorize paths in an undirected fashion. We specialize the @{text "hf_valid_generic"} check
to a still parametrized, but more concrete @{text "hf_valid"} check. The rest of the parameters
remain abstract until a later instantiation with a concrete protocols (see the instances directory).
While both the models for undirected and directed protocols import assumptions from the theory
@{text "Network_Assumptions"}, they differ in strength: the assumptions made by undirected protocols
are strictly weaker, since the entire forwarding path is authorized by each AS, and not only the
future path from the perspective of each AS.
In addition, the specific conditions that instances have to verify differs between the undirected
and the directed setting (compare the locales @{text "dataplane_3_undirected"} and
@{text "dataplane_3_directed"}).
This explains the need to split up the verification of the attacker event into two theories. Despite
the differences that concrete protocols may exhibit, these two theories suffice to show the crux
of the refinement proof. The instances merely have to show a set of static conditions.
Note that we don't use the update function in the undirected setting, since none of the instances
require it.›
theory Parametrized_Dataplane_3_undirected
imports
"Parametrized_Dataplane_2" "Network_Assumptions"
begin
type_synonym UINFO = "msgterm"
subsection ‹Hop validation check, authorized segments, and path extraction.›
text‹First we define a locale that requires a number of functions. We will later extend this
to a locale @{text "dataplane_3_undirected"}, which makes assumptions on how these functions operate.
We separate the assumptions in order to make use of some auxiliary definitions defined in this locale.›
locale dataplane_3_undirected_defs = network_assums_undirect _ _ _ auth_seg0
for auth_seg0 :: "('ainfo × 'aahi ahi_scheme list) set" +
fixes hf_valid :: "'ainfo ⇒ UINFO
⇒ ('aahi, 'uhi) HF list
⇒ ('aahi, 'uhi) HF
⇒ bool"
and auth_restrict :: "'ainfo ⇒ UINFO ⇒ ('aahi, 'uhi) HF list ⇒ bool"
and extr :: "msgterm ⇒ 'aahi ahi_scheme list"
and extr_ainfo :: "msgterm ⇒ 'ainfo"
and term_ainfo :: "'ainfo ⇒ msgterm"
and terms_hf :: "('aahi, 'uhi) HF ⇒ msgterm set"
and terms_uinfo :: "UINFO ⇒ msgterm set"
and no_oracle :: "'ainfo ⇒ UINFO ⇒ bool"
begin
abbreviation upd_uinfo :: "UINFO ⇒ ('aahi, 'uhi) HF ⇒ UINFO" where
"upd_uinfo u hf ≡ u"
abbreviation hf_valid_generic :: "'ainfo ⇒ msgterm
⇒ ('aahi, 'uhi) HF list
⇒ ('aahi, 'uhi) HF option
⇒ ('aahi, 'uhi) HF
⇒ ('aahi, 'uhi) HF option ⇒ bool" where
"hf_valid_generic ainfo uinfo hfs pre hf nxt ≡ hf_valid ainfo uinfo hfs hf"
abbreviation hfs_valid_prefix where
"hfs_valid_prefix ainfo uinfo pas fut ≡ (takeWhile (λhf . hf_valid ainfo uinfo (rev(pas)@fut) hf) fut)"
definition hfs_valid_prefix_generic ::
"'ainfo ⇒ msgterm ⇒ ('aahi, 'uhi) HF list ⇒ ('aahi, 'uhi) HF option ⇒ ('aahi, 'uhi) HF list ⇒
('aahi, 'uhi) HF option ⇒ ('aahi, 'uhi) HF list"where
"hfs_valid_prefix_generic ainfo uinfo pas pre fut nxt ≡
hfs_valid_prefix ainfo uinfo pas fut"
declare hfs_valid_prefix_generic_def[simp]
sublocale dataplane_2_defs _ _ _ auth_seg0 hf_valid_generic hfs_valid_prefix_generic
auth_restrict extr extr_ainfo term_ainfo terms_hf terms_uinfo upd_uinfo
apply unfold_locales done
lemma auth_seg2_elem: "⟦(ainfo, hfs) ∈ auth_seg2 uinfo; hf ∈ set hfs⟧
⟹ ∃uinfo . hf_valid ainfo uinfo hfs hf ∧ auth_restrict ainfo uinfo hfs ∧ (ainfo, AHIS hfs) ∈ auth_seg0"
by (auto simp add: auth_seg2_def TW.holds_takeW_is_identity dest!: TW.holds_set_list)
end
print_locale dataplane_3_undirected_defs
locale dataplane_3_undirected_ik_defs = dataplane_3_undirected_defs _ _ _ _ hf_valid auth_restrict
extr extr_ainfo term_ainfo terms_hf _ for
hf_valid :: "'ainfo ⇒ UINFO ⇒ ('aahi, 'uhi) HF list ⇒ ('aahi, 'uhi) HF ⇒ bool"
and auth_restrict :: "'ainfo => UINFO ⇒ ('aahi, 'uhi) HF list ⇒ bool"
and extr :: "msgterm ⇒ 'aahi ahi_scheme list"
and extr_ainfo :: "msgterm ⇒ 'ainfo"
and term_ainfo :: "'ainfo ⇒ msgterm"
and terms_hf :: "('aahi, 'uhi) HF ⇒ msgterm set"
+
fixes ik_add :: "msgterm set"
and ik_oracle :: "msgterm set"
begin
lemma prefix_hfs_valid_prefix_generic:
"prefix (hfs_valid_prefix_generic ainfo uinfo pas pre fut nxt) fut"
apply(simp add: hfs_valid_prefix_generic_def)
by (metis prefixI takeWhile_dropWhile_id)
lemma cons_hfs_valid_prefix_generic:
"⟦hf_valid_generic ainfo uinfo hfs (head pas) hf1 (head fut); hfs = (rev pas)@hf1 #fut⟧
⟹ hfs_valid_prefix_generic ainfo uinfo pas (head pas) (hf1 # fut) None =
hf1 # (hfs_valid_prefix_generic ainfo uinfo (hf1#pas) (Some hf1) fut None)"
by(auto simp add: TW.takeW_split_tail)
print_locale dataplane_2_ik_defs
sublocale dataplane_2_ik_defs _ _ _ _ hfs_valid_prefix_generic auth_restrict extr extr_ainfo term_ainfo
terms_hf _ no_oracle hf_valid_generic upd_uinfo ik_add ik_oracle
by unfold_locales
end
subsection ‹Conditions of the parametrized model›
text‹We now list the assumptions of this parametrized model. ›
print_locale dataplane_3_undirected_ik_defs
locale dataplane_3_undirected = dataplane_3_undirected_ik_defs _ _ _ _ terms_uinfo no_oracle hf_valid auth_restrict extr
extr_ainfo term_ainfo terms_hf ik_add ik_oracle
for hf_valid :: "'ainfo ⇒ msgterm ⇒ ('aahi, 'uhi) HF list ⇒ ('aahi, 'uhi) HF ⇒ bool"
and auth_restrict :: "'ainfo => UINFO ⇒ ('aahi, 'uhi) HF list ⇒ bool"
and extr :: "msgterm ⇒ 'aahi ahi_scheme list"
and extr_ainfo :: "msgterm ⇒ 'ainfo"
and term_ainfo :: "'ainfo ⇒ msgterm"
and terms_uinfo :: "UINFO ⇒ msgterm set"
and ik_add :: "msgterm set"
and terms_hf :: "('aahi, 'uhi) HF ⇒ msgterm set"
and ik_oracle :: "msgterm set"
and no_oracle :: "'ainfo ⇒ UINFO ⇒ bool" +
assumes COND_terms_hf:
"⟦hf_valid ainfo uinfo l hf; terms_hf hf ⊆ analz ik; no_oracle ainfo uinfo; hf ∈ set l⟧
⟹ ∃hfs . hf ∈ set hfs ∧ (∃uinfo' . (ainfo, hfs) ∈ (auth_seg2 uinfo'))"
and COND_honest_hf_analz:
"⟦ASID (AHI hf) ∉ bad; hf_valid ainfo uinfo l hf; terms_hf hf ⊆ synth (analz ik);
no_oracle ainfo uinfo; hf ∈ set l⟧
⟹ terms_hf hf ⊆ analz ik"
and COND_extr:
"⟦hf_valid ainfo uinfo l hf⟧ ⟹ extr (HVF hf) = AHIS l"
and COND_hf_valid_uinfo:
"⟦hf_valid ainfo uinfo l hf; hf_valid ainfo' uinfo' l' hf⟧
⟹ uinfo' = uinfo"
begin
text‹This is the central lemma that we need to prove to show the refinement between this model and
dp1. It states: If an attacker can synthesize a segment from his knowledge, and does not use a path
origin that was used to query the oracle, then the valid prefix of the segment is authorized. Thus,
the attacker cannot create any valid but unauthorized segments.›
lemma ik_seg_is_auth:
assumes "terms_pkt m ⊆ synth (analz ik)" and
"future m = fut" and "AInfo m = ainfo" and "nxt = None" and "no_oracle ainfo uinfo"
shows "pfragment ainfo
(AHIS (hfs_valid_prefix ainfo uinfo pas fut))
auth_seg0"
proof-
let ?hfsvalid = "hfs_valid_prefix ainfo uinfo pas fut"
let ?AHIS = "AHIS ?hfsvalid"
show ?thesis
proof(cases "∃hfhonest ∈ set ?AHIS . ASID hfhonest ∉ bad")
case True
then obtain hfhonesta where hfhonesta_def: "hfhonesta ∈ set ?AHIS" "ASID hfhonesta ∉ bad" by auto
then obtain hfhonestc where hfhonestc_def:
"hfhonestc ∈ set ?hfsvalid" "hfhonesta = AHI hfhonestc" "ASID (AHI hfhonestc) ∉ bad"
by(auto dest: AHIS_set)
then have hfhonestc_valid: "hf_valid ainfo uinfo (rev(pas)@fut) hfhonestc" using hfhonesta_def
by (meson set_takeWhileD)
have hfhonestc_fut: "hfhonestc ∈ set fut" using hfhonestc_def(1) using set_takeWhileD by fastforce
from hfhonestc_valid hfhonestc_def have "terms_hf hfhonestc ⊆ analz ik"
apply(elim COND_honest_hf_analz[where l="(rev(pas)@fut)"])
using assms hfhonesta_def set_takeWhileD
apply(auto simp add: terms_pkt_def)
by force+
then obtain hfshonest uinfo' where hfshonest_def: "hfhonestc ∈ set hfshonest" "(ainfo, hfshonest) ∈ auth_seg2 uinfo'"
using hfhonestc_valid
apply-
apply(drule COND_terms_hf) using assms apply auto
using hfhonestc_valid hfhonestc_fut by auto
then obtain uinfo' where hfhonestc_valid':
"hf_valid ainfo uinfo' hfshonest hfhonestc" by(auto simp add: auth_seg2_def)
then have uinfo'_uinfo[simp]:"uinfo' = uinfo" using hfhonestc_valid COND_hf_valid_uinfo by simp
then have AHIS_hfshonest[simp]: "AHIS hfshonest = AHIS (rev(pas)@fut)"
using hfhonestc_valid hfhonestc_valid' by(auto dest!: COND_extr)
show ?thesis
using hfshonest_def[simplified]
apply(auto simp add: auth_seg2_def pfragment_def simp del: AHIS_def map_append)
using takeWhile_dropWhile_id map_append AHIS_def by metis
next
case False
then show ?thesis
by (auto intro!: pfragment_self ASM_adversary)
qed
qed
lemma upd_uinfo_pkt_id[simp]: "upd_uinfo_pkt pkt = UInfo pkt"
apply(cases pkt)
subgoal for _ _ _ hfs
apply(cases hfs)
by auto
done
print_locale dataplane_2
sublocale dataplane_2 _ _ _ _ hfs_valid_prefix_generic _ _ _ _ _ _ no_oracle _ _ hf_valid_generic upd_uinfo
apply unfold_locales
using prefix_hfs_valid_prefix_generic
by (auto simp add: ik_seg_is_auth strip_ifs_valid_prefix simp del: AHIS_def)
end
end