Theory Secure_Channel

section ‹Secure composition: Encrypt then MAC›

theory Secure_Channel imports
  One_Time_Pad
  Message_Authentication_Code
begin

context begin
interpretation INSEC: insec_channel .

interpretation MAC: macode "rnd η" "mac η" for η . 
interpretation AUTH: auth_channel . 

interpretation CIPHER: cipher "key η" "enc η" "dec η" for η . 
interpretation SEC: sec_channel .

lemma plossless_enc [plossless_intro]:
  "plossless_converter (ℐ_uniform (nlists UNIV η) UNIV) (ℐ_uniform UNIV (nlists UNIV η) ⊕⇩ℐ ℐ_uniform (nlists UNIV η) UNIV) (CIPHER.enc η)"
  unfolding CIPHER.enc_def
  by(rule plossless_converter_of_callee) (auto simp add: stateless_callee_def enc_def in_nlists_UNIV)

lemma plossless_dec [plossless_intro]:
  "plossless_converter (ℐ_uniform UNIV (insert None (Some ` nlists UNIV η))) (ℐ_uniform UNIV (nlists UNIV η) ⊕⇩ℐ ℐ_uniform UNIV (insert None (Some ` nlists UNIV η))) (CIPHER.dec η)"
  unfolding CIPHER.dec_def
  by(rule plossless_converter_of_callee) (auto simp add: stateless_callee_def dec_def in_nlists_UNIV split: option.split)

lemma callee_invariant_on_key_oracle:
  "callee_invariant_on
     (CIPHER.KEY.key_oracle η ⊕⇩O CIPHER.KEY.key_oracle η)
     (λx. case x of None ⇒ True | Some x' ⇒ length x' = η)
     (ℐ_uniform UNIV (nlists UNIV η) ⊕⇩ℐ ℐ_full)"
