Theory NonInterferenceIntra

header {* \isaheader{Slicing guarantees IFC Noninterference} *}

theory NonInterferenceIntra imports 
  "../Slicing/StaticIntra/Slice" 
  "../Slicing/Basic/CFGExit_wf"
begin

section {* Assumptions of this Approach *}

text {*
Classical IFC noninterference, a special case of a noninterference
definition using partial equivalence relations (per)
\cite{SabelfeldS:01}, partitions the variables (i.e.\ locations) into
security levels. Usually, only levels for secret or high, written
@{text H}, and public or low, written @{text L}, variables are
used. Basically, a program that is noninterferent has to fulfil one
basic property: executing the program in two different initial states
that may differ in the values of their @{text H}-variables yields two
final states that again only differ in the values of their 
@{text H}-variables; thus the values of the @{text H}-variables did not
influence those of the @{text L}-variables.

Every per-based approach makes certain
assumptions: (i) all \mbox{@{text H}-variables} are defined at the
beginning of the program, (ii) all @{text L}-variables are observed (or
used in our terms) at the end and (iii) every variable is either
@{text H} or @{text L}. This security label is fixed for a variable
and can not be altered during a program run. Thus, we have to extend 
the prerequisites of the slicing framework in \cite{Wasserrab:08} accordingly
in a new locale:

*}

locale NonInterferenceIntraGraph = 
  BackwardSlice sourcenode targetnode kind valid_edge Entry Def Use state_val 
  backward_slice +
  CFGExit_wf sourcenode targetnode kind valid_edge Entry Def Use state_val Exit
  for sourcenode :: "'edge => 'node" and targetnode :: "'edge => 'node"
  and kind :: "'edge => 'state edge_kind" and valid_edge :: "'edge => bool"
  and Entry :: "'node" ("'('_Entry'_')") and Def :: "'node => 'var set"
  and Use :: "'node => 'var set" and state_val :: "'state => 'var => 'val"
  and backward_slice :: "'node set => 'node set" 
  and Exit :: "'node" ("'('_Exit'_')") +
  fixes H :: "'var set"
  fixes L :: "'var set"
  fixes High :: "'node"  ("'('_High'_')")
  fixes Low :: "'node"   ("'('_Low'_')")
  assumes Entry_edge_Exit_or_High:
  "[|valid_edge a; sourcenode a = (_Entry_)|] 
    ==> targetnode a = (_Exit_) ∨ targetnode a = (_High_)"
  and High_target_Entry_edge:
  "∃a. valid_edge a ∧ sourcenode a = (_Entry_) ∧ targetnode a = (_High_) ∧
       kind a = (λs. True)⇣\<surd>"
  and Entry_predecessor_of_High:
  "[|valid_edge a; targetnode a = (_High_)|] ==> sourcenode a = (_Entry_)"
  and Exit_edge_Entry_or_Low: "[|valid_edge a; targetnode a = (_Exit_)|] 
    ==> sourcenode a = (_Entry_) ∨ sourcenode a = (_Low_)"
  and Low_source_Exit_edge:
  "∃a. valid_edge a ∧ sourcenode a = (_Low_) ∧ targetnode a = (_Exit_) ∧ 
       kind a = (λs. True)⇣\<surd>"
  and Exit_successor_of_Low:
  "[|valid_edge a; sourcenode a = (_Low_)|] ==> targetnode a = (_Exit_)"
  and DefHigh: "Def (_High_) = H" 
  and UseHigh: "Use (_High_) = H"
  and UseLow: "Use (_Low_) = L"
  and HighLowDistinct: "H ∩ L = {}"
  and HighLowUNIV: "H ∪ L = UNIV"

begin

lemma Low_neq_Exit: assumes "L ≠ {}" shows "(_Low_) ≠ (_Exit_)"
proof
  assume "(_Low_) = (_Exit_)"
  have "Use (_Exit_) = {}" by fastforce
  with UseLow `L ≠ {}` `(_Low_) = (_Exit_)` show False by simp
qed

lemma Entry_path_High_path:
  assumes "(_Entry_) -as->* n" and "inner_node n"
  obtains a' as' where "as = a'#as'" and "(_High_) -as'->* n" 
  and "kind a' = (λs. True)⇣\<surd>"
