Theory One_Time_Pad

theory One_Time_Pad
  imports
    Sigma_Commit_Crypto.Xor
    "../Asymptotic_Security"
    "../Construction_Utility"
    "../Specifications/Key"
    "../Specifications/Channel"
begin

section ‹One-time-pad construction›

locale one_time_pad =
    key: ideal_key "carrier "  +
    auth: ideal_channel "id :: 'msg  'msg" False +
    sec: ideal_channel "λ_ :: 'msg. carrier " False +
    boolean_algebra 
  for 
     :: "('msg, 'more) boolean_algebra_scheme" (structure) +
  assumes
    nempty_carrier: "carrier   {}" and
    finite_carrier: "finite (carrier )"
begin


subsection ‹Defining user callees›

definition enc_callee :: " unit  'msg sec.iusr_alice 
   (sec.ousr_alice × unit, key.iusr_alice + 'msg sec.iusr_alice, 'msg key.ousr_alice + auth.ousr_alice) gpv"
  where
    "enc_callee  stateless_callee (λinp. case inp of sec.Inp_Send msg 
      if msg  carrier  then
        Pause 
          (Inl key.Inp_Alice) 
          (λkout. case projl kout of key.Out_Alice key  
            let cipher = key  msg in
            Pause (Inr (auth.Inp_Send cipher)) (λ_. Done sec.Out_Send))
      else
        Fail)"

definition dec_callee :: " unit  sec.iusr_bob 
   ('msg sec.ousr_bob × unit, key.iusr_bob + auth.iusr_bob, 'msg key.ousr_bob + 'msg auth.ousr_bob) gpv"
  where
    "dec_callee  stateless_callee (λ_.
      Pause 
        (Inr auth.Inp_Recv) 
        (λcout. case cout of 
          Inr (auth.Out_Recv cipher) 
            Pause 
              (Inl key.Inp_Bob) 
              (λkout. case projl kout of key.Out_Bob key 
                Done (sec.Out_Recv (key  cipher)))
        | _  Fail))"


subsection ‹Defining adversary converter›

type_synonym 'msg' astate = "'msg' option"

