Theory EPIC_L1_SA_Example

(*******************************************************************************
 
  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)

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

section ‹EPIC Level 1 Example instantiation of locale›
text‹In this theory we instantiate the locale @{text "dataplane0"} and thus show that its
assumptions are satisfiable. In particular, this involves the assumptions concerning the network.
We also instantiate the locale @{text "epic_l1_defs"}.›
theory EPIC_L1_SA_Example
  imports
    "EPIC_L1_SA"
begin

(*  
   A
  / \
 B   C
  \ /
   D
   |
   E
  / \
 F   G
*)

text‹The network topology that we define is the same as in the paper.›

abbreviation nA :: as where "nA ≡ 3"
abbreviation nB :: as where "nB ≡ 4"
abbreviation nC :: as where "nC ≡ 5"
abbreviation nD :: as where "nD ≡ 6"
abbreviation nE :: as where "nE ≡ 7"
abbreviation nF :: as where "nF ≡ 8"
abbreviation nG :: as where "nG ≡ 9"

abbreviation bad :: "as set" where "bad ≡ {nF}"

text‹We assume a complete graph, in which interfaces contain the name of the adjacent AS›
fun tgtas :: "as ⇒ ifs ⇒ as option" where
  "tgtas a i = Some i"
fun tgtif :: "as ⇒ ifs ⇒ ifs option" where
  "tgtif a i = Some a"

subsection‹Left segment›
abbreviation hiAl :: "ahi" where "hiAl ≡ ⦇UpIF = None, DownIF = Some nB, ASID = nA⦈"
abbreviation hiBl :: "ahi" where "hiBl ≡ ⦇UpIF = Some nA, DownIF = Some nD, ASID = nB⦈"
abbreviation hiDl :: "ahi" where "hiDl ≡ ⦇UpIF = Some nB, DownIF = Some nE, ASID = nD⦈"
abbreviation hiEl :: "ahi" where "hiEl ≡ ⦇UpIF = Some nD, DownIF = Some nF, ASID = nE⦈"
abbreviation hiFl :: "ahi" where "hiFl ≡ ⦇UpIF = Some nE, DownIF = None, ASID = nF⦈"

subsection‹Right segment›
abbreviation hiAr :: "ahi" where "hiAr ≡ ⦇UpIF = None, DownIF = Some nB, ASID = nA⦈"
abbreviation hiBr :: "ahi" where "hiBr ≡ ⦇UpIF = Some nA, DownIF = Some nD, ASID = nB⦈"
abbreviation hiDr :: "ahi" where "hiDr ≡ ⦇UpIF = Some nB, DownIF = Some nE, ASID = nD⦈"
abbreviation hiEr :: "ahi" where "hiEr ≡ ⦇UpIF = Some nD, DownIF = Some nG, ASID = nE⦈"
abbreviation hiGr :: "ahi" where "hiGr ≡ ⦇UpIF = Some nE, DownIF = None, ASID = nG⦈"

abbreviation hfF_attr_E :: "ahi set" where "hfF_attr_E ≡ {hi . ASID hi = nF ∧ UpIF hi = Some nE}"
abbreviation hfF_attr :: "ahi set" where "hfF_attr ≡ {hi . ASID hi = nF}"

abbreviation leftpath :: "ahi list" where 
  "leftpath ≡ [hiFl, hiEl, hiDl, hiBl, hiAl]"
abbreviation rightpath :: "ahi list" where 
  "rightpath ≡ [hiGr, hiEr, hiDr, hiBr, hiAr]"
abbreviation rightsegment where "rightsegment ≡ (Num 0, rightpath)"

abbreviation leftpath_wormholed :: "ahi list set" where 
  "leftpath_wormholed ≡ 
    { xs@[hf, hiEl, hiDl, hiBl, hiAl] | hf xs . hf ∈ hfF_attr_E ∧ set xs ⊆ hfF_attr}"

definition leftsegment_wormholed :: "(msgterm × ahi list) set" where 
  "leftsegment_wormholed = { (Num 0, leftpath) | leftpath . leftpath ∈ leftpath_wormholed}"

