Theory Network_Model

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

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

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

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

chapter‹Abstract, and Concrete Parametrized Models›
text‹This is the core of our verification -- the abstract and parametrized models that cover a wide
range of protocols.›
section‹Network model›
theory Network_Model
  imports
    "infrastructure/Agents"
    "infrastructure/Tools"
    "infrastructure/Take_While"
begin

text‹@{term "as"} is already defined as a type synonym for nat.›
type_synonym ifs = nat

text‹The authenticated hop information consists of the interface identifiers UpIF, DownIF and an
identifier of the AS to which the hop information belongs. Furthermore, this record is extensible 
and can include additional authenticated hop information (aahi).›
record ahi = 
  UpIF :: "ifs option"
  DownIF :: "ifs option"
  ASID :: as

type_synonym 'aahi ahis = "'aahi ahi_scheme"

locale network_model = compromised + 
  fixes
   auth_seg0 :: "('ainfo × 'aahi ahi_scheme list) set" 
   and tgtas :: "as ⇒ ifs ⇒ as option"
   and tgtif :: "as ⇒ ifs ⇒ ifs option"
begin

subsection ‹Interface check›
(******************************************************************************)

text ‹Check if the interfaces of two adjacent hop fields match. If both hops are compromised we also
interpret the link as valid.›
fun if_valid :: "'aahi ahis option ⇒ 'aahi ahis => 'aahi ahis option ⇒ bool" where
  "if_valid None hf _ ― ‹this is the case for the leaf AS›
    = True"
| "if_valid (Some hf1) (hf2) _
    = ((∃downif . DownIF hf2 = Some downif ∧ 
        tgtas (ASID hf2) downif = Some (ASID hf1) ∧
        tgtif (ASID hf2) downif = UpIF hf1)
      ∨ ASID hf1 ∈ bad ∧ ASID hf2 ∈ bad)"

text ‹makes sure that: the segment is terminated, i.e. the first AS's HF has Eo = None›
fun terminated :: "'aahi ahis list ⇒ bool" where
  "terminated (hf#xs) ⟷ DownIF hf = None ∨ ASID hf ∈ bad"
| "terminated [] = True" (* we allow this as a special case*)

text ‹makes sure that: the segment is rooted, i.e. the last HF has UpIF = None›
fun rooted :: "'aahi ahis list ⇒ bool" where
  "rooted [hf] ⟷ UpIF hf = None ∨ ASID hf ∈ bad"
| "rooted (hf#xs) = rooted xs"
| "rooted [] = True" (* we allow this as a special case*)

abbreviation ifs_valid where 
  "ifs_valid pre l nxt ≡ TW.holds if_valid pre l nxt"

abbreviation ifs_valid_prefix where 
  "ifs_valid_prefix pre l nxt ≡ TW.takeW if_valid pre l nxt"

abbreviation ifs_valid_None where 
  "ifs_valid_None l ≡ ifs_valid None l None"

abbreviation ifs_valid_None_prefix where 
  "ifs_valid_None_prefix l ≡ ifs_valid_prefix None l None"

lemma strip_ifs_valid_prefix:
  "pfragment ainfo l auth_seg0 ⟹ pfragment ainfo (ifs_valid_prefix pre l nxt) auth_seg0"
  by (auto elim: pfragment_prefix' intro: TW.takeW_prefix)


text‹Given the AS and an interface identifier of a channel, obtain the AS and interface at the other
end of the same channel.›
abbreviation rev_link :: "as ⇒ ifs ⇒ as option × ifs option" where 
  "rev_link a1 i1 ≡ (tgtas a1 i1, tgtif a1 i1)"

end
end