Quelle  SCION.thy

(*******************************************************************************
 
  Project: IsaNet

  Author:  Tobias Klenze, ETH Zurich <tobias.klenze@inf.ethz.ch>
  Version: JCSPaper.1.0
  Isabelle Version: Isabelle2021-1

  Copyright (c) 2022 Tobias Klenze
  Licence: Mozilla Public License 2.0 (MPL) / BSD-3-Clause (dual license)

*******************************************************************************)

chapter‹Instances›
text‹Here we instantiate our concrete parametrized models with a number of protocols from the
  and variants of them that we derive ourselves.›
section ‹SCION›
theory SCION
  imports
    "../Parametrized_Dataplane_3_directed"
    "../infrastructure/Keys"
begin

locale scion_defs = network_assums_direct _ _ _ auth_seg0
  for auth_seg0 :: "(msgterm × ahi list) set"
begin

(******************************************************************************)
subsection ‹Hop validation check and extract functions›
(******************************************************************************)
type_synonym SCION_HF = "(unit, unit) HF"

text‹The predicate @{term "hf_valid"} is given to the concrete parametrized model as a parameter.
  ensures the authenticity of the hop authenticator in the hop field. The predicate takes an authenticated
  field (in this model always a numeric value, hence the matching on Num ts), the hop field to
  validated and in some cases the next hop field.

  distinguish if there is a next hop field (this yields the two cases below). If there is not, then
  hvf simply consists of a MAC over the authenticated info field and the local
  information of the hop, using the key of the hop to which the hop field belongs. If on the
  hand, there is a subsequent hop field, then the hvf of that hop field is also included
  the MAC computation.›
fun hf_valid :: "msgterm ==> msgterm
    ==> SCION_HF
    ==> SCION_HF option ==> bool" where 
  "hf_valid (Num ts) uinfo (AHI = ahi, UHI = _, HVF = x) (Some (AHI = ahi2, UHI = _, HVF = x2)) ⟷
    (∃upif downif upif2 downif2.
          x = Mac[macKey (ASID ahi)] (L [Num ts, upif, downif, upif2, downif2, x2]) ∧
          ASIF (DownIF ahi) downif ∧ ASIF (UpIF ahi) upif ∧
          ASIF (DownIF ahi2) downif2 ∧ ASIF (UpIF ahi2) upif2 ∧ uinfo = ε)"
| "hf_valid (Num ts) uinfo (AHI = ahi, UHI = _, HVF = x) None ⟷
    (∃upif downif. x = Mac[macKey (ASID ahi)] (L [Num ts, upif, downif]) ∧
          ASIF (DownIF ahi) downif ∧ ASIF (UpIF ahi) upif ∧ uinfo = ε)"
| "hf_valid _ _ _ _ = False"

definition upd_uinfo :: "msgterm ==> SCION_HF ==> msgterm" where
  "upd_uinfo uinfo hf ≡ uinfo"

text‹We can extract the entire path from the hvf field, which includes the local forwarding of the
  hop, the local forwarding information of the next hop (if existant) and, recursively, all
  hvf fields and their hop information.›
fun extr :: "msgterm ==> ahi list" where
  "extr (Mac[macKey asid] (L [ts, upif, downif, upif2, downif2, x2]))
 = (UpIF = term2if upif, DownIF = term2if downif, ASID = asid) # extr x2"
| "extr (Mac[macKey asid] (L [ts, upif, downif]))
 = [(UpIF = term2if upif, DownIF = term2if downif, ASID = asid)]"
| "extr _ = []"

text‹Extract the authenticated info field from a hop validation field.›
fun extr_ainfo :: "msgterm ==> msgterm" where 
  "extr_ainfo (Mac[macKey asid] (L (Num ts # xs))) = Num ts"
| "extr_ainfo _ = ε"

abbreviation term_ainfo :: "msgterm ==> msgterm" where
  "term_ainfo ≡ id"

text‹When observing a hop field, an attacker learns the HVF. UHI is empty and the AHI only contains
  information that are not terms.›
fun terms_hf :: "SCION_HF ==> msgterm set" where 
  "terms_hf hf = {HVF hf}"

abbreviation terms_uinfo :: "msgterm ==> msgterm set" where 
  "terms_uinfo x ≡ {x}"

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 = ε)"

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 hf mo ⟷
   ((∃ahi ahi2 ts upif downif asid x upif2 downif2 x2.
     hf = (AHI = ahi, UHI = (), HVF = x) ∧
     ASID ahi = asid ∧ ASIF (DownIF ahi) downif ∧ ASIF (UpIF ahi) upif ∧
     mo = Some (AHI = ahi2, UHI = (), HVF = x2) ∧
     ASIF (DownIF ahi2) downif2 ∧ ASIF (UpIF ahi2) upif2 ∧
     x = Mac[macKey asid] (L [tsn, upif, downif, upif2, downif2, x2]) ∧
     tsn = Num ts ∧
     uinfo = ε)
 ∨ (∃ahi ts upif downif asid x.
     hf = (AHI = ahi, UHI = (), HVF = x) ∧
     ASID ahi = asid ∧ ASIF (DownIF ahi) downif ∧ ASIF (UpIF ahi) upif ∧
     mo = None ∧
     x = Mac[macKey asid] (L [tsn, upif, downif]) ∧
     tsn = Num ts ∧
     uinfo = ε)
    )"
  by(auto elim!: hf_valid.elims)

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 info_hvf: 
  assumes "hf_valid ainfo uinfo m z" "hf_valid ainfo' uinfo' m' z'" "HVF m = HVF m'" 
  shows "ainfo' = ainfo" "m' = m"
  using assms by(auto simp add: hf_valid_invert intro: ahi_eq)

