theory SLE66 imports ISM_package  --{* we build on the general ISM definitions *}
begin
ML {* Pretty.setmargin 169; quick_and_dirty:=false *}
use_thy "../awe-0.4/Extensions/AWE"
typedecl fn               --{* function name *}
typedecl dn               --{* data object name *}
datatype on = F fn | D dn --{* object name *}
consts
  f_SN   :: "fn"      --{* the name of the function giving the serial number *}
  FTest0 :: "fn set"  --{* the names of test functions of phase 0 *}
  FTest1 :: "fn set"  --{* the names of test functions of phase 1 *}
  FTest  :: "fn set"  --{* the names of all test functions *}
  F_Sec  :: "fn set"  --{* the names of all security-relevant functions *}
  F_PSec :: "fn set"  --{* the subset of @{term F_Sec} relevant for the processor *}
  F_ASec :: "fn set"  --{* the names of @{term F_Sec} relevant for applications *}
  F_NSec :: "fn set"  --{* the names of all non-security-relevant functions *}
  D_Sec  :: "dn set"  --{* the names of all security-relevant data objects *}
  D_PSec :: "dn set"  --{* the subset of @{term D_Sec} relevant for the processor *}
  D_ASec :: "dn set"  --{* the names of @{term D_Sec} relevant for applications *}
  D_NSec :: "dn set"  --{* the names of all non-security-relevant data objects *}
    Sec  :: "on set"  --{* the names of all security-relevant objects *}
defs
  FTest_def:  "FTest  \<equiv> FTest0 \<union> FTest1"
  F_ASec_def: "F_ASec \<equiv> F_Sec - F_PSec"
  D_ASec_def: "D_ASec \<equiv> D_Sec - D_PSec"
  F_NSec_def: "F_NSec \<equiv> -F_Sec"
  D_NSec_def: "D_NSec \<equiv> -D_Sec"
  Sec_def: "Sec \<equiv> {F fn |fn. fn \<in> F_Sec} \<union> {D dn |dn. dn \<in> D_Sec}"
axioms 
  f_SN_not_FTest:   "f_SN \<notin> FTest"

lemmas f_SN_not_FTest [simp]
lemma [simp]: "(- FTest0 \<inter> - FTest) = (- FTest)" by (auto simp: FTest_def)
lemma [simp]: "(- FTest1 \<inter> - FTest) = (- FTest)" by (auto simp: FTest_def)

datatype ph = P0 | P1 | P2 | Error

typedecl val --{* data and function values *}
consts SN :: val --{* serial number *}

record chip_data = 
  valF :: "fn \<rightharpoonup> val"
  valD :: "dn \<rightharpoonup> val"

translations "chip_data" \<leftharpoondown> (type) "\<lparr>valF :: fn \<rightharpoonup> val, valD :: dn \<rightharpoonup> val\<rparr>"

constdefs 
  val :: "chip_data \<Rightarrow> on \<rightharpoonup> val"
 "val s on \<equiv> case on of F fn \<Rightarrow> valF s fn  | D dn \<Rightarrow> valD s dn"

types SLE66_state = "ph \<times> chip_data"

translations "SLE66_state" \<leftharpoondown> (type) "ph \<times> chip_data"

constdefs
  fct :: "chip_data \<Rightarrow> fn set"
 "fct s \<equiv> dom (valF s)"

lemma dom_valF_fct [simp]: "f \<in> dom (valF s) = (f \<in> fct s)"
by (auto simp: fct_def)

lemma fct_upd_valF [simp]: "fct (s\<lparr>valF := f\<rparr>) = dom f" 
by(auto simp: fct_def)

consts
 "output"   :: "fn \<Rightarrow> chip_data \<Rightarrow> val"
 "change"   :: "fn \<Rightarrow> chip_data \<Rightarrow> chip_data"  
 "positive" :: "val \<Rightarrow> bool" 

datatype interface = In | Out

typedecl sb      (* --{* subjects *}*)
consts Pmf :: sb (* --{* processor manufacturer *}*)

datatype message = 
  Exec sb fn | Load sb fn val | Spy on  --{* input *}
| Val val | Ok | No                     --{* output *}

consts subject :: "message \<Rightarrow> sb"
primrec
  "subject (Exec sb fn  ) = sb"
  "subject (Load sb fn v) = sb"

subsection "ISM definition"