proof(unfold_locales, goal_cases)
  case (1 s x y s')
  then show ?case by(cases x; clarsimp split: option.splits; simp add: key_def in_nlists_UNIV)
next
  case (2 s)
  then show ?case by(clarsimp intro!: WT_calleeI split: option.split_asm)(simp_all add: in_nlists_UNIV key_def)
qed

interpretation key: callee_invariant_on
  "CIPHER.KEY.key_oracle η ⊕⇩O CIPHER.KEY.key_oracle η"
  "λx. case x of None ⇒ True | Some x' ⇒ length x' = η"
  "ℐ_uniform UNIV (nlists UNIV η) ⊕⇩ℐ ℐ_full" for η
  by(rule callee_invariant_on_key_oracle)

lemma WT_enc [WT_intro]: "ℐ_uniform (nlists UNIV η) UNIV,
  ℐ_uniform UNIV (nlists UNIV η) ⊕⇩ℐ ℐ_uniform (vld η) UNIV ⊢⇩C CIPHER.enc η √"
  unfolding CIPHER.enc_def
  by (rule WT_converter_of_callee) (simp_all add: stateless_callee_def vld_def enc_def in_nlists_UNIV)

lemma WT_dec [WT_intro]: "ℐ_uniform UNIV (insert None (Some ` nlists UNIV η)),
    ℐ_uniform UNIV (nlists UNIV η) ⊕⇩ℐ ℐ_uniform UNIV (insert None (Some ` vld η)) ⊢⇩C
    CIPHER.dec η √"
  unfolding CIPHER.dec_def
  by(rule WT_converter_of_callee)(auto simp add: stateless_callee_def dec_def vld_def in_nlists_UNIV)

lemma bound_enc [interaction_bound]: "interaction_any_bounded_converter (CIPHER.enc η) (enat 2)"
  unfolding CIPHER.enc_def
  by (rule interaction_any_bounded_converter_of_callee) 
    (auto simp add: stateless_callee_def map_gpv_id_bind_gpv zero_enat_def one_enat_def)

lemma bound_dec [interaction_bound]: "interaction_any_bounded_converter (CIPHER.dec η) (enat 2)"
  unfolding CIPHER.dec_def
  by (rule interaction_any_bounded_converter_of_callee)
    (auto simp add: stateless_callee_def map_gpv_id_bind_gpv zero_enat_def one_enat_def split: sum.split option.split)

theorem mac_otp:
  defines "ℐ_real ≡ λη. ℐ_uniform {x. valid_mac_query η x} UNIV"
    and "ℐ_ideal ≡ λ_. ℐ_full"
    and "ℐ_common ≡ λη. ℐ_uniform (vld η) UNIV ⊕⇩ℐ ℐ_full"
  shows
    "constructive_security
      (λη. 1⇩C |⇩= (CIPHER.enc η |⇩= CIPHER.dec η) ⊙ parallel_wiring ⊳
            parallel_resource1_wiring ⊳
            CIPHER.KEY.res η ∥
            (1⇩C |⇩= MAC.enm η |⇩= MAC.dem η ⊳
             1⇩C |⇩= parallel_wiring ⊳
             parallel_resource1_wiring ⊳ MAC.RO.res η ∥ INSEC.res))
      (λ_. SEC.res)
      (λη. CNV Message_Authentication_Code.sim (Inl None) ⊙ CNV One_Time_Pad.sim None)
      (λη. ℐ_uniform (Set.Collect (valid_mac_query η)) (insert None (Some ` (nlists UNIV η × nlists UNIV η))))
      (λη. ℐ_uniform UNIV {None, Some η})
      (λη. ℐ_uniform (nlists UNIV η) UNIV ⊕⇩ℐ ℐ_uniform UNIV (insert None (Some ` nlists UNIV η)))
      (λ_. enat q) True (λη. (id, map_option length) ∘⇩w (insec_query_of, map_option snd))"
proof(rule composability[OF one_time_pad[THEN constructive_security2.constructive_security, unfolded CIPHER.res_alt_def comp_converter_parallel2 comp_converter_id_left]
  secure_mac[unfolded MAC.res_def, 
        THEN constructive_security.parallel_resource1,
        THEN constructive_security.lifting],
      where ?ℐ_res2="λη. ℐ_uniform UNIV (nlists UNIV η) ⊕⇩ℐ ℐ_uniform UNIV (nlists UNIV η)" and ?bound_conv1="λ_. 2" and ?q3 = "2 * q" and bound_sim = "λ_. ∞",
simplified]
    , goal_cases)
  case (1 η)
  have [simp]: "ℐ_uniform UNIV (nlists UNIV η) ⊢c CIPHER.KEY.key_oracle η s √"
    if "pred_option (λx. length x = η) s" for s η
    apply(rule WT_calleeI)
    subgoal for call using that by(cases s; cases call; clarsimp; auto simp add: key_def in_nlists_UNIV)
    done
  have *: "callee_invariant_on (CIPHER.KEY.key_oracle η ⊕⇩O CIPHER.KEY.key_oracle η) (pred_option (λx. length x = η))
     (ℐ_uniform UNIV (nlists UNIV η) ⊕⇩ℐ ℐ_uniform UNIV (nlists UNIV η))" for η
    apply(unfold_locales)
    subgoal for s x y s' by(cases s; cases x; clarsimp; auto simp add: key_def in_nlists_UNIV)
    subgoal for s by auto
    done
  then show ?case unfolding CIPHER.KEY.res_def
    by(rule callee_invariant_on.WT_resource_of_oracle) simp

  case (2 η)
  show ?case 
    unfolding CIPHER.KEY.res_def
    apply(rule callee_invariant_on.lossless_resource_of_oracle[OF *])
    subgoal for s x by(cases s; cases x)(auto split: plus_oracle_split; simp add: key_def)+
    subgoal by simp
    done

  case (3 η)
  show ?case by(rule WT_intro)+

  case (4 η)
  show ?case by interaction_bound_converter code_simp

  case (5 η)
  show ?case by (simp add: mult_2_right)

  case (6 η)
  show ?case unfolding vld_def by(rule plossless_intro WT_intro[unfolded vld_def])+
qed

end

end