(******************************************************************************)
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
  used in this instance model.›

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

declare TWu.holds_set_list[dest]
declare TWu.holds_takeW_is_identity[simp]
declare parts_singleton[dest]

abbreviation ik_add :: "msgterm set" where "ik_add ≡ {}"

abbreviation ik_oracle :: "msgterm set" where "ik_oracle ≡ {}"

(******************************************************************************)
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
  of @{text "ik_add"} and @{text "ik_oracle"} from above. We then prove the properties
  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 auth_ainfo[dest]: "[(ainfo, hfs) ∈ auth_seg2 uinfo] ==> ∃ ts . ainfo = Num ts"
  by(auto simp add: auth_seg2_def auth_restrict_def)

lemma auth_uinfo[dest]: "[(ainfo, hfs) ∈ auth_seg2 uinfo] ==> uinfo = ε"
  by(auto simp add: auth_seg2_def auth_restrict_def)

lemma upds_simp[simp]: "TWu.upds upd_uinfo uinfo hfs = uinfo" 
  by(induction hfs, auto simp add: upd_uinfo_def)

lemma upd_shifted_simp[simp]: "TWu.upd_shifted upd_uinfo uinfo hfs nxt = uinfo"  
  by(induction hfs, auto simp only: TWu.upd_shifted.simps upds_simp)

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
  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. hf ∈ set hfs ∧ (∃ainfo . (ainfo, hfs) ∈ (auth_seg2 ε)
                    ∧ (∃ nxt. hf_valid ainfo ε 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"
    by(auto simp add: ik_hfs_def)
  then have dfs_prop: "hfs_valid_None ainfo ε hfs"  "(ainfo, AHIS hfs) ∈ auth_seg0"
    using auth_uinfo by(auto simp add: auth_seg2_def)
  then obtain nxt where hf_val: "hf_valid ainfo ε hf nxt" using dfs apply auto 
    by(auto dest: TWu.holds_set_list_no_update simp add: upd_uinfo_def) 
  then show "?rhs" using asm dfs dfs_prop hf_val by(auto intro: ik_hfs_form)
qed(auto simp add: ik_hfs_def)

(******************************************************************************)
subsubsection ‹Properties of Intruder Knowledge›
(******************************************************************************)
lemma Num_ik[intro]: "Num ts ∈ ik"
  by(auto simp add: ik_def)
    (auto simp add: auth_seg2_def auth_restrict_def TWu.holds.simps 
            intro!: exI[of _ "[]"] exI[of _ "ε"] ) (*elim!: allE[of _ "[]"]) *)

text ‹There are no ciphertexts (or signatures) in @{term "parts ik"}. Thus, @{term "analz ik"}
  @{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(fastforce simp add: ik_def auth_seg2_def auth_restrict_def)

lemma key_ik_bad: "Key (macK asid) ∈ ik ==> asid ∈ bad"
  by(auto simp add: ik_def hf_valid_invert)
    (auto 3 4 simp add: auth_seg2_def ik_hfs_simp hf_valid_invert)

lemma MAC_synth_helper:
  assumes "hf_valid ainfo uinfo m z" "HVF m = Mac[Key (macK asid)] j" "HVF m ∈ ik"
  shows "∃hfs. m ∈ set hfs ∧ (∃uinfo'. (ainfo, hfs) ∈ auth_seg2 uinfo')"
proof-
  from assms(2-3) obtain ainfo' uinfo' m' hfs' nxt' where dfs:
    "m' ∈ set hfs'" "(ainfo', hfs') ∈ auth_seg2 uinfo'" "hf_valid ainfo' uinfo' m' nxt'" 
    "HVF m = HVF m'"
    by(auto simp add: ik_def ik_hfs_simp)                
  then have "ainfo' = ainfo" "m' = m" using assms(1) by(auto elim!: info_hvf)
  then show ?thesis using dfs assms by auto
qed

text‹This definition helps with the limiting the number of cases generated. We don't require it,
  it is convenient. Given a hop validation field and an asid, return if the hvf has the expected
 .›
definition mac_format :: "msgterm ==> as ==> bool" where 
  "mac_format m asid ≡ ∃ j . m = Mac[macKey asid] j"

text‹If a valid hop field is derivable by the attacker, but does not belong to the attacker, then
  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" "checkInfo ainfo"
  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)
  by(auto simp add: ik_def ik_hfs_simp)

(******************************************************************************)
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" 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) hf_synth_ik by(auto dest!: MAC_synth)
  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 hf z" and "terms_hf hf ⊆ analz ik" and "no_oracle ainfo uinfo"
  shows "∃hfs. hf ∈ set hfs ∧ (∃uinfo' . (ainfo, hfs) ∈ auth_seg2 uinfo')"
proof-
  obtain hfs ainfo uinfo where hfs_def: "hf ∈ set hfs" "(ainfo, hfs) ∈ auth_seg2 uinfo"
    using assms
    using assms
    by simp
       (auto 3 4 simp add: hf_valid_invert ik_hfs_simp ik_def dest: ahi_eq)
  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: 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: 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 simp add: hf_valid_invert)

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