Theory Parametrized_Dataplane_1
section‹Intermediate Model›
theory Parametrized_Dataplane_1
imports
"Parametrized_Dataplane_0"
"infrastructure/Message"
begin
text‹This model is almost identical to the previous one. The only changes are (i) that the receive
event performs an interface check and (ii) that we permit the
attacker to send any packet with a future path whose interface-valid prefix is authorized, as
opposed to requiring that the entire future path is authorized. This means that the attacker can
combine hop fields of subsequent ASes as long as the combination is either authorized, or the
interfaces of the two hop fields do not correspond to each other. In the latter case the packet will
not be delivered to (or accepted by) the second AS.
Because (i) requires the @{text "evt_recv0"} event to check the interface over which packets are received,
in the mapping from this model to the abstract model we can thus cut off all invalid hop fields from
the future path.›
type_synonym ('aahi, 'ainfo) dp1_state = "('aahi, 'ainfo) dp0_state"
type_synonym ('aahi, 'ainfo) pkt1 = "('aahi, 'ainfo) pkt0"
type_synonym ('aahi, 'ainfo) evt1 = "('aahi, 'ainfo) evt0"
context network_model
begin
subsection ‹Events›
definition
dp1_dispatch_int
where
"dp1_dispatch_int s m ainfo asid pas fut hist s' ≡
m = ⦇ AInfo = ainfo, past = pas, future = fut, history = hist ⦈ ∧
hist = [] ∧
pfragment ainfo (ifs_valid_prefix None fut None) auth_seg0 ∧
dp0_add_loc s s' asid m"
text‹We construct an artificial hop field that contains a specified asid and upif. The other fields
are irrelevant, as we only use this artificial hop field as "previous" hop field in the
@{text "ifs_valid_prefix"} function. This is used in the direct dispatch event: the interface-valid prefix
must be authorized. Since the dispatching AS' own hop field is not part of the future path, but the AS
directly after the it does check for the interface correctness, we need this artificial hop
field.›
abbreviation prev_hf where
"prev_hf asid upif ≡
(Some ⦇UpIF = Some upif, DownIF = None, ASID = asid, … = undefined⦈)"
definition
dp1_dispatch_ext
where
"dp1_dispatch_ext s m asid ainfo upif pas fut hist s' ≡
m = ⦇ AInfo = ainfo, past = pas, future = fut, history = hist ⦈ ∧
hist = [] ∧
pfragment ainfo (ifs_valid_prefix (prev_hf asid upif) fut None) auth_seg0 ∧
dp0_add_chan s s' asid upif m"
definition
dp1_recv
where
"dp1_recv s m asid ainfo hf1 downif pas fut hist s' ≡
DownIF hf1 = Some downif
∧ dp0_recv s m asid ainfo hf1 downif pas fut hist s'"
subsection ‹Transition system›
fun dp1_trans where
"dp1_trans s (evt_dispatch_int0 asid m) s' ⟷
(∃ainfo pas fut hist. dp1_dispatch_int s m ainfo asid pas fut hist s')" |
"dp1_trans s (evt_dispatch_ext0 asid upif m) s' ⟷
(∃ainfo pas fut hist . dp1_dispatch_ext s m asid ainfo upif pas fut hist s')" |
"dp1_trans s (evt_recv0 asid downif m) s' ⟷
(∃ainfo hf1 pas fut hist. dp1_recv s m asid ainfo hf1 downif pas fut hist s')" |
"dp1_trans s e s' ⟷ dp0_trans s e s'"
definition dp1_init :: "('aahi, 'ainfo) dp1_state" where
"dp1_init ≡ ⦇chan = (λ_. {}), loc = (λ_. {})⦈"
definition dp1 :: "(('aahi, 'ainfo) evt1, ('aahi, 'ainfo) dp1_state) ES" where
"dp1 ≡ ⦇
init = (=) dp1_init,
trans = dp1_trans
⦈"
lemmas dp1_trans_defs = dp0_trans_defs dp1_dispatch_ext_def dp1_recv_def
lemmas dp1_defs = dp1_def dp1_dispatch_int_def dp1_init_def dp1_trans_defs
fun pkt1to0chan :: "as ⇒ ifs ⇒ ('aahi, 'ainfo) pkt1 ⇒ ('aahi, 'ainfo) pkt0" where
"pkt1to0chan asid upif ⦇ AInfo = ainfo, past = pas, future = fut, history = hist ⦈ =
⦇ pkt0.AInfo = ainfo, past = pas, future = ifs_valid_prefix (prev_hf asid upif) fut None, history = hist⦈"
fun pkt1to0loc :: "('aahi, 'ainfo) pkt1 ⇒ ('aahi, 'ainfo) pkt0" where
"pkt1to0loc ⦇ AInfo = ainfo, past = pas, future = fut, history = hist ⦈ =
⦇ pkt0.AInfo = ainfo, past = pas, future = ifs_valid_prefix None fut None, history = hist⦈"
definition R10 :: "('aahi, 'ainfo) dp1_state ⇒ ('aahi, 'ainfo) dp0_state" where
"R10 s =
⦇chan = λ(a1, i1, a2, i2) . (pkt1to0chan a1 i1) ` ((chan s) (a1, i1, a2, i2)),
loc = λx . pkt1to0loc ` ((loc s) x)⦈"
fun π⇩1 :: "('aahi, 'ainfo) evt1 ⇒ ('aahi, 'ainfo) evt0" where
"π⇩1 (evt_dispatch_int0 asid m) = evt_dispatch_int0 asid (pkt1to0loc m)"
| "π⇩1 (evt_recv0 asid downif m) = evt_recv0 asid downif (pkt1to0loc m)"
| "π⇩1 (evt_send0 asid upif m) = evt_send0 asid upif (pkt1to0loc m)"
| "π⇩1 (evt_deliver0 asid m) = evt_deliver0 asid (pkt1to0loc m)"
| "π⇩1 (evt_dispatch_ext0 asid upif m) = evt_dispatch_ext0 asid upif (pkt1to0chan asid upif m)"
| "π⇩1 (evt_observe0 s) = evt_observe0 (R10 s)"
| "π⇩1 evt_skip0 = evt_skip0"
declare TW.takeW.elims[elim]
lemma dp1_refines_dp0: "dp1 ⊑⇩π⇩1 dp0"
proof(rule simulate_ES_fun[where ?h = R10])
fix s0
assume "init dp1 s0"
then show "init dp0 (R10 s0)"
by(auto simp add: dp0_defs dp1_defs R10_def)
next
fix s e s'
assume "dp1: s─e→ s'"
then show "dp0: R10 s─ π⇩1 e→ R10 s'"
proof(auto simp add: dp1_def elim!: dp1_trans.elims dp0_trans.elims)
fix m ainfo asid pas fut hist
assume "dp1_dispatch_int s m ainfo asid pas fut hist s'"
then show "dp0: R10 s─evt_dispatch_int0 asid (pkt1to0loc m)→ R10 s'"
by(auto 3 4 simp add: dp0_defs dp1_defs dp0_msgs R10_def
intro: TW.takeW_prefix elim: pfragment_prefix' dest: strip_ifs_valid_prefix)
next
fix m asid ainfo hf1 downif pas fut hist
assume "dp1_recv s m asid ainfo hf1 downif pas fut hist s'"
then show "dp0: R10 s─evt_recv0 asid downif (pkt1to0loc m)→ R10 s'"
by(auto simp add: dp0_defs dp1_defs dp0_msgs R10_def TW.takeW_split_tail
elim!: rev_image_eqI intro!: ext)
next
fix m asid ainfo hf1 upif pas fut hist
assume "dp0_send s m asid ainfo hf1 upif pas fut hist s'"
then show "dp0: R10 s─evt_send0 asid upif (pkt1to0loc m)→ R10 s'"
by(cases "ifs_valid_None_prefix (hf1 # fut)")
(auto 3 4 simp add: dp0_defs dp1_defs dp0_msgs R10_def TW.takeW_split_tail TW.takeW.simps
elim!: rev_image_eqI TW.takeW.elims intro!: TW.takeW_pre_eqI)
next
fix m asid ainfo hf1 pas fut hist
assume "dp0_deliver s m asid ainfo hf1 pas fut hist s'"
then show "dp0: R10 s─evt_deliver0 asid (pkt1to0loc m)→ R10 s'"
by(auto simp add: dp0_defs dp1_defs dp0_msgs R10_def TW.takeW.simps
intro!: ext elim!: rev_image_eqI TW.takeW.elims)
qed(auto 3 4 simp add: dp0_defs dp1_defs dp0_msgs R10_def TW.takeW_split_tail)
qed
subsection ‹Auxilliary definitions›
text‹These definitions are not directly needed in the parametrized models, but they are useful for
instances.›
text‹Check if interface option is matched by a msgterm.›
fun ASIF :: "ifs option ⇒ msgterm ⇒ bool" where
"ASIF (Some a) (AS a') = (a=a')"
| "ASIF None ε = True"
| "ASIF _ _ = False"
lemma ASIF_None[simp]: "ASIF ifopt ε ⟷ ifopt = None" by(cases ifopt, auto)
lemma ASIF_AS[simp]: "ASIF ifopt (AS a) ⟷ ifopt = Some a" by(cases ifopt, auto)
text‹Turn a msgterm to an ifs option. Note that this maps both @{text "ε"} (the msgterm denoting the lack of
an interface) and arbitrary other msgterms that are not of the form "AS t" to None. The result may
thus be ambiguous. Use with care.›
fun term2if :: "msgterm ⇒ ifs option" where
"term2if (AS a) = Some a"
| "term2if ε = None"
| "term2if _ = None"
lemma ASIF_term2if[intro]: "ASIF i mi ⟹ ASIF (term2if mi) mi"
by(cases mi, auto)
fun if2term :: "ifs option ⇒ msgterm" where "if2term (Some a) = AS a" | "if2term None = ε"
lemma if2term_eq[elim]: "if2term a = if2term b ⟹ a = b"
apply(cases a, cases b, auto)
using if2term.elims msgterm.distinct(1)
by (metis term2if.simps(1))
lemma term2if_if2termm[simp]: "term2if (if2term a) = a" apply(cases a) by auto
fun hf2term :: "ahi ⇒ msgterm" where
"hf2term ⦇UpIF = upif, DownIF = downif, ASID = asid⦈ = L [if2term upif, if2term downif, Num asid]"
fun term2hf :: "msgterm ⇒ ahi" where
"term2hf (L [upif, downif, Num asid]) = ⦇UpIF = term2if upif, DownIF = term2if downif, ASID = asid⦈"
lemma term2hf_hf2term[simp]: "term2hf (hf2term hf) = hf" apply(cases hf) by auto
lemma ahi_eq:
"⟦ASID ahi' = ASID (ahi::ahi); ASIF (DownIF ahi') downif; ASIF (UpIF ahi') upif;
ASIF (DownIF ahi) downif; ASIF (UpIF ahi) upif⟧ ⟹ ahi = ahi'"
by(cases ahi, cases ahi')
(auto elim: ASIF.elims ahi.cases)
end
end