Theory Key

theory Key
  imports
    "../Fused_Resource"
begin


section ‹Key specification›

locale ideal_key =
  fixes valid_keys :: "'key set"
begin

subsection ‹Data-types for Parties, State, Events, Input, and Output›

datatype party = Alice | Bob

type_synonym s_shell = "party set"
datatype 'key' s_kernel = PState_Store | State_Store 'key'
type_synonym 'key' state = "'key' s_kernel × s_shell"

datatype event = Event_Shell party | Event_Kernel

datatype iadv = Inp_Adversary

datatype iusr_alice = Inp_Alice
datatype iusr_bob = Inp_Bob
type_synonym iusr = "iusr_alice + iusr_bob"

datatype oadv = Out_Adversary

datatype 'key' ousr_alice = Out_Alice 'key'
datatype 'key' ousr_bob = Out_Bob 'key'
type_synonym 'key' ousr = "'key' ousr_alice + 'key' ousr_bob"


subsubsection ‹Basic lemmas for automated handling of party sets (i.e. @{text s_shell})›

lemma Alice_neq_iff [simp]: "Alice ≠ x ⟷ x = Bob"
  by(cases x) simp_all

lemma neq_Alice_iff [simp]: "x ≠ Alice ⟷ x = Bob"
  by(cases x) simp_all

lemma Bob_neq_iff [simp]: "Bob ≠ x ⟷ x = Alice"
  by(cases x) simp_all

lemma neq_Bob_iff [simp]: "x ≠ Bob ⟷ x = Alice"
  by(cases x) simp_all

lemma Alice_in_iff_nonempty: "Alice ∈ A ⟷ A ≠ {}" if "Bob ∉ A"
  using that by(auto)(metis (full_types) party.exhaust)

lemma Bob_in_iff_nonempty: "Bob ∈ A ⟷ A ≠ {}" if "Alice ∉ A"
  using that by(auto)(metis (full_types) party.exhaust)


subsection ‹Defining the event handler›

fun poke :: "('key state, event) handler"
  where
    "poke (s_kernel, parties) (Event_Shell party) = 
      (if party ∈ parties then 
        return_pmf None
      else 
        return_spmf (s_kernel, insert party parties))"
  | "poke (PState_Store, s_shell) (Event_Kernel) = do {
      key ← spmf_of_set valid_keys;
      return_spmf (State_Store key, s_shell)  } "
  | "poke _ _ = return_pmf None"

lemma in_set_spmf_poke:
  "s' ∈ set_spmf (poke s x) ⟷
  (∃s_kernel parties party. s = (s_kernel, parties) ∧ x = Event_Shell party ∧ party ∉ parties ∧ s' = (s_kernel, insert party parties)) ∨
  (∃s_shell key. s = (PState_Store, s_shell) ∧ x = Event_Kernel ∧ key ∈ valid_keys ∧ finite valid_keys ∧ s' = (State_Store key, s_shell))"
  by(cases "(s, x)" rule: poke.cases)(auto simp add: set_spmf_of_set)

lemma foldl_poke_invar:
  "⟦ (s_kernel', parties') ∈ set_spmf (foldl_spmf poke p events); ∀(s_kernel, parties)∈set_spmf p. set_s_kernel s_kernel ⊆ valid_keys ⟧
  ⟹ set_s_kernel s_kernel' ⊆ valid_keys"
  by(induction events arbitrary: parties' rule: rev_induct)
    (auto 4 3 simp add: split_def foldl_spmf_append in_set_spmf_poke dest: bspec)

subsection ‹Defining the adversary interface›

fun iface_adv :: "('key state, iadv, oadv) oracle'"
  where
   "iface_adv state _ = return_spmf (Out_Adversary, state)"


subsection ‹Defining the user interfaces›

context
begin

private fun iface_usr_func :: "party ⇒ _ ⇒ _ ⇒ 'inp ⇒ ('wrap_key × 'key state) spmf"
  where
    "iface_usr_func party wrap (State_Store key, parties) inp = 
      (if party ∈ parties then
        return_spmf (wrap key, State_Store key, parties)
      else
        return_pmf None)"
  | "iface_usr_func _ _ _ _ = return_pmf None"

abbreviation iface_alice :: "('key state, iusr_alice, 'key ousr_alice) oracle'"
  where
    "iface_alice ≡ iface_usr_func Alice Out_Alice"

abbreviation iface_bob :: "('key state, iusr_bob, 'key ousr_bob) oracle'"
  where
    "iface_bob ≡ iface_usr_func Bob Out_Bob"

abbreviation iface_usr :: "('key state, iusr, 'key ousr) oracle'"
  where
    "iface_usr ≡ plus_oracle iface_alice iface_bob"

lemma in_set_iface_usr_func [simp]:
  "x ∈ set_spmf (iface_usr_func party wrap state inp) ⟷
   (∃key parties. state = (State_Store key, parties) ∧ party ∈ parties ∧ x = (wrap key, State_Store key, parties))"
  by(cases "(party, wrap, state, inp)" rule: iface_usr_func.cases) auto

end


subsection ‹Defining the Fuse Resource›

primcorec core :: "('key state, event, iadv, iusr, oadv,'key ousr) core" 
  where
    "cpoke core = poke"
  | "cfunc_adv core = iface_adv"
  | "cfunc_usr core = iface_usr"

sublocale fused_resource core "(PState_Store, {})" .


subsubsection ‹Lemma showing that the resulting resource is well-typed›

lemma WT_core [WT_intro]: 
  "WT_core ℐ_full (ℐ_uniform UNIV (Out_Alice ` valid_keys) ⊕⇩ℐ ℐ_uniform UNIV (Out_Bob ` valid_keys))
     (pred_prod (pred_s_kernel (λkey. key ∈ valid_keys)) (λ_. True)) core"
  apply (rule WT_core.intros)
  subgoal for s e s' by(cases "(s, e)" rule: poke.cases)(auto split: if_split_asm simp add: set_spmf_of_set)
  by auto

lemma WT_fuse [WT_intro]: 
  assumes [WT_intro]: "WT_rest ℐ_adv_rest ℐ_usr_rest I_rest rest"
  shows "(ℐ_full ⊕⇩ℐ ℐ_adv_rest) ⊕⇩ℐ ((ℐ_uniform UNIV (Out_Alice ` valid_keys) ⊕⇩ℐ ℐ_uniform UNIV (Out_Bob ` valid_keys)) ⊕⇩ℐ ℐ_usr_rest) ⊢res resource rest √"
  by(rule WT_intro)+ simp
 
end

end