Theory ICING_variant2

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