definition attr_segment :: "(msgterm × ahi list) set" where 
  "attr_segment = { (ainfo, path) | ainfo path . set path ⊆ hfF_attr}"

definition auth_seg0 :: "(msgterm × ahi list) set" where 
  "auth_seg0 = leftsegment_wormholed ∪ {rightsegment} ∪ attr_segment"

lemma tgtasif_inv:
    "⟦tgtas u i = Some v; tgtif u i = Some j⟧ ⟹ tgtas v j = Some u"
    "⟦tgtas u i = Some v; tgtif u i = Some j⟧ ⟹ tgtif v j = Some i"
  by simp+

locale no_assumptions_left 
begin

sublocale d0: network_model bad auth_seg0 tgtas tgtif
  apply unfold_locales
  done

lemma attr_ifs_valid: "⟦ASID y = nF; set ys ⊆ hfF_attr⟧ ⟹ d0.ifs_valid (Some y) ys nxt"
  by(induction ys arbitrary: y)
    (auto simp add: auth_seg0_def leftsegment_wormholed_def attr_segment_def TW.holds_split_tail 
                    TW.holds.simps list.case_eq_if)

lemma attr_ifs_valid': "⟦set ys ⊆ hfF_attr; pre = None⟧ ⟹ d0.ifs_valid pre ys nxt"
  by(induction ys nxt rule: TW.holds.induct)
    (auto simp add: auth_seg0_def leftsegment_wormholed_def attr_segment_def TW.holds_split_tail 
                    TW.holds.simps list.case_eq_if dest: attr_ifs_valid)

