Theory ICING_variant2
section ‹ICING variant›
text‹We abstract and simplify from the protocol ICING in several ways. First, we only consider
Proofs of Consent (PoC), not Proofs of Provenance (PoP). Our framework does not support proving the
path validation properties that PoPs provide, and it also currently does not support XOR, and
dynamically changing hop fields.
Thus, instead of embedding $A_i \oplus PoP_{0,1}$, we embed $A_i$ directly.
We also remove the payload from the Hash that is included in each packet.
We offer three versions of this protocol:
\begin{itemize}
\item @{text "ICING"}, which contains our best effort at modeling the protocol as accurately as
possible.
\item @{text "ICING_variant"}, in which we strip down the protocol to what is required to obtain the
security guarantees and remove unnecessary fields.
\item @{text "ICING_variant2"}, in which we furthermore simplify the protocol. The key of the MAC in
this protocol is only the key of the AS, as opposed to a key derived specifically for this hop field.
In order to prove that this scheme is secure, we have to assume that ASes only occur once on an
authorized path, since otherwise the MAC for two different hop fields (by the same AS) would be the
same, and the AS could not distinguish the hop fields based on the MAC.
\end{itemize}›
theory ICING_variant2
imports
"../Parametrized_Dataplane_3_undirected"
begin
locale icing_defs = network_assums_undirect _ _ _ auth_seg0
for auth_seg0 :: "(msgterm × ahi list) set"
+ assumes auth_seg0_no_dups:
"⟦(ainfo, hfs) ∈ auth_seg0; hf ∈ set hfs; hf' ∈ set hfs; ASID hf' = ASID hf⟧ ⟹ hf' = hf"
begin
subsection ‹Hop validation check and extract functions›
type_synonym ICING_HF = "(unit, unit) HF"
text‹The term @{term "sntag"} simply is the AS key. We use it in the computation of @{term "hf_valid"}.›
fun sntag :: "ahi ⇒ msgterm" where
"sntag ⦇UpIF = upif, DownIF = downif, ASID = asid⦈ = macKey asid"
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
expiration timestamp (in this model always a numeric value, hence the matching on
@{term "Num PoC_i_expire"}), the entire segment and the hop field to be validated.›
fun hf_valid :: "msgterm ⇒ msgterm
⇒ ICING_HF list
⇒ ICING_HF
⇒ bool" where
"hf_valid (Num PoC_i_expire) uinfo hfs ⦇AHI = ahi, UHI = uhi, HVF = x⦈ ⟷ uhi = () ∧
x = Mac[sntag ahi] (L ((Num PoC_i_expire)#(map (hf2term o AHI) hfs))) ∧ uinfo = ε"
| "hf_valid _ _ _ _ = False"
text‹We can extract the entire path (past and future) from the hvf field.›
fun extr :: "msgterm ⇒ ahi list" where
"extr (Mac[_] (L hfs))
= map term2hf (tl hfs)"
| "extr _ = []"
text‹Extract the authenticated info field from a hop validation field.›
fun extr_ainfo :: "msgterm ⇒ msgterm" where
"extr_ainfo (Mac[_] (L (Num ts # xs))) = Num ts"
| "extr_ainfo _ = ε"
abbreviation term_ainfo :: "msgterm ⇒ msgterm" where
"term_ainfo ≡ id"
text‹An authenticated info field is always a number (corresponding to a timestamp). The
unauthenticated info field is set to the empty term @{term "ε"}.›
definition auth_restrict where
"auth_restrict ainfo uinfo l ≡ (∃ts. ainfo = Num ts) ∧ (uinfo = ε)"
text‹When observing a hop field, an attacker learns the HVF. UHI is empty and the AHI only contains
public information that are not terms.›
fun terms_hf :: "ICING_HF ⇒ msgterm set" where
"terms_hf hf = {HVF hf}"
abbreviation terms_uinfo :: "msgterm ⇒ msgterm set" where
"terms_uinfo x ≡ {x}"
abbreviation no_oracle where "no_oracle ≡ (λ _ _. True)"
text‹We now define useful properties of the above definition.›
lemma hf_valid_invert:
"hf_valid tsn uinfo hfs hf ⟷
(∃ ts ahi. tsn = Num ts ∧ ahi = AHI hf ∧
UHI hf = () ∧
HVF hf = Mac[sntag ahi] (L ((Num ts)#(map (hf2term o AHI) hfs))) ∧ uinfo = ε)"
apply(cases hf) by(auto elim!: hf_valid.elims)
lemma hf_valid_auth_restrict[dest]: "hf_valid ainfo uinfo hfs hf ⟹ 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 auth_restrict_uinfo[dest]: "auth_restrict ainfo uinfo l ⟹ uinfo = ε"
by(auto simp add: auth_restrict_def)
subsection‹Definitions and properties of the added intruder knowledge›
text‹Here we define a @{text "ik_add"} and @{text "ik_oracle"} as being empty, as these features are
not used in this instance model.›
print_locale dataplane_3_undirected_defs
sublocale dataplane_3_undirected_defs _ _ _ auth_seg0 hf_valid auth_restrict extr extr_ainfo
term_ainfo terms_hf terms_uinfo no_oracle
by unfold_locales
declare parts_singleton[dest]
abbreviation ik_add :: "msgterm set" where "ik_add ≡ {}"
abbreviation ik_oracle :: "msgterm set" where "ik_oracle ≡ {}"
lemma uinfo_empty[dest]: "(ainfo, hfs) ∈ auth_seg2 uinfo ⟹ uinfo = ε"
by(auto simp add: auth_seg2_def auth_restrict_def)
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_undirected"} locale.›
print_locale dataplane_3_undirected_ik_defs
sublocale
dataplane_3_undirected_ik_defs _ _ _ auth_seg0 terms_uinfo no_oracle hf_valid auth_restrict extr
extr_ainfo term_ainfo terms_hf ik_add ik_oracle
by unfold_locales
lemma ik_hfs_form: "t ∈ parts ik_hfs ⟹ ∃ t' . t = Hash t'"
apply auto apply(drule parts_singleton)
by(auto 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
∧ (∃hfs uinfo. hf ∈ set hfs ∧ (∃ainfo . (ainfo, hfs) ∈ auth_seg2 uinfo
∧ hf_valid ainfo uinfo hfs hf)))" (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"
by(auto simp add: ik_hfs_def)
then obtain uinfo where "hfs_valid_prefix ainfo uinfo [] hfs = hfs" "(ainfo, AHIS hfs) ∈ auth_seg0"
by(auto simp add: auth_seg2_def)
then show "?rhs" using asm dfs
by (auto 3 4 simp add: auth_seg2_def intro!: ik_hfs_form exI[of _ hf])
qed(auto simp add: ik_hfs_def)
lemma ik_uinfo_empty[simp]: "ik_uinfo = {ε}"
by(auto simp add: ik_uinfo_def auth_seg2_def auth_restrict_def intro!: exI[of _ "[]"])
declare ik_uinfo_def[simp del]
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)
lemma Num_ik[intro]: "Num ts ∈ ik"
by(auto simp add: ik_def auth_seg2_def auth_restrict_def intro!: exI[of _ "[]"])
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"
by(rule no_crypt_analz_is_parts)
(auto simp add: ik_def auth_seg2_def ik_hfs_simp auth_restrict_def)
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 sntag_synth_bad: "sntag ahi ∈ synth ik ⟹ ASID ahi ∈ bad"
apply(cases ahi)
by(auto simp add: ik_def ik_hfs_simp)
lemma back_subst_set_member: "⟦hf' ∈ set hfs; hf' = hf⟧ ⟹ hf ∈ set hfs" by simp
lemma sntag_asid: "sntag hf = sntag hf' ⟹ ASID hf' = ASID hf" apply(cases hf, cases hf') by auto
lemma map_hf2term_eq: "map (λx. hf2term (AHI x)) hfs = map (λx. hf2term (AHI x)) hfs'
⟹ AHIS hfs' = AHIS hfs" apply(induction hfs hfs' rule: list_induct2', auto)
using term2hf_hf2term by (metis)
subsection‹Direct proof goals for interpretation of @{text "dataplane_3_undirected"}›
lemma COND_honest_hf_analz:
assumes "ASID (AHI hf) ∉ bad" "hf_valid ainfo uinfo hfs hf" "terms_hf hf ⊆ synth (analz ik)"
"no_oracle ainfo uinfo" "hf ∈ set hfs"
shows "terms_hf hf ⊆ analz ik"
proof-
from assms(3) have hf_synth_ik: "HVF hf ∈ synth ik" by auto
then have "∃hfs uinfo. hf ∈ set hfs ∧ (ainfo, hfs) ∈ auth_seg2 uinfo"
using assms(1,2,4,5)
apply(auto simp add: ik_def hf_valid_invert ik_hfs_simp)
subgoal for ts' hf' hfs'
apply (auto intro!: exI[of _ hfs'])
apply(frule back_subst_set_member[where hfs="hfs'"])
apply(rule HF.equality)
apply auto
apply(drule sntag_asid)
apply(drule map_hf2term_eq)
using auth_seg0_no_dups
by (metis (mono_tags, lifting) AHIS_set_rev HF.surjective auth_seg20 old.unit.exhaust)
by(auto simp add: ik_hfs_simp ik_def hf_valid_invert sntag_synth_bad)
then have "HVF 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 hfs hf" and "HVF hf ∈ ik" and "no_oracle ainfo uinfo" and "hf ∈ set hfs"
shows "∃hfs. hf ∈ set hfs ∧ (∃uinfo' . (ainfo, hfs) ∈ auth_seg2 uinfo')"
using assms apply(auto 3 4 simp add: hf_valid_invert ik_hfs_simp ik_def dest: ahi_eq)
subgoal for ts' hf' hfs'
apply (auto intro!: exI[of _ hfs'])
apply(frule back_subst_set_member[where hfs="hfs'"])
apply auto
apply(rule HF.equality)
apply auto
apply(drule sntag_asid)
apply(drule map_hf2term_eq)
using auth_seg0_no_dups
by (metis (mono_tags, lifting) AHIS_set_rev HF.surjective auth_seg20 old.unit.exhaust)
done
lemma COND_extr:
"⟦hf_valid ainfo uinfo l hf⟧ ⟹ extr (HVF hf) = AHIS l"
by(auto simp add: hf_valid_invert)
lemma COND_hf_valid_uinfo:
"⟦hf_valid ainfo uinfo l hf; hf_valid ainfo' uinfo' l' hf⟧
⟹ uinfo' = uinfo"
by(auto simp add: hf_valid_invert)
subsection‹Instantiation of @{text "dataplane_3_undirected"} locale›
print_locale dataplane_3_undirected
sublocale
dataplane_3_undirected _ _ _ auth_seg0 hf_valid auth_restrict extr extr_ainfo term_ainfo terms_uinfo ik_add terms_hf
ik_oracle no_oracle
apply unfold_locales
using COND_terms_hf COND_honest_hf_analz COND_extr COND_hf_valid_uinfo by auto
end
end