ism SLE66 =
  ports interface
    inputs \<spacespace>"{In}"
    outputs "{Out}"
  messages message
  states
    control ph init "P0" 
    data   chip_data name "s"

  transitions

  R00: P0 \<rightarrow> P1
    pre "f \<in> fct s\<inter>FTest0", "positive (output f s)"
    in  In  "[Exec Pmf f]"
    out Out "[Ok]"
    post valF := "valF s|`(-FTest0)"
  R01: P0 \<rightarrow> P2
    pre "f \<in> fct s\<inter>FTest1", "positive (output f s)"
    in  In  "[Exec Pmf f]"
    out Out "[Ok]"
    post valF := "valF s|`(-FTest)"
  R02: P0 \<rightarrow> Error
    pre "f \<in> fct s\<inter>FTest0", "\<not>positive (output f s)"
    in  In  "[Exec Pmf f]"
    out Out "[No]"
  R03: P0 \<rightarrow> P0
    pre "f \<in> fct s - FTest"
    in  In  "[Exec Pmf f]"
    out Out "[Val (output f s)]"
    post "change f s"
  R04: P0 \<rightarrow> P0
    pre "sb \<noteq> Pmf \<or> f \<notin> fct s"
    in  In  "[Exec sb f]"
    out Out "[No]"
  R11: P1 \<rightarrow> P2
    pre "f \<in> fct s\<inter>FTest1", "positive (output f s)"
    in  In  "[Exec Pmf f]"
    out Out "[Ok]"
    post valF := "valF s|`(-FTest1)"
  R12: P1 \<rightarrow> Error 
    pre "f \<in> fct s\<inter>FTest1", "\<not>positive (output f s)"
    in  In  "[Exec Pmf f]"
    out Out "[No]"
  R13: P1 \<rightarrow> P1
    pre "f \<in> fct s - FTest1"
    in  In  "[Exec Pmf f]"
    out Out "[Val (output f s)]"
    post "change f s"
  R14: P1 \<rightarrow> P1
    pre "sb \<noteq> Pmf \<or> f \<notin> fct s"
    in  In  "[Exec sb f]"
    out Out "[No]"
  R21: P2 \<rightarrow> P2
    pre "f \<in> fct s"
    in  In  "[Exec sb f]"
    out Out "[Val (output f s)]"
    post "change f s"
  R22: P2 \<rightarrow> P2
    pre "f \<notin> fct s"
    in  In  "[Exec sb f]"
    out Out "[No]"
  R31: Error \<rightarrow> Error
    pre "f_SN \<in> fct s"
    in  In  "[Exec sb f_SN]"
    out Out "[Val SN]"
  R32: Error \<rightarrow> Error
    pre "f \<notin> fct s\<inter>{f_SN}"
    in  In  "[Exec sb f]"
    out Out "[No]"
  R41: P1 \<rightarrow> P1
    pre "f \<in> F_NSec \<union> (F_ASec - fct s)"
    in  In  "[Load Pmf f v]"
    out Out "[Ok]"
    post valF := "valF s(f\<mapsto>v)"
  R42: ph \<rightarrow> ph
    pre "f \<notin> F_NSec \<union> (F_ASec - fct s) \<or> sb \<noteq> Pmf \<or> ph \<noteq> P1"
    in  In  "[Load sb f v]"
    out Out "[No]"
  R51: ph \<rightarrow> ph
    pre "on \<notin> Sec", "ph \<noteq> Error"
    in  In  "[Spy on]"
    out Out "case val s on of None \<Rightarrow> [] | Some v \<Rightarrow> [Val v]"
  R52: ph \<rightarrow> Error
    pre "on \<in> Sec", "v \<in> {[],[Val (the (val s on))]}", "ph \<noteq> Error"
    in  In  "[Spy on]"
    out Out "v"
    post "any"
  R52':ph \<rightarrow> ph
    pre "on \<in> Sec", "ph \<noteq> Error"
    in  In  "[Spy on]"
    out Out "[]"
  R53: Error \<rightarrow> Error
    in  In  "[Spy on]"
    out Out "[]"
    post "any"

lemma trans_ism [simp]: "ism.trans ism = transs"
by (simp add: ism_def ism.defs)

constdefs
  unwind :: "SLE66_state \<Rightarrow> on set \<Rightarrow> SLE66_state \<Rightarrow> bool"
 ("_/ ~_~/ _" [61, 61, 61] 60)
 "s ~A~ t \<equiv> fst s = fst t \<and> fct (snd s) = fct (snd t) \<and>
            (\<forall>on\<in>A. val (snd s) on = val (snd t) on)"

lemma unwind_def2: "(ph, s) ~A~ (ph',t) = (ph = ph' \<and> fct s = fct t \<and>
                      (\<forall>fn. F fn \<in> A \<longrightarrow> valF s fn = valF t fn) \<and>
                      (\<forall>dn. D dn \<in> A \<longrightarrow> valD s dn = valD t dn))"
by (auto simp add: unwind_def val_def split add: on.split)

lemma unwind_ph_fct_D: "(ph, s) ~A~ (ph',t) \<Longrightarrow> ph = ph' \<and> fct s = fct t"
by (simp add: unwind_def2)

theorem noleak_Sec_determ: "\<And>s t. \<lbrakk>s ~-Sec~ t; 
  s \<in> reach ism; ((p,s),c,(p' ,s')) \<in> transs;
  t \<in> reach ism; ((p,t),c,(p'',t')) \<in> transs; 
  fst s' \<noteq> Error; fst t' \<noteq> Error\<rbrakk> \<Longrightarrow> p' = p'' \<and> s' ~-Sec~ t'"
apply (clarsimp, frule unwind_ph_fct_D, clarify)
apply (erule SLE66.transs.elims)
apply (safe del: conjI IntI disjE UnE insertE)
apply (erule_tac [!] SLE66.transs.elims, simp_all)
oops

end