definition look_callee :: "'msg astate  sec.iadv_look 
   ('msg sec.oadv_look × 'msg astate, sec.iadv_look,  'msg set sec.oadv_look) gpv"
  where
    "look_callee  λstate inp.   
      Pause 
        sec.Inp_Look
        (λcout. case cout of
          sec.Out_Look msg_set  
            (case state of
              None  do {
                msg  lift_spmf (spmf_of_set (msg_set));
                Done (auth.Out_Look msg, Some msg)  }
            | Some msg  Done (auth.Out_Look msg, Some msg)))"

definition sim :: "
  (key.iadv + auth.iadv_drop + auth.iadv_look + 'msg auth.iadv_fedit,
    key.oadv + auth.oadv_drop + 'msg auth.oadv_look + auth.oadv_fedit,
    sec.iadv_drop + sec.iadv_look + 'msg sec.iadv_fedit,
    sec.oadv_drop + 'msg set sec.oadv_look + sec.oadv_fedit) converter"
  where
    "sim  
      let look_converter = converter_of_callee look_callee None in
      ldummy_converter (λ_. key.Out_Adversary) (1C |= look_converter |= 1C)"


subsection ‹Defining event-translator›

type_synonym estate = "bool × (key.party + auth.party) set"

abbreviation einit :: estate
  where
    "einit  (False, {})"

definition sec_party_of_key_party :: "key.party  sec.party" 
  where
    "sec_party_of_key_party  key.case_party sec.Alice sec.Bob"

abbreviation etran_base_helper :: "estate  key.party + auth.party  sec.event list"
  where
    "etran_base_helper  (λ(s_flg, s_kap) item. 
      let sp_of = case_sum sec_party_of_key_party id in
      let se_of = (λchk out. if s_flg  chk then [out] else []) in
      let chk_alice = Inl key.Alice  s_kap  Inr auth.Alice  s_kap in
      let chk_bob = Inl key.Bob  s_kap  Inr auth.Bob  s_kap in
      sec.case_party
        (se_of chk_alice (sec.Event_Shell sec.Alice))
        (se_of chk_bob (sec.Event_Shell sec.Bob))
        (sp_of item))"

abbreviation etran_base :: "(estate, key.party + auth.party, sec.event list) oracle'"
  where
    "etran_base  (λ(s_flg, s_kap) item.  
      let s_kap' = insert item s_kap in
      let event = etran_base_helper (s_flg, s_kap') item in
      if item  s_kap then return_spmf (event, s_flg, s_kap') else return_pmf None)"

fun etran :: "(estate, key.event + auth.event, sec.event list) oracle'"
  where
    "etran state (Inl (key.Event_Shell party)) = etran_base state (Inl party)"
  | "etran (False, s_kap) (Inl key.Event_Kernel) = 
      (let check_alice = Inl key.Alice  s_kap  Inr auth.Alice  s_kap in
      let check_bob = Inl key.Bob  s_kap  Inr auth.Bob  s_kap in
      let e_alice = if check_alice then [sec.Event_Shell sec.Alice] else [] in
      let e_bob = if check_bob then [sec.Event_Shell sec.Bob] else [] in
      return_spmf (e_alice @ e_bob, True, s_kap))"
  | "etran state (Inr (auth.Event_Shell party)) = etran_base state (Inr party)"
  | "etran _ _ = return_pmf None"


subsubsection ‹Basic lemmas for automated handling of @{term sec_party_of_key_party}

lemma sec_party_of_key_party_simps [simp]:
  "sec_party_of_key_party key.Alice = sec.Alice"
  "sec_party_of_key_party key.Bob = sec.Bob"
  by(simp_all add: sec_party_of_key_party_def)

lemma sec_party_of_key_party_eq_simps [simp]:
  "sec_party_of_key_party p = sec.Alice  p = key.Alice"
  "sec_party_of_key_party p = sec.Bob  p = key.Bob"
  by(simp_all add: sec_party_of_key_party_def split: key.party.split)

lemma key_case_party_collapse [simp]: "key.case_party x x p = x"
  by(simp split: key.party.split)

lemma sec_case_party_collapse [simp]: "sec.case_party x x p = x"
  by(simp split: sec.party.split)

lemma Alice_in_sec_party_of_key_party [simp]:
  "sec.Alice  sec_party_of_key_party ` P  key.Alice  P"
  by(auto simp add: sec_party_of_key_party_def split: key.party.splits)

lemma Bob_in_sec_party_of_key_party [simp]:
  "sec.Bob  sec_party_of_key_party ` P  key.Bob  P"
  by(auto simp add: sec_party_of_key_party_def split: key.party.splits)

lemma case_sec_party_of_key_party [simp]: "sec.case_party a b (sec_party_of_key_party x) = key.case_party a b x"
  by(simp add: sec_party_of_key_party_def split: sec.party.split key.party.split)


subsection ‹Defining Ideal and Real constructions›

context 
  fixes 
    key_rest :: "('key_s_rest, key.event, 'key_iadv_rest, 'key_iusr_rest, 'key_oadv_rest, 'key_ousr_rest) rest_wstate" and
    auth_rest :: "('auth_s_rest, auth.event, 'auth_iadv_rest, 'auth_iusr_rest, 'auth_oadv_rest, 'auth_ousr_rest) rest_wstate"
begin

definition ideal_rest 
  where
    "ideal_rest  translate_rest einit etran (parallel_rest key_rest auth_rest)"

definition ideal_resource 
  where
    "ideal_resource  (sim |= 1C) |= 1C |= 1C   (sec.resource ideal_rest)"

definition real_resource 
  where
    "real_resource  attach_c1f22_c1f22 (CNV enc_callee ()) (CNV dec_callee ()) (key.resource key_rest) (auth.resource auth_rest)"


subsection ‹Wiring and simplifying the Ideal construction›

definition ideal_s_core' :: "((_ × 'msg astate × _) × _) × estate × 'msg sec.state"
  where
    "ideal_s_core'  ((((), None, ()), ()), (False, {}), sec.State_Void, {})"

definition ideal_s_rest' :: "_ × 'key_s_rest × 'auth_s_rest"
  where
    "ideal_s_rest'  (((), ()), rinit key_rest, rinit auth_rest)"

primcorec ideal_core' :: "(((unit × _ × unit) × unit) ×  _,  _, key.iadv + _, _, _, _) core"
  where
    "cpoke ideal_core' = (λ(s_advusr, s_event, s_core) event. do {
        (events, s_event')  (etran s_event event);
        s_core'  foldl_spmf sec.poke (return_spmf s_core) events;
        return_spmf (s_advusr, s_event', s_core')
    })"
  | "cfunc_adv ideal_core' = (λ((s_adv, s_usr), s_core) iadv.
      let handle_l = (λ_. Done (Inl key.Out_Adversary, s_adv)) in
      let handle_r = (λqr. map_gpv (map_prod Inr id) id ((1I I look_callee I 1I) s_adv qr)) in
      map_spmf 
        (λ((oadv, s_adv'), s_core'). (oadv, (s_adv', s_usr), s_core'))
        (exec_gpv sec.iface_adv (case_sum handle_l handle_r iadv) s_core))"
  | "cfunc_usr ideal_core' = sec.iface_usr"

primcorec ideal_rest' :: "((unit × unit) × _, _, _, _, _, _, _) rest_scheme"
  where
    "rinit ideal_rest' = (((), ()), rinit key_rest, rinit auth_rest)"
  | "rfunc_adv ideal_rest' = (parallel_eoracle (rfunc_adv key_rest) (rfunc_adv auth_rest))"
  | "rfunc_usr ideal_rest' = (parallel_eoracle (rfunc_usr key_rest) (rfunc_usr auth_rest))"


subsubsection ‹The ideal attachment lemma›
  
lemma attach_ideal: "ideal_resource = RES (fused_resource.fuse ideal_core' ideal_rest') (ideal_s_core', ideal_s_rest')"
proof -

  have fact1: "ideal_rest' = attach_rest 1I 1I (Pair ((), ())) (parallel_rest key_rest auth_rest)"  (is "?L = ?R")
  proof -

    have "rinit ?L = rinit ?R"
      by simp

    moreover have "rfunc_adv ?L = rfunc_adv ?R"
      unfolding attach_rest_id_oracle_adv parallel_eoracle_def
      by (simp add: extend_state_oracle_def)

    moreover have "rfunc_usr ?L = rfunc_usr ?R"
      unfolding attach_rest_id_oracle_usr parallel_eoracle_def
      by (simp add: extend_state_oracle_def)

    ultimately show ?thesis
      by (coinduction) blast
  qed

  have fact2: "ideal_core' =
    (let handle_l = (λs ql. Generative_Probabilistic_Value.Done (Inl key.Out_Adversary, s)) in
     let handle_r = (λs qr. map_gpv (map_prod Inr id) id ((1I I look_callee I 1I) s qr)) in
     let tcore = translate_core etran sec.core in
    attach_core (λs. case_sum (handle_l s) (handle_r s)) 1I tcore)" (is "?L = ?R")
  proof -

    have "cpoke ?L = cpoke ?R"
      by (simp add: split_def map_spmf_conv_bind_spmf)

    moreover have "cfunc_adv ?L = cfunc_adv ?R"
      unfolding attach_core_def
      by (simp add: split_def)

    moreover have "cfunc_usr ?L = cfunc_usr ?R"
      unfolding Let_def attach_core_id_oracle_usr
      by (clarsimp simp add: extend_state_oracle_def[symmetric])
    
    ultimately show ?thesis
      by (coinduction) blast
  qed

  show ?thesis
    unfolding ideal_resource_def sec.resource_def sim_def ideal_rest_def ideal_s_core'_def ideal_s_rest'_def
    apply(simp add: conv_callee_parallel_id_right[symmetric, where s'="()"])
    apply(simp add: conv_callee_parallel_id_left[symmetric, where s="()"])
    apply(simp add: ldummy_converter_of_callee)
    apply(subst fused_resource_move_translate[of _ einit etran])
    apply(simp add: resource_of_oracle_state_iso)
    apply(simp add: iso_swapar_def split_beta ideal_rest_def)
    apply(subst (1 2 3) converter_of_callee_id_oracle[symmetric, of "()"])
    apply(subst attach_parallel_fuse'[where f_init="Pair ((), ())"])
    apply(simp add: fact1[symmetric] fact2[symmetric, simplified Let_def])
    done  
qed

subsection ‹Wiring and simplifying the Real construction›

definition real_s_core' :: "_ × 'msg key.state × 'msg auth.state"
  where
    "real_s_core'  (((), (), ()), (key.PState_Store, {}), (auth.State_Void, {}))"

definition real_s_rest'
  where
    "real_s_rest'  ideal_s_rest'"

primcorec real_core' :: "((unit × _) × _, _, _, _, _, _) core"
  where
    "cpoke real_core' = (λ(s_advusr, s_core) event. 
      map_spmf (Pair s_advusr) (parallel_handler key.poke auth.poke s_core event))"
  | "cfunc_adv real_core' = (key.iface_adv O auth.iface_adv)"
  | "cfunc_usr real_core' = (λ((s_adv, s_usr), s_core) iusr.
      let handle_req = lsumr  map_sum id (rsuml  map_sum swap_sum id  lsumr)  rsuml in
      let handle_ret = lsumr  (map_sum id (rsuml  (map_sum swap_sum id  lsumr))  rsuml) in
      map_spmf 
        (λ((ousr, s_usr'), s_core'). (ousr, (s_adv, s_usr'), s_core'))
        (exec_gpv 
          (key.iface_usr O auth.iface_usr)
          (map_gpv' id handle_req  handle_ret ((enc_callee I dec_callee) s_usr iusr)) s_core))"

definition real_rest'
  where
    "real_rest'  ideal_rest'"


subsubsection ‹The real attachment lemma›

private lemma WT_callee_real1: "((ℐ_full  ℐ_full)  (ℐ_full  ℐ_full))  ((ℐ_full  ℐ_full)  (ℐ_full  ℐ_full)) ⊢c 
  (key.fuse key_rest O auth.fuse auth_rest) s "
  apply(rule WT_calleeI)
  apply(cases s)
  apply(case_tac call)
   apply(rename_tac [!] x)
   apply(case_tac [!] x)
     apply(rename_tac [!] y)
     apply(case_tac [!] y)
  by(auto simp add: fused_resource.fuse.simps)

private lemma WT_callee_real2: "(ℐ_full  ℐ_full)  (((ℐ_full  ℐ_full)  (ℐ_full  ℐ_full))  ℐ_full) ⊢c
  fused_resource.fuse (parallel_core key.core auth.core) (parallel_rest key_rest auth_rest) s "
  apply(rule WT_calleeI)
  apply(cases s)
  apply(case_tac call)
   apply(rename_tac [!] x)
   apply(case_tac [!] x)
     apply(rename_tac [!] y)
     apply(case_tac [!] y)
         apply(rename_tac [5] z)
         apply(rename_tac [6] z)
         apply(case_tac [5] z)
          apply(case_tac [7] z)
  by(auto simp add: fused_resource.fuse.simps)


lemma attach_real: "real_resource = RES (fused_resource.fuse real_core' real_rest') (real_s_core', real_s_rest')"
proof -

  have fact1: "real_core' = attach_core 1I (attach_wiring_right parallel_wiringw (enc_callee I dec_callee)) 
    (parallel_core key.core auth.core) " (is "?L = ?R")
  proof-

    have "cpoke ?L = cpoke ?R"
      by simp

    moreover have "cfunc_adv ?L = cfunc_adv ?R"
      unfolding attach_core_id_oracle_adv
      by (simp add: extend_state_oracle_def)

    moreover have "cfunc_usr ?L = cfunc_usr ?R"
      unfolding parallel_wiringw_def swap_lassocrw_def swapw_def lassocrw_def rassoclw_def
      by (simp add: attach_wiring_right_simps parallel2_wiring_simps comp_wiring_simps)

    ultimately show ?thesis
      by (coinduction) blast
  qed

  have fact2: "real_rest' = attach_rest 1I 1I (Pair ((), ())) (parallel_rest key_rest auth_rest) "  (is "?L = ?R")
  proof -
    have "rinit ?L = rinit ?R"
      unfolding real_rest'_def ideal_rest'_def 
      by simp

    moreover have "rfunc_adv ?L = rfunc_adv ?R"
      unfolding real_rest'_def ideal_rest'_def attach_rest_id_oracle_adv 
      by (simp add: extend_state_oracle_def)

    moreover have "rfunc_usr ?L = rfunc_usr ?R"
      unfolding real_rest'_def ideal_rest'_def attach_rest_id_oracle_usr
      by (simp add: extend_state_oracle_def)

    ultimately show ?thesis
      by (coinduction) blast
  qed

  show ?thesis
    unfolding real_resource_def attach_c1f22_c1f22_def wiring_c1r22_c1r22_def key.resource_def auth.resource_def
    apply(subst resource_of_parallel_oracle[symmetric])
    apply(subst attach_compose)
    apply(subst attach_wiring_resource_of_oracle)
       apply(rule wiring_intro)
      apply (rule WT_resource_of_oracle[OF WT_callee_real1])
     apply simp
    subgoal
      apply(subst parallel_oracle_fuse)
      apply(subst resource_of_oracle_state_iso)
       apply simp
      apply(simp add: parallel_state_iso_def)
      apply(subst conv_callee_parallel[symmetric])
      apply(subst eq_resource_on_UNIV_iff[symmetric])
      apply(rule eq_resource_on_trans)
       apply(rule eq_ℐ_attach_on')
         apply (rule WT_resource_of_oracle[OF WT_callee_real2])
        apply(rule parallel_converter2_eq_ℐ_cong)
         apply(rule eq_ℐ_converter_reflI)
         apply(rule WT_intro)+
        apply(rule parallel_converter2_eq_ℐ_cong)
         apply(rule comp_converter_of_callee_wiring)
          apply(rule wiring_intro)
         apply(subst conv_callee_parallel)
         apply(rule WT_intro)
          apply (rule WT_converter_of_callee[where=ℐ_full and ℐ'="ℐ_full  ℐ_full"])
           apply (rule WT_gpv_ℐ_mono)
            apply (rule WT_gpv_full)
           apply (rule ℐ_full_le_plus_ℐ)
            apply(rule order_refl)
           apply(rule order_refl)
          apply (clarsimp simp add: enc_callee_def stateless_callee_def split!: sec.iusr_alice.splits key.ousr_alice.splits)
         apply (rule WT_converter_of_callee[where=ℐ_full and ℐ'="ℐ_full  ℐ_full"])
          apply (rule WT_gpv_ℐ_mono)
           apply (rule WT_gpv_full)
          apply (rule ℐ_full_le_plus_ℐ)
           apply(rule order_refl)
          apply(rule order_refl)
         apply (clarsimp simp add: enc_callee_def stateless_callee_def split!: sec.iusr_alice.splits key.ousr_alice.splits)
        apply(subst id_converter_eq_self)
         apply(rule order_refl)
        apply simp
       apply simp
      apply(subst eq_resource_on_UNIV_iff)
      apply(subst (1 2 3) converter_of_callee_id_oracle[symmetric, of "()"])
      apply(subst attach_parallel_fuse')
      apply(simp add: fact1 fact2 real_s_core'_def real_s_rest'_def ideal_s_rest'_def)
    done
  done
qed


subsection ‹Proving the trace-equivalence of simplified Ideal and Real constructions›

context
begin


subsubsection ‹Proving the trace-equivalence of cores›

private abbreviation 
  "a_I  λ(x, y). ((((), x, ()), ()), y)"

private abbreviation
  "a_R  λx. (((), (), ()), x)"

abbreviation
  "asm_act  (λflg pset_sec pset_key pset_auth pset_union.
     pset_union = pset_key <+> pset_auth 
     (flg  pset_sec = sec_party_of_key_party ` pset_key  pset_auth))"

private inductive S :: "(((_ × 'msg option × _) × _) × estate × 'msg sec.state) spmf 
   (_ × 'msg key.state × 'msg auth.state) spmf  bool"
  where
― ‹(Auth =a)@(Key =0)›
    s_0_0: "S (return_spmf (a_I (None, (False, s_act_ka), sec.State_Void, s_act_s))) 
      (return_spmf (a_R ((key.PState_Store, s_act_k), auth.State_Void, s_act_a)))"
  if "asm_act False s_act_s s_act_k s_act_a s_act_ka" and "s_act_s = {}"
― ‹(Auth =a)@(Key =1)›
  | s_0_1: "S (return_spmf (a_I (None, (True, s_act_ka), sec.State_Void, s_act)))
      (map_spmf (λkey. a_R ((key.State_Store key, s_act_k), auth.State_Void, s_act_a)) (spmf_of_set (carrier )))"
  if "asm_act True s_act s_act_k s_act_a s_act_ka"
― ‹../(Auth =a)@(Key =1) \# wl›
  | s_1_1: "S (return_spmf (a_I (None, (True ,s_act_ka), sec.State_Store msg, s_act_s)))
      (map_spmf (λkey. a_R ((key.State_Store key, s_act_k), auth.State_Store (key  msg), s_act_a)) (spmf_of_set (carrier )))"
  if "asm_act True s_act_s s_act_k s_act_a s_act_ka" and "key.Alice  s_act_k" and "auth.Alice  s_act_a" and "msg  carrier "
  | s_2_1: "S (return_spmf (a_I (None, (True ,s_act_ka), sec.State_Collect msg, s_act_s)))
      (map_spmf (λkey. a_R ((key.State_Store key, s_act_k), auth.State_Collect (key  msg), s_act_a)) (spmf_of_set (carrier )))"
  if "asm_act True s_act_s s_act_k s_act_a s_act_ka" and "key.Alice  s_act_k" and "auth.Alice  s_act_a" and "msg  carrier "
  | s_3_1: "S (return_spmf (a_I (None, (True ,s_act_ka), sec.State_Collected, s_act_s)))
      (map_spmf (λkey. a_R ((key.State_Store key, s_act_k), auth.State_Collected, s_act_a)) (spmf_of_set (carrier )))"
  if "asm_act True s_act_s s_act_k s_act_a s_act_ka" and "s_act_k = {key.Alice, key.Bob}" and "s_act_a = {auth.Alice, auth.Bob}"
― ‹../(Auth =a)@(Key =1) \# look›
  | s_1'_1: "S (return_spmf (a_I (Some (key  msg), (True ,s_act_ka), sec.State_Store msg, s_act_s)))
      (return_spmf (a_R ((key.State_Store key, s_act_k), auth.State_Store (key  msg), s_act_a)))"
  if "asm_act True s_act_s s_act_k s_act_a s_act_ka" and "key.Alice  s_act_k" and "auth.Alice  s_act_a" and "msg  carrier " and "key  carrier "
  | s_2'_1: "S (return_spmf (a_I (Some (key  msg), (True ,s_act_ka), sec.State_Collect msg, s_act_s)))
      (return_spmf (a_R ((key.State_Store key, s_act_k), auth.State_Collect (key  msg), s_act_a)))"
  if "asm_act True s_act_s s_act_k s_act_a s_act_ka" and "key.Alice  s_act_k" and "auth.Alice  s_act_a" and "msg  carrier " and "key  carrier "
  | s_3'_1: "S (return_spmf (a_I (Some (key  msg), (True ,s_act_ka), sec.State_Collected, s_act_s)))
      (return_spmf (a_R ((key.State_Store key, s_act_k), auth.State_Collected, s_act_a)))"
  if "asm_act True s_act_s s_act_k s_act_a s_act_ka" and "s_act_k = {key.Alice, key.Bob}" and "s_act_a = {auth.Alice, auth.Bob}" and "msg  carrier " and "key  carrier "

private lemma trace_eq_core: "trace_core_eq ideal_core' real_core' 
  UNIV (UNIV <+> UNIV <+> UNIV <+> (auth.Inp_Fedit ` carrier )) ((sec.Inp_Send ` carrier ) <+> UNIV) 
  (return_spmf ideal_s_core') (return_spmf real_s_core')"
proof -

  have inj_xor: "msg  carrier  ; x  carrier ; y  carrier ; x  msg = y  msg  x = y" for msg x y
    by (metis (no_types, opaque_lifting) local.xor_ac(2) local.xor_left_inverse)

  note [simp] = enc_callee_def dec_callee_def look_callee_def nempty_carrier finite_carrier
    exec_gpv_bind spmf.map_comp map_bind_spmf bind_map_spmf bind_spmf_const o_def Let_def
      
  show ?thesis
    apply (rule trace_core_eq_simI_upto[where S=S])
    subgoal Init_OK 
      by (simp add: ideal_s_core'_def real_s_core'_def S.simps)
    subgoal POut_OK for s_i s_r query
      apply (cases query)
      subgoal for e_key 
        apply (cases e_key)
        subgoal for e_shell by (erule S.cases) (auto simp add: map_spmf_conv_bind_spmf[symmetric] split: key.party.splits)
        subgoal e_kernel by (erule S.cases) (auto simp add: map_spmf_conv_bind_spmf[symmetric])
        done
      subgoal for e_auth
        apply (cases e_auth)
        subgoal for e_shell
          by (erule S.cases) (auto simp add: map_spmf_conv_bind_spmf[symmetric] split:auth.party.splits)
        done
      done
    subgoal PState_OK for s_i s_r query
      apply (cases query)
      subgoal for e_key
        apply (cases e_key)
        subgoal for e_shell by (erule S.cases) (auto simp add: map_spmf_conv_bind_spmf[symmetric] intro!: trace_eq_simcl.base S.intros[simplified] split: key.party.splits)
        subgoal e_kernel by (erule S.cases) (auto simp add: map_spmf_conv_bind_spmf[symmetric] sec_party_of_key_party_def intro!: trace_eq_simcl.base S.intros[simplified] split: key.party.splits)    
        done
      subgoal for e_auth
        apply (cases e_auth)
        subgoal for e_shell by (erule S.cases) (auto simp add: map_spmf_conv_bind_spmf[symmetric] intro!: trace_eq_simcl.base S.intros[simplified] split:auth.party.splits)
        done
      done
    subgoal AOut_OK for s_i s_r query
      apply (cases query)
      subgoal for q_key by (erule S.cases) simp_all 
      subgoal for q_auth
        apply (cases q_auth)
        subgoal for q_auth_drop by (erule S.cases) (simp_all add: id_oracle_def)
        subgoal for q_auth_lfe
          apply (cases q_auth_lfe)
          subgoal for q_auth_look
          proof (erule S.cases, goal_cases)
            case (3 s_act_s s_act_k s_act_a s_act_ka msg) ― ‹Corresponds to @{thm [source] s_1_1}
            then show ?case 
              apply(simp add: exec_gpv_extend_state_oracle exec_gpv_map_gpv_id exec_gpv_plus_oracle_right exec_gpv_plus_oracle_left)
              apply (subst one_time_pad[symmetric, of "msg"])
               apply (simp_all add: xor_comm)
              apply (rule bind_spmf_cong[OF HOL.refl])
              by (simp add: xor_comm)
          qed simp_all
          subgoal for q_auth_fedit  by (erule S.cases) (auto simp add: id_oracle_def split:auth.iadv_fedit.split)
          done
        done
      done
    subgoal AState_OK for s_i s_r query
      apply (cases query)
      subgoal for q_key by (erule S.cases) (auto simp add: map_spmf_conv_bind_spmf[symmetric] intro!: trace_eq_simcl.base S.intros[simplified])
      subgoal for q_auth
        apply (cases q_auth)
        subgoal for q_auth_drop by (erule S.cases) (auto simp add: id_oracle_def)
        subgoal for q_auth_lfe
          apply (cases q_auth_lfe)
          subgoal for q_auth_look
          proof (erule S.cases, goal_cases)
            case (3 s_act_s s_act_k s_act_a s_act_ka msg) ― ‹Corresponds to @{thm [source] s_1_1}
            then show ?case 
              apply(simp add: exec_gpv_extend_state_oracle exec_gpv_map_gpv_id exec_gpv_plus_oracle_right exec_gpv_plus_oracle_left)
              apply (clarsimp simp add: map_spmf_conv_bind_spmf[symmetric])
              apply (subst (1 2) cond_spmf_fst_map_Pair1; clarsimp simp add: set_spmf_of_set inj_on_def intro: inj_xor)
               apply (rule inj_xor, simp_all)             
              apply(subst (1 2 3) inv_into_f_f)
              by (auto simp add: S.simps inj_on_def intro: inj_xor)
          qed (auto intro!: trace_eq_simcl.base S.intros[simplified])
          subgoal for q_auth_fedit by (erule S.cases) (auto simp add: map_spmf_conv_bind_spmf[symmetric] id_oracle_def intro!: trace_eq_simcl.base S.intros[simplified])
          done
        done
      done
    subgoal UOut_OK for s_i s_r query
      apply (cases query)
      subgoal for q_alice
      proof (erule S.cases, goal_cases)
        case (2 s_act_s s_act_k s_act_a s_act_ka) ― ‹Corresponds to @{thm [source] s_0_1}
        then show ?case 
          apply (cases "auth.Alice  s_act_a"; cases "key.Alice  s_act_k")
             apply (simp_all add: stateless_callee_def split_def split!: auth.iusr_alice.split)
          done 
      qed (simp_all add: stateless_callee_def split: auth.iusr_alice.split)
      subgoal for q_bob
      proof (erule S.cases, goal_cases)
        case (4 s_act_s s_act_k s_act_a s_act_ka msg) ― ‹Corresponds to @{thm [source] s_2_1}
        then show ?case 
          apply (cases "sec.Bob  s_act_s")
          subgoal
            apply (clarsimp simp add: stateless_callee_def)
            apply (simp add: spmf_rel_eq[symmetric])
            apply (rule rel_spmf_bindI2)
            by simp_all
          subgoal by (cases "sec.Bob  s_act_a") (clarsimp simp add: stateless_callee_def)+
          done
      qed (simp_all add: stateless_callee_def)
      done
    subgoal UState_OK for s_i s_r query
      apply (cases query)
      subgoal for q_alice
      proof (erule S.cases, goal_cases)
        case (2 s_act s_act_k s_act_a s_act_ka) ― ‹Corresponds to @{thm [source] s_0_1}
        then show ?case 
          apply (cases "auth.Alice  s_act_a"; cases "key.Alice  s_act_k")
          subgoal
            apply (clarsimp simp add: map_spmf_conv_bind_spmf[symmetric] stateless_callee_def split_def split!: auth.iusr_alice.split if_splits)
            apply(rule trace_eq_simcl.base)
            apply (rule S.intros(3)[simplified])
            by simp_all
          by (clarsimp simp add: map_spmf_conv_bind_spmf[symmetric] stateless_callee_def split_def split: auth.iusr_alice.split)+
      qed (auto simp add: stateless_callee_def split: auth.iusr_alice.split_asm)
      subgoal for q_bob
      proof (erule S.cases, goal_cases)
        case (4 s_act_s s_act_k s_act_a s_act_ka msg) ― ‹Corresponds to @{thm [source] s_2_1}
        then show ?case 
          apply (cases "sec.Bob  s_act_s")
          subgoal 
            apply (clarsimp simp add: stateless_callee_def map_spmf_conv_bind_spmf[symmetric])
            apply (subst map_spmf_of_set_inj_on)
             apply (simp_all add: inj_on_def)
            apply (subst map_spmf_of_set_inj_on[symmetric])
             apply (simp add: inj_on_def)
            apply clarsimp
            apply(rule trace_eq_simcl.base)
            apply (rule S.intros(5)[simplified])
              apply (simp_all split: sec.party.splits )
            by auto
          subgoal by (clarsimp simp add: stateless_callee_def split: if_splits)
          done
      next
        case (7 s_act_s s_act_k s_act_a s_act_ka msg key) ― ‹Corresponds to @{thm [source] s_2'_1}
        then show ?case 
          apply (cases "sec.Bob  s_act_s")
          subgoal 
            apply (clarsimp simp add: stateless_callee_def map_spmf_conv_bind_spmf[symmetric])
            apply (rule S.intros(8)[simplified])
                apply simp_all
            by auto
          subgoal by (clarsimp simp add: stateless_callee_def split: if_splits)
          done
      qed (auto simp add: stateless_callee_def split: auth.iusr_alice.split_asm)
      done
    done
qed


subsubsection ‹Proving the trace equivalence of fused cores and rests›

private definition ℐ_adv_core :: "(key.iadv + 'msg auth.iadv, key.oadv + 'msg auth.oadv) "
  where "ℐ_adv_core  ℐ_full  (ℐ_full  (ℐ_full  ℐ_uniform (sec.Inp_Fedit ` (carrier )) UNIV))"

private definition ℐ_usr_core :: "('msg sec.iusr, 'msg sec.ousr) "
  where "ℐ_usr_core  ℐ_uniform (sec.Inp_Send ` (carrier )) UNIV  ℐ_uniform UNIV (sec.Out_Recv ` carrier )"

private definition invar_ideal' :: "((_ × 'msg astate × _) × _) × estate × 'msg sec.state  bool"
  where "invar_ideal' = pred_prod (pred_prod (pred_prod (λ_. True) (pred_prod (pred_option (λx. x  carrier )) (λ_. True))) (λ_. True)) (pred_prod (λ_. True) (pred_prod (sec.pred_s_kernel (λx. x  carrier )) (λ_. True)))"

private definition invar_real' :: "_ × ('msg key.s_kernel × _) × 'msg sec.s_kernel × _  bool"
  where "invar_real' = pred_prod (λ_. True) (pred_prod (pred_prod (key.pred_s_kernel (λx. x  carrier )) (λ_. True)) (pred_prod (sec.pred_s_kernel (λx. x  carrier )) (λ_. True)))"

lemma invar_ideal_s_core' [simp]: "invar_ideal' ideal_s_core'"
  by(simp add: invar_ideal'_def ideal_s_core'_def)

lemma invar_real_s_core' [simp]: "invar_real' real_s_core'"
  by(simp add: invar_real'_def real_s_core'_def)

lemma WT_ideal_core' [WT_intro]: "WT_core ℐ_adv_core ℐ_usr_core invar_ideal' ideal_core'"
  apply(rule WT_core.intros)
  apply                
    (auto split!: sum.splits option.splits if_split_asm simp add: ℐ_adv_core_def ℐ_usr_core_def exec_gpv_map_gpv_id exec_gpv_extend_state_oracle exec_gpv_plus_oracle_left exec_gpv_plus_oracle_right invar_ideal'_def sec.in_set_spmf_iface_drop sec.in_set_spmf_iface_look sec.in_set_spmf_iface_fedit sec.in_set_spmf_iface_alice sec.in_set_spmf_iface_bob id_oracle_def look_callee_def exec_gpv_bind set_spmf_of_set sec.poke_alt_def foldl_spmf_pair_right)
  done

lemma WT_ideal_rest' [WT_intro]:
  assumes "WT_rest ℐ_adv_restk ℐ_usr_restk I_key_rest key_rest"
    and "WT_rest ℐ_adv_resta ℐ_usr_resta I_auth_rest auth_rest"
  shows "WT_rest (ℐ_adv_restk  ℐ_adv_resta) (ℐ_usr_restk  ℐ_usr_resta) (λ(_, s_rest). pred_prod I_key_rest I_auth_rest s_rest) ideal_rest'"
  by(rule WT_rest.intros)(fastforce simp add: fused_resource.fuse.simps parallel_eoracle_def dest: WT_restD_rfunc_adv[OF assms(1)] WT_restD_rfunc_adv[OF assms(2)] WT_restD_rfunc_usr[OF assms(1)] WT_restD_rfunc_usr[OF assms(2)] simp add: assms[THEN WT_restD_rinit])+


lemma WT_real_core' [WT_intro]: "WT_core ℐ_adv_core ℐ_usr_core invar_real' real_core'"
  apply(rule WT_core.intros)
   apply(auto simp add: ℐ_adv_core_def ℐ_usr_core_def enc_callee_def dec_callee_def
        stateless_callee_def Let_def exec_gpv_extend_state_oracle exec_gpv_map_gpv' exec_gpv_plus_oracle_left exec_gpv_plus_oracle_right
        invar_real'_def in_set_spmf_parallel_handler key.in_set_spmf_poke sec.poke_alt_def auth.in_set_spmf_iface_look auth.in_set_spmf_iface_fedit
        sec.in_set_spmf_iface_alice sec.in_set_spmf_iface_bob
        split!: key.ousr_alice.splits key.ousr_bob.splits auth.ousr_alice.splits auth.ousr_bob.splits sum.splits if_split_asm)
    done

private lemma trace_eq_sec: 
    fixes ℐ_adv_restk ℐ_adv_resta ℐ_usr_restk ℐ_usr_resta 
  defines "outs_adv  (UNIV <+> UNIV <+> UNIV <+> sec.Inp_Fedit ` carrier ) <+> outs_ℐ (ℐ_adv_restk  ℐ_adv_resta)"
      and "outs_usr  (sec.Inp_Send ` carrier  <+> UNIV) <+> outs_ℐ (ℐ_usr_restk  ℐ_usr_resta)"
  assumes WT_key [WT_intro]: "WT_rest ℐ_adv_restk ℐ_usr_restk I_key_rest key_rest" 
      and WT_auth [WT_intro]: "WT_rest ℐ_adv_resta ℐ_usr_resta I_auth_rest auth_rest"
    shows "(outs_adv <+> outs_usr) C fused_resource.fuse ideal_core' ideal_rest' ((ideal_s_core', ideal_s_rest'))  
      fused_resource.fuse real_core' real_rest' ((real_s_core', real_s_rest'))"
proof -
  define eℐ_adv_rest :: "(_, _ × (key.event + auth.event) list) "
    where "eℐ_adv_rest  map_ℐ id (case_sum (map_prod Inl (map Inl)) (map_prod Inr (map Inr))) (eℐ ℐ_adv_restk  eℐ ℐ_adv_resta)"
  define eℐ_usr_rest :: "(_, _ × (key.event + auth.event) list) "
    where "eℐ_usr_rest  map_ℐ id (case_sum (map_prod Inl (map Inl)) (map_prod Inr (map Inr))) (eℐ ℐ_usr_restk  eℐ ℐ_usr_resta)"

  note I_defs = ℐ_adv_core_def ℐ_usr_core_def
  note eI_defs = eℐ_adv_rest_def eℐ_usr_rest_def 

  have fact1[unfolded outs_plus_ℐ]: 
    "trace_rest_eq ideal_rest' ideal_rest' (outs_ℐ (ℐ_adv_restk  ℐ_adv_resta)) (outs_ℐ (ℐ_usr_restk  ℐ_usr_resta)) s s" for s
    apply(rule rel_rest'_into_trace_rest_eq[where S="(=)" and M="(=)", unfolded eq_onp_def], simp_all)
    apply(fold relator_eq)
    apply(rule rel_rest'_mono[THEN predicate2D, rotated -1, OF HOL.refl[of ideal_rest', folded relator_eq]])
    by auto

  have fact2 [unfolded eI_defs]: "callee_invariant_on (callee_of_rest ideal_rest') (λ(_, s_rest). pred_prod I_key_rest I_auth_rest s_rest) (eℐ_adv_rest  eℐ_usr_rest)"
    apply unfold_locales
    subgoal for s x y s'
      apply(cases "(snd s, x)" rule: parallel_oracle.cases)
       apply(auto 4 3 simp add: parallel_eoracle_def eI_defs split!: sum.splits dest: WT_restD(1,2)[OF WT_key] WT_restD(1,2)[OF WT_auth])
      done
    subgoal for s
      apply(fastforce intro!: WT_calleeI simp add: parallel_eoracle_def eI_defs image_image dest: WT_restD(1,2)[OF WT_key] WT_restD(1,2)[OF WT_auth] intro: rev_image_eqI)
      done
    done

  have fact3[unfolded I_defs]: "callee_invariant_on (callee_of_core ideal_core') invar_ideal' (ℐ_full  (ℐ_adv_core  ℐ_usr_core))"
    by(rule WT_intro)+

  have fact4[unfolded I_defs]: "callee_invariant_on (callee_of_core real_core') invar_real' (ℐ_full  (ℐ_adv_core  ℐ_usr_core))"
    by(rule WT_intro)+

  note nempty_carrier[simp]
  show ?thesis using WT_key[THEN WT_restD_rinit] WT_auth[THEN WT_restD_rinit]
    apply (simp add: real_rest'_def real_s_rest'_def assms(1, 2))
    thm fuse_trace_eq[where ℐE=ℐ_full and ℐCA=ℐ_adv_core and ℐCU=ℐ_usr_core and ℐRA=eℐ_adv_rest and ℐRU=eℐ_usr_rest,unfolded eI_defs ℐ_adv_core_def ℐ_usr_core_def,simplified]
    apply (rule fuse_trace_eq[where ℐE=ℐ_full and ℐCA=ℐ_adv_core and ℐCU=ℐ_usr_core and ℐRA=eℐ_adv_rest and ℐRU=eℐ_usr_rest
      and ?IR1.0 = "λ(_, s_rest). pred_prod I_key_rest I_auth_rest s_rest"
      and ?IR2.0 = "λ(_, s_rest). pred_prod I_key_rest I_auth_rest s_rest"
      and ?IC1.0 = invar_ideal' and ?IC2.0=invar_real',
      unfolded eI_defs ℐ_adv_core_def ℐ_usr_core_def, simplified])
    by (simp_all add: trace_eq_core fact1 fact2 fact3 fact4 ideal_s_rest'_def)
qed


subsubsection ‹Simplifying the final resource by moving the interfaces from core to rest›


lemma connect[unfolded ℐ_adv_core_def ℐ_usr_core_def]:
    fixes ℐ_adv_restk ℐ_adv_resta ℐ_usr_restk ℐ_usr_resta 
  defines "  (ℐ_adv_core  (ℐ_adv_restk  ℐ_adv_resta))  (ℐ_usr_core  (ℐ_usr_restk  ℐ_usr_resta))"
  assumes [WT_intro]: "WT_rest ℐ_adv_restk ℐ_usr_restk I_key_rest key_rest" 
      and [WT_intro]: "WT_rest ℐ_adv_resta ℐ_usr_resta I_auth_rest auth_rest"
      and "exception_ℐ  ⊢g D "
    shows "connect D (obsf_resource ideal_resource) = connect D (obsf_resource real_resource)"
proof -
  note I_defs = ℐ_adv_core_def ℐ_usr_core_def

  have fact1: " ⊢res RES (fused_resource.fuse ideal_core' ideal_rest') s " 
    if "pred_prod I_key_rest I_auth_rest (snd (snd s))" "invar_ideal' (fst s)"
    for s
    unfolding assms(1)
    apply(rule callee_invariant_on.WT_resource_of_oracle[where I="pred_prod invar_ideal' (λ(_, s_rest). pred_prod I_key_rest I_auth_rest s_rest)"])
    subgoal by(rule fused_resource.callee_invariant_on_fuse)(rule WT_intro)+
    subgoal using that by(cases s)(simp)
    done

  have fact2: " ⊢res RES (fused_resource.fuse real_core' real_rest') s " 
    if "pred_prod I_key_rest I_auth_rest (snd (snd s))" "invar_real' (fst s)"
    for s
    unfolding real_rest'_def assms(1)
    apply(rule callee_invariant_on.WT_resource_of_oracle[where I="pred_prod invar_real' (λ(_, s_rest). pred_prod I_key_rest I_auth_rest s_rest)"])
    subgoal by(rule fused_resource.callee_invariant_on_fuse)(rule WT_intro)+
    subgoal using that by(cases s)(simp)
    done

  show ?thesis
    unfolding attach_ideal attach_real
    apply (rule connect_cong_trace[where="exception_ℐ "])
    apply (rule trace_eq_obsf_resourceI, subst trace_eq'_resource_of_oracle)
    apply (rule trace_eq_sec[OF assms(2) assms(3)])
    subgoal by (rule assms(4))
    subgoal using WT_gpv_outs_gpv[OF assms(4)] by(simp add: I_defs assms(1) nempty_carrier)
    subgoal using assms(2,3)[THEN WT_restD_rinit] by (intro WT_obsf_resource)(rule fact1; simp add: ideal_s_rest'_def)
    subgoal using assms(2,3)[THEN WT_restD_rinit] by (intro WT_obsf_resource)(rule fact2; simp add: real_s_rest'_def ideal_s_rest'_def)
    done
qed

end

end


end


subsection ‹Concrete security›

context one_time_pad begin

lemma WT_enc_callee [WT_intro]:
  "ℐ_uniform (sec.Inp_Send ` carrier ) UNIV, ℐ_uniform UNIV (key.Out_Alice ` carrier )   ℐ_uniform (sec.Inp_Send ` carrier ) UNIV C CNV enc_callee () "
  by (rule WT_converter_of_callee) (auto 4 3 simp add: enc_callee_def stateless_callee_def image_def split!: key.ousr_alice.split)

lemma WT_dec_callee [WT_intro]:
  "ℐ_uniform UNIV (sec.Out_Recv ` carrier ), ℐ_uniform UNIV (key.Out_Bob ` carrier )  ℐ_uniform UNIV (sec.Out_Recv ` carrier ) C CNV dec_callee () "
  by(rule WT_converter_of_callee)(auto simp add: dec_callee_def stateless_callee_def split!: sec.ousr_bob.splits)

lemma pfinite_enc_callee [pfinite_intro]: 
   "pfinite_converter (ℐ_uniform (sec.Inp_Send ` carrier ) UNIV) (ℐ_uniform UNIV (key.Out_Alice ` carrier )  ℐ_uniform (sec.Inp_Send ` carrier ) UNIV) (CNV enc_callee ())"
  apply(rule raw_converter_invariant.pfinite_converter_of_callee[where I="λ_. True"])
  subgoal by unfold_locales(auto simp add: enc_callee_def stateless_callee_def)
  subgoal by(auto simp add: enc_callee_def stateless_callee_def)
  subgoal by simp
  done

lemma pfinite_dec_callee [pfinite_intro]:
  "pfinite_converter (ℐ_uniform UNIV (sec.Out_Recv ` carrier )) (ℐ_uniform UNIV (key.Out_Bob ` carrier )  ℐ_uniform UNIV (sec.Out_Recv ` carrier )) (CNV dec_callee ())"
  apply(rule raw_converter_invariant.pfinite_converter_of_callee[where I="λ_. True"])
  subgoal by unfold_locales(auto simp add: dec_callee_def stateless_callee_def)
  subgoal by(auto simp add: dec_callee_def stateless_callee_def)
  subgoal by simp
  done

context 
  fixes 
    key_rest :: "('key_s_rest, key.event, 'key_iadv_rest, 'key_iusr_rest, 'key_oadv_rest, 'key_ousr_rest) rest_wstate" and
    auth_rest :: "('auth_s_rest, auth.event, 'auth_iadv_rest, 'auth_iusr_rest, 'auth_oadv_rest, 'auth_ousr_rest) rest_wstate" and
    ℐ_adv_restk and ℐ_adv_resta and ℐ_usr_restk and ℐ_usr_resta and I_key_rest and I_auth_rest
  assumes 
    WT_key_rest [WT_intro]: "WT_rest ℐ_adv_restk ℐ_usr_restk I_key_rest key_rest" and 
    WT_auth_rest [WT_intro]: "WT_rest ℐ_adv_resta ℐ_usr_resta I_auth_rest auth_rest"
begin

theorem secure:
  defines "ℐ_real  ((ℐ_full  (ℐ_full  (ℐ_full  ℐ_uniform (sec.Inp_Fedit ` (carrier )) UNIV)))  (ℐ_adv_restk  ℐ_adv_resta))" 
      and "ℐ_common_core  ℐ_uniform (sec.Inp_Send ` (carrier )) UNIV  ℐ_uniform UNIV (sec.Out_Recv ` carrier )"
      and "ℐ_common_rest  ℐ_usr_restk  ℐ_usr_resta"
      and "ℐ_ideal  (ℐ_full  (ℐ_full  ℐ_uniform (sec.Inp_Fedit ` (carrier )) UNIV))  (ℐ_adv_restk  ℐ_adv_resta)" 
    shows "constructive_security_obsf (real_resource TYPE(_) TYPE(_) key_rest auth_rest) (sec.resource (ideal_rest key_rest auth_rest)) (sim |= 1C) ℐ_real ℐ_ideal (ℐ_common_core  ℐ_common_rest) 𝒜 0" 
proof
  let ?ℐ_common = "ℐ_common_core  ℐ_common_rest"
  show "ℐ_real  ?ℐ_common ⊢res real_resource TYPE(_) TYPE(_) key_rest auth_rest "
    unfolding ℐ_real_def ℐ_common_core_def ℐ_common_rest_def real_resource_def attach_c1f22_c1f22_def wiring_c1r22_c1r22_def fused_wiring_def
    by(rule WT_intro | simp )+

  show [WT_intro]: "ℐ_ideal  ?ℐ_common ⊢res sec.resource (ideal_rest key_rest auth_rest) "
    unfolding ℐ_common_core_def ℐ_common_rest_def ℐ_ideal_def ideal_rest_def
    by(rule WT_intro)+ simp

  show [WT_intro]: "ℐ_real, ℐ_ideal C sim |= 1C " 
    unfolding ℐ_real_def ℐ_ideal_def
    apply(rule WT_intro)+
    subgoal
      unfolding sim_def Let_def look_callee_def
      apply (fold conv_callee_parallel_id_right[where s'="()"])
      apply (fold conv_callee_parallel_id_left[where s="()"])
      apply (subst ldummy_converter_of_callee)
      apply (rule WT_converter_of_callee)
       by (auto simp add: id_oracle_def map_gpv_conv_bind[symmetric] map_lift_spmf
          split: auth.oadv_look.split option.split )
    by (rule WT_intro)

  show "pfinite_converter ℐ_real ℐ_ideal (sim |= 1C)"
    unfolding ℐ_real_def ℐ_ideal_def
    apply(rule pfinite_intro)+
    subgoal 
      unfolding sim_def Let_def look_callee_def
      apply (fold conv_callee_parallel_id_right[where s'="()"])
      apply (fold conv_callee_parallel_id_left[where s="()"])
      apply (subst ldummy_converter_of_callee)
      apply(rule raw_converter_invariant.pfinite_converter_of_callee[where I="λ_. True"])
      subgoal 
        by unfold_locales (auto split!: sum.split sec.oadv_look.split option.split 
            simp add: left_gpv_map id_oracle_def intro!: WT_intro WT_gpv_right_gpv WT_gpv_left_gpv)
      by (auto split!: sum.splits sec.oadv_look.splits option.splits)
    by (rule pfinite_intro)

  assume WT [WT_intro]: "exception_ℐ (ℐ_real  ?ℐ_common) ⊢g 𝒜 "
  show "advantage 𝒜 (obsf_resource ((sim |= 1C) |= (1C |= 1C)  sec.resource (ideal_rest key_rest auth_rest)))
    (obsf_resource (real_resource TYPE(_) TYPE(_) key_rest auth_rest))  0"
    using connect[OF WT_key_rest, OF WT_auth_rest, OF WT[unfolded assms(1, 2, 3)]]
    unfolding advantage_def by (simp add: ideal_resource_def)
qed simp

end

end


subsection ‹Asymptotic security›

locale one_time_pad' =
  fixes  :: "security  ('msg, 'more) boolean_algebra_scheme"
  assumes one_time_pad [locale_witness]: "η. one_time_pad ( η)"
begin

sublocale one_time_pad " η" for η ..

definition real_resource' where "real_resource' rest1 rest2 η = real_resource TYPE(_) TYPE(_) η (rest1 η) (rest2 η)"
definition ideal_resource' where "ideal_resource' rest1 rest2 η = sec.resource η (ideal_rest (rest1 η) (rest2 η))"
definition sim' where "sim' η = (sim |= 1C)"

context 
  fixes 
    key_rest :: "nat  ('key_s_rest, key.event, 'key_iadv_rest, 'key_iusr_rest, 'key_oadv_rest, 'key_ousr_rest) rest_wstate" and
    auth_rest :: "nat  ('auth_s_rest, auth.event, 'auth_iadv_rest, 'auth_iusr_rest, 'auth_oadv_rest, 'auth_ousr_rest) rest_wstate" and
    ℐ_adv_restk and ℐ_adv_resta and ℐ_usr_restk and ℐ_usr_resta and I_key_rest and I_auth_rest
  assumes 
    WT_key_res: "η. WT_rest (ℐ_adv_restk η) (ℐ_usr_restk η) (I_key_rest η) (key_rest η)" and 
    WT_auth_rest: "η. WT_rest (ℐ_adv_resta η) (ℐ_usr_resta η) (I_auth_rest η) (auth_rest η)"
begin

theorem secure':
  defines "ℐ_real  λη. ((ℐ_full  (ℐ_full  (ℐ_full  ℐ_uniform (sec.Inp_Fedit ` (carrier ( η))) UNIV)))  (ℐ_adv_restk η  ℐ_adv_resta η))"
      and "ℐ_common  λη. ((ℐ_uniform (sec.Inp_Send ` (carrier ( η))) UNIV  ℐ_uniform UNIV (sec.Out_Recv ` carrier ( η)))  (ℐ_usr_restk η  ℐ_usr_resta η))"
      and "ℐ_ideal  λη. (ℐ_full  (ℐ_full  ℐ_uniform (sec.Inp_Fedit ` (carrier ( η))) UNIV))  (ℐ_adv_restk η  ℐ_adv_resta η)" 
    shows "constructive_security_obsf' (real_resource' key_rest auth_rest) (ideal_resource' key_rest auth_rest) sim' ℐ_real ℐ_ideal ℐ_common 𝒜"
proof(rule constructive_security_obsf'I)
  show "constructive_security_obsf (real_resource' key_rest auth_rest η) (ideal_resource' key_rest auth_rest η)
          (sim' η) (ℐ_real η) (ℐ_ideal η) (ℐ_common η) (𝒜 η) 0" for η
    unfolding real_resource'_def ideal_resource'_def sim'_def ℐ_real_def ℐ_common_def ℐ_ideal_def
    by(rule secure)(rule WT_key_res WT_auth_rest)+
qed simp

end


end

end