proof(atomize_elim)
  from `(_Entry_) -as->* n` `inner_node n`
  show "∃a' as'. as = a'#as' ∧ (_High_) -as'->* n ∧ kind a' = (λs. True)⇣\<surd>"
  proof(induct n'≡"(_Entry_)" as n rule:path.induct)
    case (Cons_path n'' as n' a)
    from `n'' -as->* n'` `inner_node n'` have "n'' ≠ (_Exit_)" 
      by(fastforce simp:inner_node_def)
    with `valid_edge a` `targetnode a = n''` `sourcenode a = (_Entry_)`
    have "n'' = (_High_)" by -(drule Entry_edge_Exit_or_High,auto)
    from High_target_Entry_edge
    obtain a' where "valid_edge a'" and "sourcenode a' = (_Entry_)"
      and "targetnode a' = (_High_)" and "kind a' = (λs. True)⇣\<surd>"
      by blast
    with `valid_edge a` `sourcenode a = (_Entry_)` `targetnode a = n''`
      `n'' = (_High_)`
    have "a = a'" by(auto dest:edge_det)
    with `n'' -as->* n'` `n'' = (_High_)` `kind a' = (λs. True)⇣\<surd>` show ?case by blast
  qed fastforce
qed



lemma Exit_path_Low_path:
  assumes "n -as->* (_Exit_)" and "inner_node n"
  obtains a' as' where "as = as'@[a']" and "n -as'->* (_Low_)"
  and "kind a' = (λs. True)⇣\<surd>"
proof(atomize_elim)
  from `n -as->* (_Exit_)`
  show "∃as' a'. as = as'@[a'] ∧ n -as'->* (_Low_) ∧ kind a' = (λs. True)⇣\<surd>"
  proof(induct as rule:rev_induct)
    case Nil
    with `inner_node n` show ?case by fastforce
  next
    case (snoc a' as')
    from `n -as'@[a']->* (_Exit_)`
    have "n -as'->* sourcenode a'" and "valid_edge a'" and "targetnode a' = (_Exit_)"
      by(auto elim:path_split_snoc)
    { assume "sourcenode a' = (_Entry_)"
      with `n -as'->* sourcenode a'` have "n = (_Entry_)"
        by(blast intro!:path_Entry_target)
      with `inner_node n` have False by(simp add:inner_node_def) }
    with `valid_edge a'` `targetnode a' = (_Exit_)` have "sourcenode a' = (_Low_)"
      by(blast dest!:Exit_edge_Entry_or_Low)
    from Low_source_Exit_edge
    obtain ax where "valid_edge ax" and "sourcenode ax = (_Low_)"
      and "targetnode ax = (_Exit_)" and "kind ax = (λs. True)⇣\<surd>"
      by blast
    with `valid_edge a'` `targetnode a' = (_Exit_)` `sourcenode a' = (_Low_)`
    have "a' = ax" by(fastforce intro:edge_det)
    with `n -as'->* sourcenode a'` `sourcenode a' = (_Low_)` `kind ax = (λs. True)⇣\<surd>`
    show ?case by blast
  qed
qed


lemma not_Low_High: "V ∉ L ==> V ∈ H"
  using HighLowUNIV
  by fastforce

lemma not_High_Low: "V ∉ H ==> V ∈ L"
  using HighLowUNIV
  by fastforce


section {* Low Equivalence *}

text {*
In classical noninterference, an external observer can only see public values,
in our case the @{text L}-variables. If two states agree in the values of all 
@{text L}-variables, these states are indistinguishable for him. 
\emph{Low equivalence} groups those states in an equivalence class using 
the relation @{text "≈⇣L"}:
*}

definition lowEquivalence :: "'state => 'state => bool" (infixl "≈⇣L" 50)
  where "s ≈⇣L s' ≡ ∀V ∈ L. state_val s V = state_val s' V"

text {* The following lemmas connect low equivalent states with
relevant variables as necessary in the correctness proof for slicing. *}

lemma relevant_vars_Entry:
  assumes "V ∈ rv S (_Entry_)" and "(_High_) ∉ backward_slice S"
  shows "V ∈ L"
proof -
  from `V ∈ rv S (_Entry_)` obtain as n' where "(_Entry_) -as->* n'"
    and "n' ∈ backward_slice S" and "V ∈ Use n'"
    and "∀nx ∈ set(sourcenodes as). V ∉ Def nx" by(erule rvE)
  from `(_Entry_) -as->* n'` have "valid_node n'" by(rule path_valid_node)
  thus ?thesis
  proof(cases n' rule:valid_node_cases)
    case Entry
    with `V ∈ Use n'` have False by(simp add:Entry_empty)
    thus ?thesis by simp
  next
    case Exit
    with `V ∈ Use n'` have False by(simp add:Exit_empty)
    thus ?thesis by simp
  next
    case inner
    with `(_Entry_) -as->* n'` obtain a' as' where "as = a'#as'"
      and "(_High_) -as'->* n'" by -(erule Entry_path_High_path)
    from `(_Entry_) -as->* n'` `as = a'#as'`
    have "sourcenode a' = (_Entry_)" by(fastforce elim:path.cases)
    show ?thesis
    proof(cases "as' = []")
      case True
      with `(_High_) -as'->* n'` have "n' = (_High_)" by fastforce
      with `n' ∈ backward_slice S` `(_High_) ∉ backward_slice S`
      have False by simp
      thus ?thesis by simp
    next
      case False
      with `(_High_) -as'->* n'` have "hd (sourcenodes as') = (_High_)"
        by(rule path_sourcenode)
      from False have "hd (sourcenodes as') ∈ set (sourcenodes as')"
        by(fastforce intro:hd_in_set simp:sourcenodes_def)
      with `as = a'#as'` have "hd (sourcenodes as') ∈ set (sourcenodes as)"
        by(simp add:sourcenodes_def)
      with `hd (sourcenodes as') = (_High_)` `∀nx ∈ set(sourcenodes as). V ∉ Def nx`
      have "V ∉ Def (_High_)" by fastforce
      hence "V ∉ H" by(simp add:DefHigh)
      thus ?thesis by(rule not_High_Low)
    qed
  qed
qed



lemma lowEquivalence_relevant_nodes_Entry:
  assumes "s ≈⇣L s'" and "(_High_) ∉ backward_slice S"
  shows "∀V ∈ rv S (_Entry_). state_val s V = state_val s' V"
proof
  fix V assume "V ∈ rv S (_Entry_)"
  with `(_High_) ∉ backward_slice S` have "V ∈ L" by -(rule relevant_vars_Entry)
  with `s ≈⇣L s'` show "state_val s V = state_val s' V" by(simp add:lowEquivalence_def)
qed



lemma rv_Low_Use_Low:
  assumes "(_Low_) ∈ S"
  shows "[|n -as->* (_Low_); n -as'->* (_Low_);
    ∀V ∈ rv S n. state_val s V = state_val s' V;
    preds (slice_kinds S as) s; preds (slice_kinds S as') s'|]
  ==> ∀V ∈ Use (_Low_). state_val (transfers (slice_kinds S as) s) V =
                       state_val (transfers (slice_kinds S as') s') V"
proof(induct n as n≡"(_Low_)" arbitrary:as' s s' rule:path.induct)
  case empty_path
  { fix V assume "V ∈ Use (_Low_)"
    moreover
    from `valid_node (_Low_)` have "(_Low_) -[]->* (_Low_)"
      by(fastforce intro:path.empty_path)
    moreover
    from `valid_node (_Low_)` `(_Low_) ∈ S` have "(_Low_) ∈ backward_slice S"
      by(fastforce intro:refl)
    ultimately have "V ∈ rv S (_Low_)"
      by(fastforce intro:rvI simp:sourcenodes_def) }
  hence "∀V ∈ Use (_Low_). V ∈ rv S (_Low_)" by simp
  show ?case
  proof(cases "L = {}")
    case True with UseLow show ?thesis by simp
  next
    case False
    from `(_Low_) -as'->* (_Low_)` have "as' = []"
    proof(induct n≡"(_Low_)" as' n'≡"(_Low_)" rule:path.induct)
      case (Cons_path n'' as a)
      from `valid_edge a` `sourcenode a = (_Low_)`
      have "targetnode a = (_Exit_)" by -(rule Exit_successor_of_Low,simp+)
      with `targetnode a = n''` `n'' -as->* (_Low_)`
      have "(_Low_) = (_Exit_)" by -(rule path_Exit_source,fastforce)
      with False have False by -(drule Low_neq_Exit,simp)
      thus ?case by simp
    qed simp
    with `∀V ∈ Use (_Low_). V ∈ rv S (_Low_)` 
      `∀V∈rv S (_Low_). state_val s V = state_val s' V`
    show ?thesis by(auto simp:slice_kinds_def)
  qed
next
  case (Cons_path n'' as a n)
  note IH = `!!as' s s'. [|n'' -as'->* (_Low_);
    ∀V∈rv S n''. state_val s V = state_val s' V;
   preds (slice_kinds S as) s; preds (slice_kinds S as') s'|]
  ==> ∀V∈Use (_Low_). state_val (transfers (slice_kinds S as) s) V =
                     state_val (transfers (slice_kinds S as') s') V`
  show ?case
  proof(cases "L = {}")
    case True with UseLow show ?thesis by simp
  next
    case False
    show ?thesis
    proof(cases as')
      case Nil
      with `n -as'->* (_Low_)` have "n = (_Low_)" by fastforce
      with `valid_edge a` `sourcenode a = n` have "targetnode a = (_Exit_)"
        by -(rule Exit_successor_of_Low,simp+)
      from Low_source_Exit_edge obtain ax where "valid_edge ax"
        and "sourcenode ax = (_Low_)" and "targetnode ax = (_Exit_)"
        and "kind ax = (λs. True)⇣\<surd>" by blast
      from `valid_edge a` `sourcenode a = n` `n = (_Low_)` `targetnode a = (_Exit_)`
        `valid_edge ax` `sourcenode ax = (_Low_)` `targetnode ax = (_Exit_)`
      have "a = ax" by(fastforce dest:edge_det)
      with `kind ax = (λs. True)⇣\<surd>` have "kind a = (λs. True)⇣\<surd>" by simp
      with `targetnode a = (_Exit_)` `targetnode a = n''` `n'' -as->* (_Low_)`
      have "(_Low_) = (_Exit_)" by -(rule path_Exit_source,auto)
      with False have False by -(drule Low_neq_Exit,simp)
      thus ?thesis by simp
    next
      case (Cons ax asx)
      with `n -as'->* (_Low_)` have "n = sourcenode ax" and "valid_edge ax" 
        and "targetnode ax -asx->* (_Low_)" by(auto elim:path_split_Cons)
      show ?thesis
      proof(cases "targetnode ax = n''")
        case True
        with `targetnode ax -asx->* (_Low_)` have "n'' -asx->* (_Low_)" by simp
        from `valid_edge ax` `valid_edge a` `n = sourcenode ax` `sourcenode a = n`
          True `targetnode a = n''` have "ax = a" by(fastforce intro:edge_det)
        from `preds (slice_kinds S (a#as)) s` 
        have preds1:"preds (slice_kinds S as) (transfer (slice_kind S a) s)"
          by(simp add:slice_kinds_def)
        from `preds (slice_kinds S as') s'` Cons `ax = a`
        have preds2:"preds (slice_kinds S asx) 
          (transfer (slice_kind S a) s')"
          by(simp add:slice_kinds_def)
        from `valid_edge a` `sourcenode a = n` `targetnode a = n''`
          `preds (slice_kinds S (a#as)) s` `preds (slice_kinds S as') s'`
          `ax = a` Cons `∀V∈rv S n. state_val s V = state_val s' V`
        have "∀V∈rv S n''. state_val (transfer (slice_kind S a) s) V =
                                 state_val (transfer (slice_kind S a) s') V"
          by -(rule rv_edge_slice_kinds,auto)
        from IH[OF `n'' -asx->* (_Low_)` this preds1 preds2] 
          Cons `ax = a` show ?thesis by(simp add:slice_kinds_def)
      next
        case False
        with `valid_edge a` `valid_edge ax` `sourcenode a = n` `n = sourcenode ax`
          `targetnode a = n''` `preds (slice_kinds S (a#as)) s`
          `preds (slice_kinds S as') s'` Cons
          `∀V∈rv S n. state_val s V = state_val s' V`
        have False by -(rule rv_branching_edges_slice_kinds_False,auto)
        thus ?thesis by simp
      qed
    qed
  qed
qed


section {* The Correctness Proofs *}

text {*
In the following, we present two correctness proofs that slicing guarantees
IFC noninterference. In both theorems, 
@{text "(_High_) ∉ backward_slice S"}, where @{text "(_Low_) ∈ S"},
makes sure that no high variable (which are all defined in @{text "(_High_)"}) 
can influence a low variable (which are all used in @{text "(_Low_)"}).

First, a theorem regarding 
@{text "(_Entry_) -as->* (_Exit_)"} paths in the control flow graph (CFG),
which agree to a complete program execution: *}

lemma nonInterference_path_to_Low:
  assumes "s ≈⇣L s'" and "(_High_) ∉ backward_slice S" and "(_Low_) ∈ S"
  and "(_Entry_) -as->* (_Low_)" and "preds (kinds as) s"
  and "(_Entry_) -as'->* (_Low_)" and "preds (kinds as') s'"
  shows "transfers (kinds as) s ≈⇣L transfers (kinds as') s'"
proof -
  from `(_Entry_) -as->* (_Low_)` `preds (kinds as) s` `(_Low_) ∈ S`
  obtain asx where "preds (slice_kinds S asx) s"
    and "∀V ∈ Use (_Low_). state_val(transfers (slice_kinds S asx) s) V = 
                           state_val(transfers (kinds as) s) V"
    and "slice_edges S as = slice_edges S asx"
    and "(_Entry_) -asx->* (_Low_)" by(erule fundamental_property_of_static_slicing)
  from `(_Entry_) -as'->* (_Low_)` `preds (kinds as') s'` `(_Low_) ∈ S`
  obtain asx' where "preds (slice_kinds S asx') s'"
    and "∀V ∈ Use (_Low_). state_val (transfers (slice_kinds S asx') s') V = 
                           state_val (transfers (kinds as') s') V"
    and "slice_edges S as' = slice_edges S asx'"
    and "(_Entry_) -asx'->* (_Low_)" by(erule fundamental_property_of_static_slicing)
  from `s ≈⇣L s'` `(_High_) ∉ backward_slice S`
  have "∀V ∈ rv S (_Entry_). state_val s V = state_val s' V" 
    by(rule lowEquivalence_relevant_nodes_Entry)
  with `(_Entry_) -asx->* (_Low_)` `(_Entry_) -asx'->* (_Low_)` `(_Low_) ∈ S`
    `preds (slice_kinds S asx) s` `preds (slice_kinds S asx') s'`
  have "∀V ∈ Use (_Low_). state_val (transfers (slice_kinds S asx) s) V =
                          state_val (transfers (slice_kinds S asx') s') V"
    by -(rule rv_Low_Use_Low,auto)
  with `∀V ∈ Use (_Low_). state_val(transfers (slice_kinds S asx) s) V = 
                          state_val(transfers (kinds as) s) V`
    `∀V ∈ Use (_Low_). state_val (transfers (slice_kinds S asx') s') V = 
                       state_val (transfers (kinds as') s') V`
  show ?thesis by(auto simp:lowEquivalence_def UseLow)
qed


theorem nonInterference_path:
  assumes "s ≈⇣L s'" and "(_High_) ∉ backward_slice S" and "(_Low_) ∈ S"
  and "(_Entry_) -as->* (_Exit_)" and "preds (kinds as) s"
  and "(_Entry_) -as'->* (_Exit_)" and "preds (kinds as') s'"
  shows "transfers (kinds as) s ≈⇣L transfers (kinds as') s'"
proof -
  from `(_Entry_) -as->* (_Exit_)` obtain x xs where "as = x#xs"
    and "(_Entry_) = sourcenode x" and "valid_edge x" 
    and "targetnode x -xs->* (_Exit_)"
    apply(cases "as = []")
     apply(simp,drule empty_path_nodes,drule Entry_noteq_Exit,simp)
    by(erule path_split_Cons)
  from `valid_edge x` have "valid_node (targetnode x)" by simp
  hence "inner_node (targetnode x)"
  proof(cases rule:valid_node_cases)
    case Entry
    with `valid_edge x` have False by(rule Entry_target)
    thus ?thesis by simp
  next
    case Exit
    with `targetnode x -xs->* (_Exit_)` have "xs = []"
      by -(rule path_Exit_source,simp)
    from Entry_Exit_edge obtain z where "valid_edge z"
      and "sourcenode z = (_Entry_)" and "targetnode z = (_Exit_)"
      and "kind z = (λs. False)⇣\<surd>" by blast
    from `valid_edge x` `valid_edge z` `(_Entry_) = sourcenode x` 
      `sourcenode z = (_Entry_)` Exit `targetnode z = (_Exit_)`
    have "x = z" by(fastforce intro:edge_det)
    with `preds (kinds as) s` `as = x#xs` `xs = []` `kind z = (λs. False)⇣\<surd>` 
    have False by(simp add:kinds_def)
    thus ?thesis by simp
  qed simp
  with `targetnode x -xs->* (_Exit_)` obtain x' xs' where "xs = xs'@[x']"
    and "targetnode x -xs'->* (_Low_)" and "kind x' = (λs. True)⇣\<surd>"
    by(fastforce elim:Exit_path_Low_path)
  with `(_Entry_) = sourcenode x` `valid_edge x`
  have "(_Entry_) -x#xs'->* (_Low_)" by(fastforce intro:Cons_path)
  from `as = x#xs` `xs = xs'@[x']` have "as = (x#xs')@[x']" by simp
  with `preds (kinds as) s` have "preds (kinds (x#xs')) s"
    by(simp add:kinds_def preds_split)
  from `(_Entry_) -as'->* (_Exit_)` obtain y ys where "as' = y#ys"
    and "(_Entry_) = sourcenode y" and "valid_edge y" 
    and "targetnode y -ys->* (_Exit_)"
    apply(cases "as' = []")
     apply(simp,drule empty_path_nodes,drule Entry_noteq_Exit,simp)
    by(erule path_split_Cons)
  from `valid_edge y` have "valid_node (targetnode y)" by simp
  hence "inner_node (targetnode y)"
  proof(cases rule:valid_node_cases)
    case Entry
    with `valid_edge y` have False by(rule Entry_target)
    thus ?thesis by simp
  next
    case Exit
    with `targetnode y -ys->* (_Exit_)` have "ys = []"
      by -(rule path_Exit_source,simp)
    from Entry_Exit_edge obtain z where "valid_edge z"
      and "sourcenode z = (_Entry_)" and "targetnode z = (_Exit_)"
      and "kind z = (λs. False)⇣\<surd>" by blast
    from `valid_edge y` `valid_edge z` `(_Entry_) = sourcenode y` 
      `sourcenode z = (_Entry_)` Exit `targetnode z = (_Exit_)`
    have "y = z" by(fastforce intro:edge_det)
    with `preds (kinds as') s'` `as' = y#ys` `ys = []` `kind z = (λs. False)⇣\<surd>` 
    have False by(simp add:kinds_def)
    thus ?thesis by simp
  qed simp
  with `targetnode y -ys->* (_Exit_)` obtain y' ys' where "ys = ys'@[y']"
    and "targetnode y -ys'->* (_Low_)" and "kind y' = (λs. True)⇣\<surd>"
    by(fastforce elim:Exit_path_Low_path)
  with `(_Entry_) = sourcenode y` `valid_edge y`
  have "(_Entry_) -y#ys'->* (_Low_)" by(fastforce intro:Cons_path)
  from `as' = y#ys` `ys = ys'@[y']` have "as' = (y#ys')@[y']" by simp
  with `preds (kinds as') s'` have "preds (kinds (y#ys')) s'"
    by(simp add:kinds_def preds_split)
  from `s ≈⇣L s'` `(_High_) ∉ backward_slice S` `(_Low_) ∈ S`
    `(_Entry_) -x#xs'->* (_Low_)` `preds (kinds (x#xs')) s`
    `(_Entry_) -y#ys'->* (_Low_)` `preds (kinds (y#ys')) s'`
  have "transfers (kinds (x#xs')) s ≈⇣L transfers (kinds (y#ys')) s'"
    by(rule nonInterference_path_to_Low)
  with `as = x#xs` `xs = xs'@[x']` `kind x' = (λs. True)⇣\<surd>`
    `as' = y#ys` `ys = ys'@[y']` `kind y' = (λs. True)⇣\<surd>`
  show ?thesis by(simp add:kinds_def transfers_split)
qed


end

text {* The second theorem assumes that we have a operational semantics,
whose evaluations are written @{text "⟨c,s⟩ => ⟨c',s'⟩"} and which conforms 
to the CFG. The correctness theorem then states that if no high variable
influenced a low variable and the initial states were low equivalent, the
reulting states are again low equivalent: *}


locale NonInterferenceIntra = 
  NonInterferenceIntraGraph sourcenode targetnode kind valid_edge Entry 
    Def Use state_val backward_slice Exit H L High Low +
  BackwardSlice_wf sourcenode targetnode kind valid_edge Entry Def Use state_val 
    backward_slice sem identifies
  for sourcenode :: "'edge => 'node" and targetnode :: "'edge => 'node"
  and kind :: "'edge => 'state edge_kind" and valid_edge :: "'edge => bool"
  and Entry :: "'node" ("'('_Entry'_')") and Def :: "'node => 'var set"
  and Use :: "'node => 'var set" and state_val :: "'state => 'var => 'val"
  and backward_slice :: "'node set => 'node set"
  and sem :: "'com => 'state => 'com => 'state => bool" 
    ("((1⟨_,/_⟩) =>/ (1⟨_,/_⟩))" [0,0,0,0] 81)
  and identifies :: "'node => 'com => bool" ("_ \<triangleq> _" [51, 0] 80)
  and Exit :: "'node" ("'('_Exit'_')")
  and H :: "'var set" and L :: "'var set" 
  and High :: "'node"  ("'('_High'_')") and Low :: "'node"   ("'('_Low'_')") +
  fixes final :: "'com => bool"
  assumes final_edge_Low: "[|final c; n \<triangleq> c|] 
  ==> ∃a. valid_edge a ∧ sourcenode a = n ∧ targetnode a = (_Low_) ∧ kind a = \<Up>id"
begin

text{* The following theorem needs the explicit edge from @{text "(_High_)"}
  to @{text n}. An approach using a @{text "init"} predicate for initial statements,
  being reachable from @{text "(_High_)"} via a @{text "(λs. True)⇣\<surd>"} edge,
  does not work as the same statement could be identified by several nodes, some
  initial, some not. E.g., in the program \texttt{while (True) Skip;;Skip}
  two nodes identify this inital statement: the initial node and the node
  within the loop (because of loop unrolling).*}

theorem nonInterference:
  assumes "s⇣1 ≈⇣L s⇣2" and "(_High_) ∉ backward_slice S" and "(_Low_) ∈ S"
  and "valid_edge a" and "sourcenode a = (_High_)" and "targetnode a = n" 
  and "kind a = (λs. True)⇣\<surd>" and "n \<triangleq> c" and "final c'"
  and "⟨c,s⇣1⟩ => ⟨c',s⇣1'⟩" and "⟨c,s⇣2⟩ => ⟨c',s⇣2'⟩"
  shows "s⇣1' ≈⇣L s⇣2'"
proof -
  from High_target_Entry_edge obtain ax where "valid_edge ax"
    and "sourcenode ax = (_Entry_)" and "targetnode ax = (_High_)"
    and "kind ax = (λs. True)⇣\<surd>" by blast
  from `n \<triangleq> c` `⟨c,s⇣1⟩ => ⟨c',s⇣1'⟩`
  obtain n⇣1 as⇣1 where "n -as⇣1->* n⇣1" and "transfers (kinds as⇣1) s⇣1 = s⇣1'"
    and "preds (kinds as⇣1) s⇣1" and "n⇣1 \<triangleq> c'"
    by(fastforce dest:fundamental_property)
  from `n -as⇣1->* n⇣1` `valid_edge a` `sourcenode a = (_High_)` `targetnode a = n`
  have "(_High_) -a#as⇣1->* n⇣1" by(rule Cons_path)
  from `final c'` `n⇣1 \<triangleq> c'`
  obtain a⇣1 where "valid_edge a⇣1" and "sourcenode a⇣1 = n⇣1" 
    and "targetnode a⇣1 = (_Low_)" and "kind a⇣1 = \<Up>id" by(fastforce dest:final_edge_Low)
  hence "n⇣1 -[a⇣1]->* (_Low_)" by(fastforce intro:path_edge)
  with `(_High_) -a#as⇣1->* n⇣1` have "(_High_) -(a#as⇣1)@[a⇣1]->* (_Low_)"
    by(rule path_Append)
  with `valid_edge ax` `sourcenode ax = (_Entry_)` `targetnode ax = (_High_)`
  have "(_Entry_) -ax#((a#as⇣1)@[a⇣1])->* (_Low_)" by -(rule Cons_path)
  from `kind ax = (λs. True)⇣\<surd>` `kind a = (λs. True)⇣\<surd>` `preds (kinds as⇣1) s⇣1`
    `kind a⇣1 = \<Up>id` have "preds (kinds (ax#((a#as⇣1)@[a⇣1]))) s⇣1"
    by (simp add:kinds_def preds_split)
  from `n \<triangleq> c` `⟨c,s⇣2⟩ => ⟨c',s⇣2'⟩`
  obtain n⇣2 as⇣2 where "n -as⇣2->* n⇣2" and "transfers (kinds as⇣2) s⇣2 = s⇣2'"
    and "preds (kinds as⇣2) s⇣2" and "n⇣2 \<triangleq> c'"
    by(fastforce dest:fundamental_property)
  from `n -as⇣2->* n⇣2` `valid_edge a` `sourcenode a = (_High_)` `targetnode a = n`
  have "(_High_) -a#as⇣2->* n⇣2" by(rule Cons_path)
  from `final c'` `n⇣2 \<triangleq> c'`
  obtain a⇣2 where "valid_edge a⇣2" and "sourcenode a⇣2 = n⇣2" 
    and "targetnode a⇣2 = (_Low_)" and "kind a⇣2 = \<Up>id" by(fastforce dest:final_edge_Low)
  hence "n⇣2 -[a⇣2]->* (_Low_)" by(fastforce intro:path_edge)
  with `(_High_) -a#as⇣2->* n⇣2` have "(_High_) -(a#as⇣2)@[a⇣2]->* (_Low_)"
    by(rule path_Append)
  with `valid_edge ax` `sourcenode ax = (_Entry_)` `targetnode ax = (_High_)`
  have "(_Entry_) -ax#((a#as⇣2)@[a⇣2])->* (_Low_)" by -(rule Cons_path)
  from `kind ax = (λs. True)⇣\<surd>` `kind a = (λs. True)⇣\<surd>` `preds (kinds as⇣2) s⇣2`
    `kind a⇣2 = \<Up>id` have "preds (kinds (ax#((a#as⇣2)@[a⇣2]))) s⇣2"
    by (simp add:kinds_def preds_split)
  from `s⇣1 ≈⇣L s⇣2` `(_High_) ∉ backward_slice S` `(_Low_) ∈ S`
    `(_Entry_) -ax#((a#as⇣1)@[a⇣1])->* (_Low_)` `preds (kinds (ax#((a#as⇣1)@[a⇣1]))) s⇣1`
    `(_Entry_) -ax#((a#as⇣2)@[a⇣2])->* (_Low_)` `preds (kinds (ax#((a#as⇣2)@[a⇣2]))) s⇣2`
  have "transfers (kinds (ax#((a#as⇣1)@[a⇣1]))) s⇣1 ≈⇣L 
        transfers (kinds (ax#((a#as⇣2)@[a⇣2]))) s⇣2"
    by(rule nonInterference_path_to_Low)
  with `kind ax = (λs. True)⇣\<surd>` `kind a = (λs. True)⇣\<surd>` `kind a⇣1 = \<Up>id` `kind a⇣2 = \<Up>id`
    `transfers (kinds as⇣1) s⇣1 = s⇣1'` `transfers (kinds as⇣2) s⇣2 = s⇣2'`
  show ?thesis by(simp add:kinds_def transfers_split)
qed


end

end