Theory EPIC_L1_SA
section ‹EPIC Level 1 in the Strong Attacker Model›
theory EPIC_L1_SA
imports
"../Parametrized_Dataplane_3_directed"
"../infrastructure/Keys"
begin
type_synonym EPIC_HF = "(unit, msgterm) HF"
type_synonym UINFO = "nat"
locale epic_l1_defs = network_assums_direct _ _ _ auth_seg0
for auth_seg0 :: "(msgterm × ahi list) set" +
fixes no_oracle :: "msgterm ⇒ UINFO ⇒ bool"
begin
subsection ‹Hop validation check and extract functions›
text‹The predicate @{term "hf_valid"} is given to the concrete parametrized model as a parameter.
It ensures the authenticity of the hop authenticator in the hop field. The predicate takes an authenticated
info field (in this model always a numeric value, hence the matching on Num ts), an unauthenticated
info field uinfo, the hop field to be validated and in some cases the next hop field.
We distinguish if there is a next hop field (this yields the two cases below). If there is not, then
the hop authenticator @{text "σ"} simply consists of a MAC over the authenticated info field and the local
routing information of the hop, using the key of the hop to which the hop field belongs. If on the
other hand, there is a subsequent hop field, then the uhi field of that hop field is also included
in the MAC computation.
The hop authenticator @{text "σ"} is used to compute both the hop validation field and the uhi field.
The first is computed as a MAC over the path origin (pair of absolute timestamp ts and the relative
timestamp given in uinfo), using the hop authenticator as a key to the MAC. The hop authenticator
is not secret, and any end host can use it to create a valid hvf. The uhi field, according to the
protocol description, is @{text "σ"} shortened to a few bytes. We model this as applying the hash on @{text "σ"}.
The predicate @{term "hf_valid"} checks if the hop authenticator, hvf and uhi field are computed
correctly.›
fun hf_valid :: "msgterm ⇒ UINFO
⇒ EPIC_HF
⇒ EPIC_HF option ⇒ bool" where
"hf_valid (Num ts) uinfo ⦇AHI = ahi, UHI = uhi, HVF = x⦈ (Some ⦇AHI = ahi2, UHI = uhi2, HVF = x2⦈) ⟷
(∃σ upif downif. σ = Mac[macKey (ASID ahi)] (L [Num ts, upif, downif, uhi2]) ∧
ASIF (DownIF ahi) downif ∧ ASIF (UpIF ahi) upif ∧ uhi = Hash σ ∧ x = Mac[σ] ⟨Num ts, Num uinfo⟩)"
| "hf_valid (Num ts) uinfo ⦇AHI = ahi, UHI = uhi, HVF = x⦈ None ⟷
(∃σ upif downif. σ = Mac[macKey (ASID ahi)] (L [Num ts, upif, downif]) ∧
ASIF (DownIF ahi) downif ∧ ASIF (UpIF ahi) upif ∧ uhi = Hash σ ∧ x = Mac[σ] ⟨Num ts, Num uinfo⟩)"
| "hf_valid _ _ _ _ = False"
definition upd_uinfo :: "nat ⇒ EPIC_HF ⇒ nat" where
"upd_uinfo uinfo hf ≡ uinfo"
text‹We can extract the entire path from the uhi field, since it includes the hop authenticator,
which includes the local forwarding information as well as, recursively, all upstream hop
authenticators and their hop information.
However, the parametrized model defines the extract function to operate on the hop validation field,
not the uhi field. We therefore define a separate function that extracts the path from a hvf.
We can do so, as both hvf and uhi contain the hop authenticator.
Internally, that function uses @{term "extrUhi"}.›
fun extrUhi :: "msgterm ⇒ ahi list" where
"extrUhi (Hash (Mac[macKey asid] (L [ts, upif, downif, uhi2])))
= ⦇UpIF = term2if upif, DownIF = term2if downif, ASID = asid⦈ # extrUhi uhi2"
| "extrUhi (Hash (Mac[macKey asid] (L [ts, upif, downif])))
= [⦇UpIF = term2if upif, DownIF = term2if downif, ASID = asid⦈]"
| "extrUhi _ = []"
text‹This function extracts from a hop validation field (HVF hf) the entire path.›
fun extr :: "msgterm ⇒ ahi list" where
"extr (Mac[σ] _) = extrUhi (Hash σ)"
| "extr _ = []"
text‹Extract the authenticated info field from a hop validation field.›
fun extr_ainfo :: "msgterm ⇒ msgterm" where
"extr_ainfo (Mac[_] ⟨Num ts, _⟩) = Num ts"
| "extr_ainfo _ = ε"
abbreviation term_ainfo :: "msgterm ⇒ msgterm" where
"term_ainfo ≡ id"
text‹When observing a hop field, an attacker learns the HVF and the UHI. The AHI only contains
public information that are not terms.›
fun terms_hf :: "EPIC_HF ⇒ msgterm set" where
"terms_hf hf = {HVF hf, UHI hf}"
abbreviation terms_uinfo :: "UINFO ⇒ msgterm set" where
"terms_uinfo x ≡ {}"
text‹An authenticated info field is always a number (corresponding to a timestamp). The
unauthenticated info field is as well a number, representing combination of timestamp offset
and SRC address.›
definition auth_restrict where
"auth_restrict ainfo uinfo l ≡ (∃ts. ainfo = Num ts)"
text‹We now define useful properties of the above definition.›
lemma hf_valid_invert:
"hf_valid tsn uinfo hf mo ⟷
((∃ahi ahi2 σ ts upif downif asid x upif2 downif2 asid2 uhi uhi2 x2.
hf = ⦇AHI = ahi, UHI = uhi, HVF = x⦈ ∧
ASID ahi = asid ∧ ASIF (DownIF ahi) downif ∧ ASIF (UpIF ahi) upif ∧
mo = Some ⦇AHI = ahi2, UHI = uhi2, HVF = x2⦈ ∧
ASID ahi2 = asid2 ∧ ASIF (DownIF ahi2) downif2 ∧ ASIF (UpIF ahi2) upif2 ∧
σ = Mac[macKey asid] (L [tsn, upif, downif, uhi2]) ∧
tsn = Num ts ∧
uhi = Hash σ ∧
x = Mac[σ] ⟨tsn, Num uinfo⟩)
∨ (∃ahi σ ts upif downif asid uhi x.
hf = ⦇AHI = ahi, UHI = uhi, HVF = x⦈ ∧
ASID ahi = asid ∧ ASIF (DownIF ahi) downif ∧ ASIF (UpIF ahi) upif ∧
mo = None ∧
σ = Mac[macKey asid] (L [tsn, upif, downif]) ∧
tsn = Num ts ∧
uhi = Hash σ ∧
x = Mac[σ] ⟨tsn, Num uinfo⟩)
)"
apply(auto elim!: hf_valid.elims) using option.exhaust ASIF.simps by metis+
lemma hf_valid_auth_restrict[dest]: "hf_valid ainfo uinfo hf z ⟹ auth_restrict ainfo uinfo l"
by(auto simp add: hf_valid_invert auth_restrict_def)
lemma auth_restrict_ainfo[dest]: "auth_restrict ainfo uinfo l ⟹ ∃ts. ainfo = Num ts"
by(auto simp add: auth_restrict_def)
lemma info_hvf:
assumes "hf_valid ainfo uinfo m z" "HVF m = Mac[σ] ⟨ainfo', Num uinfo'⟩ ∨ hf_valid ainfo' uinfo' m z'"
shows "uinfo = uinfo'" "ainfo' = ainfo"
using assms by(auto simp add: hf_valid_invert)
subsection‹Definitions and properties of the added intruder knowledge›
text‹Here we define two sets which are added to the intruder knowledge: @{text "ik_add"}, which contains hop
authenticators. And @{text "ik_oracle"}, which contains the oracle's output to the strong attacker.›
print_locale dataplane_3_directed_defs
sublocale dataplane_3_directed_defs _ _ _ auth_seg0 hf_valid auth_restrict extr extr_ainfo term_ainfo
terms_hf terms_uinfo upd_uinfo no_oracle
by unfold_locales
abbreviation is_oracle where "is_oracle ainfo t ≡ ¬ no_oracle ainfo t "
declare TWu.holds_set_list[dest]
declare TWu.holds_takeW_is_identity[simp]
declare parts_singleton[dest]
text‹This additional Intruder Knowledge allows us to model the attacker's access not only to the
hop validation fields and segment identifiers of authorized segments (which are already given in
@{text "ik_hfs"}), but to the underlying hop authenticators that are used to create them.›
definition ik_add :: "msgterm set" where
"ik_add ≡ { σ | ainfo uinfo l hf σ.
(ainfo::msgterm, l::(EPIC_HF list)) ∈
((local.auth_seg2 uinfo)::((msgterm × EPIC_HF list) set))
∧ hf ∈ set l ∧ HVF hf = Mac[σ] ⟨ainfo, Num uinfo⟩ }"
lemma ik_addI:
"⟦(ainfo, l) ∈ local.auth_seg2 uinfo; hf ∈ set l; HVF hf = Mac[σ] ⟨ainfo, Num uinfo⟩⟧ ⟹ σ ∈ ik_add"
by(auto simp add: ik_add_def)
lemma ik_add_form: "t ∈ local.ik_add ⟹ ∃ asid l . t = Mac[macKey asid] l"
by(auto simp add: ik_add_def auth_seg2_def dest!: TWu.holds_set_list)
(auto simp add: hf_valid_invert)
lemma parts_ik_add[simp]: "parts ik_add = ik_add"
by (auto intro!: parts_Hash dest: ik_add_form)
text‹This is the oracle output provided to the adversary. Only those hop validation fields and
segment identifiers whose path origin (combination of ainfo uinfo) is not contained in
@{term "no_oracle"} appears here.›
definition ik_oracle :: "msgterm set" where
"ik_oracle = {t | t ainfo hf l uinfo . hf ∈ set l ∧ hfs_valid_None ainfo uinfo l ∧
is_oracle ainfo uinfo ∧ (∀uinfo' . (ainfo, l) ∉ auth_seg2 uinfo') ∧
(t = HVF hf ∨ t = UHI hf) }"
lemma ik_oracle_parts_form:
"t ∈ ik_oracle ⟹
(∃ asid l ainfo uinfo . t = Mac[Mac[macKey asid] l] ⟨ainfo, uinfo⟩) ∨
(∃ asid l . t = Hash (Mac[macKey asid] l))"
by(auto simp add: ik_oracle_def hf_valid_invert dest!: TWu.holds_set_list)
lemma parts_ik_oracle[simp]: "parts ik_oracle = ik_oracle"
by (auto intro!: parts_Hash dest: ik_oracle_parts_form)
lemma ik_oracle_simp: "t ∈ ik_oracle ⟷
(∃ainfo hf l uinfo. hf ∈ set l ∧ hfs_valid_None ainfo uinfo l ∧ is_oracle ainfo uinfo
∧ (∀uinfo'. (ainfo, l) ∉ auth_seg2 uinfo') ∧ (t = HVF hf ∨ t = UHI hf))"
by(rule iffI, frule ik_oracle_parts_form)
(auto simp add: ik_oracle_def hf_valid_invert)
subsection‹Properties of the intruder knowledge, including @{text "ik_add"} and @{text "ik_oracle"}›
text‹We now instantiate the parametrized model's definition of the intruder knowledge, using the
definitions of @{text "ik_add"} and @{text "ik_oracle"} from above. We then prove the properties
that we need to instantiate the @{text "dataplane_3_directed"} locale.›
sublocale
dataplane_3_directed_ik_defs _ _ _ auth_seg0 terms_uinfo no_oracle hf_valid auth_restrict extr extr_ainfo term_ainfo
terms_hf upd_uinfo ik_add ik_oracle
by unfold_locales
lemma ik_hfs_form: "t ∈ parts ik_hfs ⟹ ∃ t' . t = Hash t'"
by(auto 3 4 simp add: auth_seg2_def hf_valid_invert)
declare ik_hfs_def[simp del]
lemma parts_ik_hfs[simp]: "parts ik_hfs = ik_hfs"
by (auto intro!: parts_Hash ik_hfs_form)
text‹This lemma allows us not only to expand the definition of @{term "ik_hfs"}, but also
to obtain useful properties, such as a term being a Hash, and it being part of a valid hop field.›
lemma ik_hfs_simp:
"t ∈ ik_hfs ⟷ (∃t' . t = Hash t') ∧ (∃hf . (t = HVF hf ∨ t = UHI hf)
∧ (∃hfs. hf ∈ set hfs ∧ (∃ainfo uinfo . (ainfo, hfs) ∈ auth_seg2 uinfo
∧ (∃nxt. hf_valid ainfo uinfo hf nxt))))" (is "?lhs ⟷ ?rhs")
proof
assume asm: "?lhs"
then obtain ainfo uinfo hf hfs where
dfs: "hf ∈ set hfs" "(ainfo, hfs) ∈ auth_seg2 uinfo" "t = HVF hf ∨ t = UHI hf"
by(auto simp add: ik_hfs_def)
then have "hfs_valid_None ainfo uinfo hfs" "(ainfo, AHIS hfs) ∈ auth_seg0"
by(auto simp add: auth_seg2_def)
then show "?rhs" using asm dfs
using upd_uinfo_def
by (auto 3 4 simp add: auth_seg2_def intro!: ik_hfs_form exI[of _ hf] exI[of _ hfs]
dest: TWu.holds_set_list_no_update)
qed(auto simp add: ik_hfs_def)
subsubsection ‹Properties of Intruder Knowledge›
lemma auth_ainfo[dest]: "⟦(ainfo, hfs) ∈ auth_seg2 uinfo⟧ ⟹ ∃ ts . ainfo = Num ts"
by(auto simp add: auth_seg2_def)
text ‹There are no ciphertexts (or signatures) in @{term "parts ik"}. Thus, @{term "analz ik"}
and @{term "parts ik"} are identical.›
lemma analz_parts_ik[simp]: "analz ik = parts ik"
apply(rule no_crypt_analz_is_parts)
by(auto simp add: ik_def auth_seg2_def auth_restrict_def ik_hfs_simp)
(auto simp add: ik_add_def ik_oracle_def auth_seg2_def hf_valid_invert hfs_valid_prefix_generic_def
dest!: TWu.holds_set_list)
lemma parts_ik[simp]: "parts ik = ik"
by(auto 3 4 simp add: ik_def auth_seg2_def auth_restrict_def dest!: parts_singleton_set)
lemma key_ik_bad: "Key (macK asid) ∈ ik ⟹ asid ∈ bad"
by(auto simp add: ik_def hf_valid_invert ik_oracle_simp)
(auto 3 4 simp add: auth_seg2_def ik_hfs_simp ik_add_def hf_valid_invert)
subsubsection‹Hop authenticators are agnostic to uinfo field›
text‹Those hop validation fields contained in @{term "auth_seg2"} or that can be generated from the hop
authenticators in @{text "ik_add"} have the property that they are agnostic about the uinfo field. If a
hop validation field is contained in @{term "auth_seg2"} (resp. derivable from @{text "ik_add"}),
then a field with a different uinfo is also contained (resp. derivable).
To show this, we first define a function that updates uinfo in a hop validation field.›
fun uinfo_change_hf :: "UINFO ⇒ EPIC_HF ⇒ EPIC_HF" where
"uinfo_change_hf new_uinfo hf =
(case HVF hf of Mac[σ] ⟨ainfo, uinfo⟩ ⇒ hf⦇HVF := Mac[σ] ⟨ainfo, Num new_uinfo⟩⦈ | _ ⇒ hf)"
fun uinfo_change :: "UINFO ⇒ EPIC_HF list ⇒ EPIC_HF list" where
"uinfo_change new_uinfo hfs = map (uinfo_change_hf new_uinfo) hfs"
lemma uinfo_change_valid:
"hfs_valid ainfo uinfo l nxt ⟹ hfs_valid ainfo new_uinfo (uinfo_change new_uinfo l) nxt"
apply(induction l nxt rule: TWu.holds.induct[where ?upd=upd_uinfo])
apply auto
subgoal for info x y ys nxt
by(cases "map (uinfo_change_hf new_uinfo) ys")
(cases info, auto 3 4 simp add: TWu.holds_split_tail hf_valid_invert upd_uinfo_def)+
by(auto 3 4 simp add: TWu.holds_split_tail hf_valid_invert TWu.holds.simps upd_uinfo_def)
lemma uinfo_change_hf_AHI: "AHI (uinfo_change_hf new_uinfo hf) = AHI hf"
apply(cases "HVF hf") apply auto
subgoal for x apply(cases x) apply auto
subgoal for x1 x2 apply(cases x2) by auto
done
done
lemma uinfo_change_hf_AHIS[simp]: "AHIS (map (uinfo_change_hf new_uinfo) l) = AHIS l"
apply(induction l) using uinfo_change_hf_AHI by auto
lemma uinfo_change_auth_seg2:
assumes "hf_valid ainfo uinfo m z" "σ = Mac[Key (macK asid)] j"
"HVF m = Mac[σ] ⟨ainfo, Num uinfo'⟩" "σ ∈ ik_add" "no_oracle ainfo uinfo"
shows "∃hfs. m ∈ set hfs ∧ (∃uinfo''. (ainfo, hfs) ∈ auth_seg2 uinfo'')"
proof-
from assms(4) obtain ainfo_add uinfo_add l_add hf_add where
"(ainfo_add, l_add) ∈ auth_seg2 uinfo_add" "hf_add ∈ set l_add" "HVF hf_add = Mac[σ] ⟨ainfo_add, Num uinfo_add⟩"
by(auto simp add: ik_add_def)
then have add: "m ∈ set (uinfo_change uinfo l_add)" "(ainfo_add, (uinfo_change uinfo l_add)) ∈ auth_seg2 uinfo"
using assms(1-3,5) apply(auto simp add: auth_seg2_def simp del: AHIS_def)
apply(auto simp add: hf_valid_invert intro!: image_eqI dest!: TWu.holds_set_list)[1]
apply(auto simp add: auth_restrict_def intro!: exI elim: ahi_eq dest: uinfo_change_valid simp del: AHIS_def)
by(auto simp add: hf_valid_invert upd_uinfo_def dest!: TWu.holds_set_list_no_update)
then have "ainfo_add = ainfo"
using assms(1) by(auto simp add: auth_seg2_def dest!: TWu.holds_set_list dest: info_hvf)
then show ?thesis using add by fastforce
qed
lemma MAC_synth_oracle:
assumes "hf_valid ainfo uinfo m z" "HVF m ∈ ik_oracle"
shows "is_oracle ainfo uinfo"
using assms
by(auto simp add: ik_oracle_def assms(1) hf_valid_invert upd_uinfo_def
dest!: TWu.holds_set_list_no_update)
lemma ik_oracle_is_oracle:
"⟦Mac[σ] ⟨ainfo, Num uinfo⟩ ∈ ik_oracle⟧ ⟹ is_oracle ainfo uinfo"
by (auto simp add: ik_oracle_def dest: info_hvf)
(auto dest!: TWu.holds_set_list_no_update simp add: hf_valid_invert upd_uinfo_def)
lemma MAC_synth_helper:
"⟦hf_valid ainfo uinfo m z; no_oracle ainfo uinfo;
HVF m = Mac[σ] ⟨ainfo, Num uinfo⟩; σ = Mac[Key (macK asid)] j; σ ∈ ik ∨ HVF m ∈ ik⟧
⟹ ∃hfs. m ∈ set hfs ∧ (∃uinfo'. (ainfo, hfs) ∈ auth_seg2 uinfo')"
apply(auto simp add: ik_def ik_hfs_simp
dest: MAC_synth_oracle ik_add_form ik_oracle_parts_form[simplified])
prefer 3 subgoal by(auto elim!: uinfo_change_auth_seg2)
prefer 3 subgoal by(auto elim!: uinfo_change_auth_seg2 intro: ik_addI dest: info_hvf HOL.sym)
by(auto simp add: hf_valid_invert)
text‹This definition helps with the limiting the number of cases generated. We don't require it,
but it is convenient. Given a hop validation field and an asid, return if the hvf has the expected
format.›
definition mac_format :: "msgterm ⇒ as ⇒ bool" where
"mac_format m asid ≡ ∃ j ts uinfo . m = Mac[Mac[macKey asid] j] ⟨Num ts, uinfo⟩"
text‹If a valid hop field is derivable by the attacker, but does not belong to the attacker, and is
over a path origin that does not belong to an oracle query, then the hop field is already
contained in the set of authorized segments.›
lemma MAC_synth:
assumes "hf_valid ainfo uinfo m z" "HVF m ∈ synth ik" "mac_format (HVF m) asid"
"asid ∉ bad" "no_oracle ainfo uinfo"
shows "∃hfs . m ∈ set hfs ∧ (∃uinfo'. (ainfo, hfs) ∈ auth_seg2 uinfo')"
using assms
apply(auto simp add: mac_format_def elim!: MAC_synth_helper dest!: key_ik_bad)
apply(auto simp add: ik_def ik_hfs_simp dest: ik_add_form dest!: ik_oracle_parts_form)
using assms(1) by(auto dest: info_hvf simp add: hf_valid_invert)
subsection‹Direct proof goals for interpretation of @{text "dataplane_3_directed"}›
lemma COND_honest_hf_analz:
assumes "ASID (AHI hf) ∉ bad" "hf_valid ainfo uinfo hf nxt" "terms_hf hf ⊆ synth (analz ik)"
"no_oracle ainfo uinfo"
shows "terms_hf hf ⊆ analz ik"
proof-
let ?asid = "ASID (AHI hf)"
from assms(3) have hf_synth_ik: "HVF hf ∈ synth ik" "UHI hf ∈ synth ik" by auto
from assms(2) have "mac_format (HVF hf) ?asid"
by(auto simp add: mac_format_def hf_valid_invert)
then obtain hfs uinfo where "hf ∈ set hfs" "(ainfo, hfs) ∈ auth_seg2 uinfo"
using assms(1,2,4) hf_synth_ik by(auto dest!: MAC_synth)
then have "HVF hf ∈ ik" "UHI hf ∈ ik"
using assms(2)
by(auto simp add: ik_hfs_def intro!: ik_ik_hfs intro!: exI)
then show ?thesis by auto
qed
lemma COND_terms_hf:
assumes "hf_valid ainfo uinfo hf z" and "HVF hf ∈ ik" and "no_oracle ainfo uinfo"
shows "∃hfs. hf ∈ set hfs ∧ (∃uinfo . (ainfo, hfs) ∈ auth_seg2 uinfo)"
proof-
obtain hfs ainfo where hfs_def: "hf ∈ set hfs" "(ainfo, hfs) ∈ auth_seg2 uinfo"
using assms by(auto 3 4 simp add: hf_valid_invert ik_hfs_simp ik_def dest: ahi_eq
dest!: ik_oracle_is_oracle ik_add_form)
then obtain hfs ainfo where hfs_def: "hf ∈ set hfs" "(ainfo, hfs) ∈ auth_seg2 uinfo" by auto
show ?thesis
using hfs_def apply (auto simp add: auth_seg2_def dest!: TWu.holds_set_list)
using hfs_def assms(1) by (auto simp add: auth_seg2_def dest: info_hvf)
qed
lemma COND_extr_prefix_path:
"⟦hfs_valid ainfo uinfo l nxt; nxt = None⟧ ⟹ prefix (extr_from_hd l) (AHIS l)"
by(induction l nxt rule: TWu.holds.induct[where ?upd=upd_uinfo])
(auto simp add: upd_uinfo_def TWu.holds_split_tail TWu.holds.simps(1) hf_valid_invert,
auto split: list.split_asm simp add: hf_valid_invert intro!: ahi_eq elim: ASIF.elims)
lemma COND_path_prefix_extr:
"prefix (AHIS (hfs_valid_prefix ainfo uinfo l nxt))
(extr_from_hd l)"
apply(induction l nxt rule: TWu.takeW.induct[where ?Pa="hf_valid ainfo",where ?upd=upd_uinfo])
by(auto simp add: upd_uinfo_def TWu.takeW_split_tail TWu.takeW.simps(1))
(auto 3 4 simp add: hf_valid_invert intro!: ahi_eq elim: ASIF.elims)
lemma COND_hf_valid_uinfo:
"⟦hf_valid ainfo uinfo hf nxt; hf_valid ainfo' uinfo' hf nxt'⟧ ⟹ uinfo' = uinfo"
by(auto dest: info_hvf)
lemma COND_upd_uinfo_ik:
"⟦terms_uinfo uinfo ⊆ synth (analz ik); terms_hf hf ⊆ synth (analz ik)⟧
⟹ terms_uinfo (upd_uinfo uinfo hf) ⊆ synth (analz ik)"
by (auto simp add: upd_uinfo_def)
lemma COND_upd_uinfo_no_oracle:
"no_oracle ainfo uinfo ⟹ no_oracle ainfo (upd_uinfo uinfo fld)"
by (auto simp add: upd_uinfo_def)
lemma COND_auth_restrict_upd:
"auth_restrict ainfo uinfo (x#y#hfs)
⟹ auth_restrict ainfo (upd_uinfo uinfo y) (y#hfs)"
by (auto simp add: auth_restrict_def upd_uinfo_def)
subsection‹Instantiation of @{text "dataplane_3_directed"} locale›
print_locale dataplane_3_directed
sublocale
dataplane_3_directed _ _ _ auth_seg0 terms_uinfo terms_hf hf_valid auth_restrict extr extr_ainfo term_ainfo
upd_uinfo ik_add
ik_oracle no_oracle
apply unfold_locales
using COND_terms_hf COND_honest_hf_analz COND_extr_prefix_path
COND_path_prefix_extr COND_hf_valid_uinfo COND_upd_uinfo_ik COND_upd_uinfo_no_oracle
COND_auth_restrict_upd by auto
end
end