lemma leftpath_ifs_valid: "⟦pre = None; ASID hf = nF; UpIF hf = Some nE; set xs ⊆ hfF_attr⟧
    ⟹ d0.ifs_valid pre (xs @ [hf, hiEl, hiDl, hiBl, hiAl]) nxt"
  by(auto simp add: TW.holds_append auth_seg0_def leftsegment_wormholed_def attr_segment_def 
                    TW.holds_split_tail TW.holds.simps list.case_eq_if intro!: attr_ifs_valid')force+

lemma ASM_if_valid: "⟦(info, l) ∈ auth_seg0; pre = None⟧ ⟹ d0.ifs_valid pre l nxt"
  by(auto simp add: auth_seg0_def leftsegment_wormholed_def attr_segment_def TW.holds_split_tail 
                    TW.holds.simps intro: attr_ifs_valid' leftpath_ifs_valid)

(*move to parametrized model?*)
lemma rooted_app[simp]: "d0.rooted (xs@y#ys) ⟷ d0.rooted (y#ys)"
  by(induction xs arbitrary: y ys, auto)
    (metis Nil_is_append_conv d0.rooted.simps(2) d0.terminated.cases)+

lemma ASM_rooted: "(info, l) ∈ auth_seg0 ⟹ d0.rooted l" 
  apply(induction l)
  apply(auto 3 4 simp add: auth_seg0_def leftsegment_wormholed_def attr_segment_def TW.holds_split_tail)
  subgoal for x xs
    by(cases xs, auto)
  done

lemma ASM_terminated: "(info, l) ∈ auth_seg0 ⟹ d0.terminated l"
  apply(auto simp add: auth_seg0_def leftsegment_wormholed_def TW.holds_split_tail attr_segment_def)
  subgoal for hf xs
    by(induction xs, auto)
  by(induction l, auto)

lemma ASM_empty: "(info, []) ∈ auth_seg0" 
  by(auto simp add: auth_seg0_def leftsegment_wormholed_def attr_segment_def)

lemma ASM_singleton: "⟦ASID hf ∈ bad⟧ ⟹ (info, [hf]) ∈ auth_seg0" 
  by(auto simp add: auth_seg0_def leftsegment_wormholed_def attr_segment_def)

lemma ASM_extension: 
  "⟦(info, hf2#ys) ∈ auth_seg0; ASID hf2 ∈ bad; ASID hf1 ∈ bad⟧ 
⟹ (info, hf1#hf2#ys) ∈ auth_seg0" 
  by(auto simp add: auth_seg0_def leftsegment_wormholed_def TW.holds_split_tail attr_segment_def)

lemma ASM_modify: "⟦(info, hf#ys) ∈ auth_seg0; ASID hf = a;
      ASID hf' = a; UpIF hf' = UpIF hf; a ∈ bad⟧ ⟹ (info, hf'#ys) ∈ auth_seg0"
  apply(auto simp add: auth_seg0_def leftsegment_wormholed_def attr_segment_def)
  subgoal for y hfa l
    by(induction l, auto)
  subgoal for y hfa l
    by(induction l, auto)
  done

lemma rightpath_no_nF: "⟦ASID hf = nF; zs @ hf # ys = rightpath⟧ ⟹ False"
apply(cases ys rule: rev_cases, auto)
subgoal for ys' apply(cases ys' rule: rev_cases, auto)
 subgoal for ys'' apply(cases ys'' rule: rev_cases, auto)
  subgoal for ys''' apply(cases ys''' rule: rev_cases, auto)
   subgoal for ys''' by(cases ys''' rule: rev_cases, auto)
   done
  done
 done
done

lemma ASM_cutoff_leftpath:
"⟦ASID hf = nF; 
∀hfa. UpIF hfa = Some nE ⟶ ASID hfa = nF ⟶ (∀xs. hf # ys = xs @ [hfa, hiEl, hiDr, hiBr, hiAr] ⟶ 
¬ set xs ⊆ hfF_attr); x ∈ set ys; info = Num 0;
        zs @ hf # ys = xs @ [hfa, hiEl, hiDr, hiBr, hiAr]; ASID hfa = nF; UpIF hfa = Some nE; set xs ⊆ hfF_attr⟧
       ⟹ ASID x = nF"
apply(cases ys rule: rev_cases, simp)
subgoal for ys' b
 apply(cases ys' rule: rev_cases, simp)
 subgoal for ys'' c
  apply(cases ys'' rule: rev_cases, simp)
  subgoal for ys''' d
   apply(cases ys'' rule: rev_cases, simp)
   subgoal for ys''' e
    apply(cases ys''' rule: rev_cases, simp)
    subgoal for ys'''' f
     apply(cases ys'''' rule: rev_cases, simp)
     by auto blast+
    done
   done
  done
 done
done

lemma ASM_cutoff: "⟦(info, zs@hf#ys) ∈ auth_seg0; ASID hf ∈ bad⟧ ⟹ (info, hf#ys) ∈ auth_seg0"
  apply(simp add: auth_seg0_def, auto dest: rightpath_no_nF)
  by(auto simp add: leftsegment_wormholed_def TW.holds_split_tail attr_segment_def intro: ASM_cutoff_leftpath)

sublocale network_assums_direct_instance: network_assums_direct bad tgtas tgtif auth_seg0
  apply unfold_locales
  using ASM_if_valid ASM_rooted ASM_terminated ASM_empty ASM_singleton ASM_extension ASM_modify ASM_cutoff
  by simp_all

definition no_oracle :: "msgterm ⇒ nat ⇒ bool" where 
  "no_oracle ainfo uinfo = True"

sublocale e1: epic_l1_defs bad tgtas tgtif auth_seg0 no_oracle
  by unfold_locales

declare e1.upd_uinfo_def[simp]
declare TWu.holds_takeW_is_identity[simp]
thm TWu.holds_takeW_is_identity
declare e1.auth_restrict_def [simp]
declare no_oracle_def [simp]
declare e1.upd_pkt_def [simp]

subsection‹Executability›
subsubsection‹Honest sender's packet forwarding›

abbreviation ainfo where "ainfo ≡ Num 0"
abbreviation uinfo :: nat where "uinfo ≡ 1"
abbreviation σA where "σA ≡ Mac[macKey nA] (L [ainfo, ε, AS nB])"
abbreviation σB where "σB ≡ Mac[macKey nB] (L [ainfo, AS nA, AS nD, Hash σA])"
abbreviation σD where "σD ≡ Mac[macKey nD] (L [ainfo, AS nB, AS nE, Hash σB])"
abbreviation σE where "σE ≡ Mac[macKey nE] (L [ainfo, AS nD, AS nF, Hash σD])"
abbreviation σF where "σF ≡ Mac[macKey nF] (L [ainfo, AS nE, ε, Hash σE])"

definition hfAl where "hfAl ≡ ⦇AHI = hiAl, UHI = Hash σA, HVF = Mac[σA] ⟨ainfo, Num uinfo⟩⦈"
definition hfBl where "hfBl ≡ ⦇AHI = hiBl, UHI = Hash σB, HVF = Mac[σB] ⟨ainfo, Num uinfo⟩⦈"
definition hfDl where "hfDl ≡ ⦇AHI = hiDl, UHI = Hash σD, HVF = Mac[σD] ⟨ainfo, Num uinfo⟩⦈"
definition hfEl where "hfEl ≡ ⦇AHI = hiEl, UHI = Hash σE, HVF = Mac[σE] ⟨ainfo, Num uinfo⟩⦈"
definition hfFl where "hfFl ≡ ⦇AHI = hiFl, UHI = Hash σF, HVF = Mac[σF] ⟨ainfo, Num uinfo⟩⦈"

lemmas hfl_defs = hfAl_def hfBl_def hfDl_def hfEl_def hfFl_def

lemma "e1.hf_valid ainfo uinfo hfAl None"
  by (simp add: e1.hf_valid_invert hfAl_def)
lemma "e1.hf_valid ainfo uinfo hfBl (Some hfAl)"
  apply (auto simp add: e1.hf_valid_invert hfAl_def hfBl_def)
  using d0.ASIF.simps by blast+

lemma "e1.hf_valid ainfo uinfo hfFl (Some hfEl)"
  apply (auto intro!: exI simp add: e1.hf_valid_invert hfl_defs)
  using d0.ASIF.simps by blast+

abbreviation forwardingpath where
  "forwardingpath ≡ [hfFl, hfEl, hfDl, hfBl, hfAl]"

definition pkt0 where "pkt0 ≡ ⦇
                AInfo = ainfo,
                UInfo = uinfo,
                past = [],
                future = forwardingpath,
                history = []
              ⦈"
definition pkt1 where "pkt1 ≡ ⦇
                AInfo = ainfo,
                UInfo = uinfo,
                past = [hfFl],
                future = [hfEl, hfDl, hfBl, hfAl],
                history = [hiFl]
              ⦈"
definition pkt2 where "pkt2 ≡ ⦇
                AInfo = ainfo,
                UInfo = uinfo,
                past = [hfEl, hfFl],
                future = [hfDl, hfBl, hfAl],
                history = [hiEl, hiFl]
              ⦈"
definition pkt3 where "pkt3 ≡ ⦇
                AInfo = ainfo,
                UInfo = uinfo,
                past = [hfDl, hfEl, hfFl],
                future = [hfBl, hfAl],
                history = [hiDl, hiEl, hiFl]
              ⦈"
definition pkt4 where "pkt4 ≡ ⦇
                AInfo = ainfo,
                UInfo = uinfo,
                past = [hfBl, hfDl, hfEl, hfFl],
                future = [hfAl],
                history = [hiBl, hiDl, hiEl, hiFl]
              ⦈"
definition pkt5 where "pkt5 ≡ ⦇
                AInfo = ainfo,
                UInfo = uinfo,
                past = [hfAl, hfBl, hfDl, hfEl, hfFl],
                future = [],
                history = [hiAl, hiBl, hiDl, hiEl, hiFl]
              ⦈"

(*s0 -- dispatch -- s1 -- send -- s2 -- recv -- s3 ... s9 -- deliver -- s10*)
definition s0 where "s0 ≡ e1.dp2_init"
definition s1 where "s1 ≡ s0⦇loc2 := (loc2 s0)(nF := {pkt0})⦈"
definition s2 where 
  "s2 ≡ s1⦇chan2 := (chan2 s1)((nF, nE, nE, nF) := chan2 s1 (nF, nE, nE, nF) ∪ {pkt1})⦈"
definition s3 where "s3 ≡ s2⦇loc2 := (loc2 s2)(nE := {pkt1})⦈"
definition s4 where 
  "s4 ≡ s3⦇chan2 := (chan2 s3)((nE, nD, nD, nE) := chan2 s3 (nE, nD, nD, nE) ∪ {pkt2})⦈"
definition s5 where "s5 ≡ s4⦇loc2 := (loc2 s4)(nD := {pkt2})⦈"
definition s6 where 
  "s6 ≡ s5⦇chan2 := (chan2 s5)((nD, nB, nB, nD) := chan2 s5 (nD, nB, nB, nD) ∪ {pkt3})⦈"
definition s7 where "s7 ≡ s6⦇loc2 := (loc2 s6)(nB := {pkt3})⦈"
definition s8 where 
  "s8 ≡ s7⦇chan2 := (chan2 s7)((nB, nA, nA, nB) := chan2 s7 (nB, nA, nA, nB) ∪ {pkt4})⦈"
definition s9 where "s9 ≡ s8⦇loc2 := (loc2 s8)(nA := {pkt4})⦈"
definition s10 where "s10 ≡ s9⦇loc2 := (loc2 s9)(nA := {pkt4, pkt5})⦈"

lemmas forwading_states = 
  s0_def s1_def s2_def s3_def s4_def s5_def s6_def s7_def s8_def s9_def s10_def 

lemma forwardingpath_valid: "e1.hfs_valid_None ainfo uinfo forwardingpath"
  by(auto simp add: TWu.holds_split_tail hfl_defs)

lemma forwardingpath_auth: "pfragment ainfo forwardingpath (e1.auth_seg2 uinfo)"
  apply(auto simp add: e1.auth_seg2_def pfragment_def)
  using forwardingpath_valid
  by(auto intro!: exI[of _ "[]"] simp add: e1.hfs_valid_prefix_generic_def auth_seg0_def leftsegment_wormholed_def hfl_defs)

lemma reach_s0: "reach e1.dp2 s0" by(auto simp add: s0_def e1.dp2_def)

lemma s0_s1: "e1.dp2: s0 ─evt_dispatch_int2 nF pkt0→ s1"
  using forwardingpath_auth 
  by(auto dest!: e1.dp2_dispatch_int_also_works_for_honest[where ?m = pkt0])
    (auto simp add: e1.dp2_def e1.dp2_defs e1.dp2_msgs forwading_states pkt0_def e1.dp2_init_def)

lemma s1_s2: "e1.dp2: s1 ─evt_send2 nF nE pkt0→ s2"
  by (auto simp add: e1.dp2_def forwading_states e1.dp2_defs e1.dp2_msgs pkt0_def pkt1_def)
     (auto simp add: hfl_defs)

lemma s2_s3: "e1.dp2: s2 ─evt_recv2 nE nF pkt1→ s3"
  by (auto simp add: e1.dp2_def forwading_states e1.dp2_defs e1.dp2_msgs pkt0_def pkt1_def)
     (auto simp add: hfl_defs)

lemma s3_s4: "e1.dp2: s3 ─evt_send2 nE nD pkt1→ s4"
  by (auto simp add: e1.dp2_def forwading_states e1.dp2_defs e1.dp2_msgs pkt1_def pkt2_def)
     (auto simp add: hfl_defs)

lemma s4_s5: "e1.dp2: s4 ─evt_recv2 nD nE pkt2→ s5"
  by (auto simp add: e1.dp2_def forwading_states e1.dp2_defs e1.dp2_msgs pkt1_def pkt2_def)
     (auto simp add: hfl_defs)

lemma s5_s6: "e1.dp2: s5 ─evt_send2 nD nB pkt2→ s6"
  by (auto simp add: e1.dp2_def forwading_states e1.dp2_defs e1.dp2_msgs pkt3_def pkt2_def)
     (auto simp add: hfl_defs)

lemma s6_s7: "e1.dp2: s6 ─evt_recv2 nB nD pkt3→ s7"
  by (auto simp add: e1.dp2_def forwading_states e1.dp2_defs e1.dp2_msgs pkt3_def pkt2_def)
     (auto simp add: hfl_defs)

lemma s7_s8: "e1.dp2: s7 ─evt_send2 nB nA pkt3→ s8"
  by (auto simp add: e1.dp2_def forwading_states e1.dp2_defs e1.dp2_msgs pkt4_def pkt3_def)
     (auto simp add: hfl_defs)

lemma s8_s9: "e1.dp2: s8 ─evt_recv2 nA nB pkt4→ s9"
  by (auto simp add: e1.dp2_def forwading_states e1.dp2_defs e1.dp2_msgs pkt4_def pkt3_def)
     (auto simp add: hfl_defs)

lemma s9_s10: "e1.dp2: s9 ─evt_deliver2 nA pkt4→ s10"
  by (auto simp add: e1.dp2_def forwading_states e1.dp2_defs e1.dp2_msgs pkt5_def pkt4_def)
     (auto simp add: hfl_defs)

text‹The state in which the packet is received is reachable›
lemma executability: "reach e1.dp2 s10"
  using reach_s0 s0_s1 s1_s2 s2_s3 s3_s4 s4_s5 s5_s6 s6_s7 s7_s8 s8_s9 s9_s10 
  by(auto elim!: reach_trans)

subsubsection‹Attacker event executability›
text‹We also show that the attacker event can be executed.›

definition pkt_attr where "pkt_attr ≡ ⦇
                AInfo = ainfo,
                UInfo = uinfo,
                past = [],
                future = [hfEl],
                history = []
              ⦈"

definition s_attr where 
  "s_attr ≡ s0⦇chan2 := (chan2 s0)((nF, nE, nE, nF) := chan2 s0 (nF, nE, nE, nF) ∪ {pkt_attr})⦈"

lemma ik_hfs_in_ik: "t ∈ e1.ik_hfs ⟹ t ∈ synth (analz (e1.ik_dyn s))"
  by(auto simp add: e1.ik_dyn_def e1.ik_def)

lemma hvf_e_auth: "HVF hfEl ∈ e1.ik_hfs"
  apply(auto simp add: e1.ik_hfs_def e1.auth_seg2_def
               intro!: exI[of _ hfEl] exI[of _ "[hfFl, hfEl, hfDl, hfBl, hfAl]"] exI[of _ ainfo])
  using e1.hfs_valid_prefix_generic_def no_assumptions_left.forwardingpath_valid
  by(auto intro!: exI[of _ uinfo] simp add: auth_seg0_def leftsegment_wormholed_def hfl_defs)

lemma uhi_e_auth: "UHI hfEl ∈ e1.ik_hfs"
  apply(auto simp add: e1.ik_hfs_def e1.auth_seg2_def
               intro!: exI[of _ hfEl] exI[of _ "[hfFl, hfEl, hfDl, hfBl, hfAl]"] exI[of _ ainfo])
  using e1.hfs_valid_prefix_generic_def no_assumptions_left.forwardingpath_valid
  by(auto simp add: e1.auth_seg2_def auth_seg0_def leftsegment_wormholed_def hfl_defs)

text‹The attacker can also execute her event.›
lemma attr_executability: "reach e1.dp2 s_attr"
proof- 
  have "e1.dp2: s0 ─evt_dispatch_ext2 nF nE pkt_attr→ s_attr"
    apply (auto simp add: forwading_states e1.dp2_defs e1.dp2_msgs pkt_attr_def e1.ik_hfs_def e1.terms_pkt_def)
    using hvf_e_auth uhi_e_auth 
    by(auto dest: ik_hfs_in_ik simp add: s_attr_def s0_def e1.dp2_init_def pkt_attr_def)
  then show ?thesis using reach_s0 by auto
qed

end
end