Theory PRF_IND_CPA

(* Title: PRF_IND_CPA.thy
  Author: Andreas Lochbihler, ETH Zurich *)

subsection ‹IND-CPA from PRF›

theory PRF_IND_CPA imports
  CryptHOL.GPV_Bisim
  CryptHOL.List_Bits
  Pseudo_Random_Function
  IND_CPA
begin

text ‹
  Formalises the construction from cite"PetcherMorrisett2015POST".
›

declare [[simproc del: let_simp]]

type_synonym key = "bool list"
type_synonym plain = "bool list"
type_synonym cipher = "bool list * bool list"

locale otp =
  fixes f :: "key  bool list  bool list"
  and len :: nat
  assumes length_f: "xs ys.  length xs = len; length ys = len   length (f xs ys) = len"
begin

definition key_gen :: "bool list spmf"
where "key_gen = spmf_of_set (nlists UNIV len)"

definition valid_plain :: "plain  bool"
where "valid_plain plain  length plain = len"

definition encrypt :: "key  plain  cipher spmf"
where
  "encrypt key plain = do {
     r  spmf_of_set (nlists UNIV len);
     return_spmf (r, xor_list plain (f key r))
   }"

fun decrypt :: "key  cipher  plain option"
where "decrypt key (r, c) = Some (xor_list (f key r) c)"

lemma encrypt_decrypt_correct:
  " length key = len; length plain = len 
   encrypt key plain  (λcipher. return_spmf (decrypt key cipher)) = return_spmf (Some plain)"
by(simp add: encrypt_def zip_map2 o_def split_def bind_eq_return_spmf length_f in_nlists_UNIV xor_list_left_commute)

interpretation ind_cpa: ind_cpa key_gen encrypt decrypt valid_plain .
interpretation "prf": "prf" key_gen f "spmf_of_set (nlists UNIV len)" .

definition prf_encrypt_oracle :: "unit  plain  (cipher × unit, plain, plain) gpv"
where
  "prf_encrypt_oracle x plain = do {
     r  lift_spmf (spmf_of_set (nlists UNIV len));
     Pause r (λpad. Done ((r, xor_list plain pad), ()))
  }"

lemma interaction_bounded_by_prf_encrypt_oracle [interaction_bound]:
  "interaction_any_bounded_by (prf_encrypt_oracle σ plain) 1"
unfolding prf_encrypt_oracle_def by simp

lemma lossless_prf_encyrpt_oracle [simp]: "lossless_gpv ℐ_top (prf_encrypt_oracle s x)"
by(simp add: prf_encrypt_oracle_def)

definition prf_adversary :: "(plain, cipher, 'state) ind_cpa.adversary  (plain, plain) prf.adversary"
where
  "prf_adversary 𝒜 = do {
     let (𝒜1, 𝒜2) = 𝒜;
     (((p1, p2), σ), n)  inline prf_encrypt_oracle 𝒜1 ();
     if valid_plain p1  valid_plain p2 then do { 
       b  lift_spmf coin_spmf;
       let pb = (if b then p1 else p2);
       r  lift_spmf (spmf_of_set (nlists UNIV len));
       pad  Pause r Done;
       let c = (r, xor_list pb pad);
       (b', _)  inline prf_encrypt_oracle (𝒜2 c σ) n;
       Done (b' = b)
     } else lift_spmf coin_spmf
  }"

theorem prf_encrypt_advantage:
  assumes "ind_cpa.ibounded_by 𝒜 q"
  and "lossless_gpv ℐ_full (fst 𝒜)"
  and "cipher σ. lossless_gpv ℐ_full (snd 𝒜 cipher σ)"
  shows "ind_cpa.advantage 𝒜  prf.advantage (prf_adversary 𝒜) + q / 2 ^ len"
proof -
  note [split del] = if_split
    and [cong del] = if_weak_cong
    and [simp] =
      bind_spmf_const map_spmf_bind_spmf bind_map_spmf 
      exec_gpv_bind exec_gpv_inline
      rel_spmf_bind_reflI rel_spmf_reflI
  obtain 𝒜1 𝒜2 where 𝒜: "𝒜 = (𝒜1, 𝒜2)" by(cases "𝒜")
  from ind_cpa.ibounded_by _ _
  obtain q1 q2 :: nat
    where q1: "interaction_any_bounded_by 𝒜1 q1"
    and q2: "cipher σ. interaction_any_bounded_by (𝒜2 cipher σ) q2"
    and "q1 + q2  q"
    unfolding 𝒜 by(rule ind_cpa.ibounded_byE)(auto simp add: iadd_le_enat_iff)
  from 𝒜 assms have lossless1: "lossless_gpv ℐ_full 𝒜1"
    and lossless2: "cipher σ. lossless_gpv ℐ_full (𝒜2 cipher σ)" by simp_all
  have weight1: "oracle s. (s x. lossless_spmf (oracle s x)) 
     weight_spmf (exec_gpv oracle 𝒜1 s) = 1"
    by(rule lossless_weight_spmfD)(rule lossless_exec_gpv[OF lossless1], simp_all)
  have weight2: "oracle s cipher σ. (s x. lossless_spmf (oracle s x)) 
     weight_spmf (exec_gpv oracle (𝒜2 cipher σ) s) = 1"
    by(rule lossless_weight_spmfD)(rule lossless_exec_gpv[OF lossless2], simp_all)

  let ?oracle1 = "λkey (s', s) y. map_spmf (λ((x, s'), s). (x, (), ())) (exec_gpv (prf.prf_oracle key) (prf_encrypt_oracle () y) ())"
  have bisim1: "key. rel_spmf (λ(x, _) (y, _). x = y)
          (exec_gpv (ind_cpa.encrypt_oracle key) 𝒜1 ())
          (exec_gpv (?oracle1 key) 𝒜1 ((), ()))"
    using TrueI
    by(rule exec_gpv_oracle_bisim)(auto simp add: encrypt_def prf_encrypt_oracle_def ind_cpa.encrypt_oracle_def prf.prf_oracle_def o_def)
  have bisim2: "key cipher σ. rel_spmf (λ(x, _) (y, _). x = y)
             (exec_gpv (ind_cpa.encrypt_oracle key) (𝒜2 cipher σ) ())
             (exec_gpv (?oracle1 key) (𝒜2 cipher σ) ((), ()))"
    using TrueI
    by(rule exec_gpv_oracle_bisim)(auto simp add: encrypt_def prf_encrypt_oracle_def ind_cpa.encrypt_oracle_def prf.prf_oracle_def o_def)
   
  have ind_cpa_0: "rel_spmf (=) (ind_cpa.ind_cpa 𝒜) (prf.game_0 (prf_adversary 𝒜))"
    unfolding IND_CPA.ind_cpa.ind_cpa_def 𝒜 key_gen_def Let_def prf_adversary_def Pseudo_Random_Function.prf.game_0_def
    apply(simp)
    apply(rewrite in "bind_spmf _ " bind_commute_spmf)
    apply(rule rel_spmf_bind_reflI)
    apply(rule rel_spmf_bindI[OF bisim1])
    apply(clarsimp simp add: if_distribs bind_coin_spmf_eq_const')
    apply(auto intro: rel_spmf_bindI[OF bisim2] intro!: rel_spmf_bind_reflI simp add: encrypt_def prf.prf_oracle_def cong del: if_cong)
    done

  define rf_encrypt where "rf_encrypt = (λs plain. bind_spmf (spmf_of_set (nlists UNIV len)) (λr :: bool list. 
    bind_spmf (prf.random_oracle s r) (λ(pad, s'). 
    return_spmf ((r, xor_list plain pad), s')))
  )"
  interpret rf_finite: callee_invariant_on rf_encrypt "λs. finite (dom s)" ℐ_full
    by unfold_locales(auto simp add: rf_encrypt_def dest: prf.finite.callee_invariant)
  have lossless_rf_encrypt [simp]: "s plain. lossless_spmf (rf_encrypt s plain)"
    by(auto simp add: rf_encrypt_def)

  define game2 where "game2 = do {
    (((p0, p1), σ), s1)  exec_gpv rf_encrypt 𝒜1 Map.empty;
    if valid_plain p0  valid_plain p1 then do {
      b  coin_spmf;
      let pb = (if b then p0 else p1);
      (cipher, s2)  rf_encrypt s1 pb;
      (b', s3)  exec_gpv rf_encrypt (𝒜2 cipher σ) s2;
      return_spmf (b' = b)
    } else coin_spmf
  }"

  let ?oracle2 = "λ(s', s) y. map_spmf (λ((x, s'), s). (x, (), s)) (exec_gpv prf.random_oracle (prf_encrypt_oracle () y) s)"
  let ?I = "λ(x, _, s) (y, s'). x = y  s = s'"
  have bisim1: "rel_spmf ?I (exec_gpv ?oracle2 𝒜1 ((), Map.empty)) (exec_gpv rf_encrypt 𝒜1 Map.empty)"
     by(rule exec_gpv_oracle_bisim[where X="λ(_, s) s'. s = s'"])
       (auto simp add: rf_encrypt_def prf_encrypt_oracle_def intro!: rel_spmf_bind_reflI)
  have bisim2: "cipher σ s. rel_spmf ?I (exec_gpv ?oracle2 (𝒜2 cipher σ) ((), s)) (exec_gpv rf_encrypt (𝒜2 cipher σ) s)"
    by(rule exec_gpv_oracle_bisim[where X="λ(_, s) s'. s = s'"])
      (auto simp add: prf_encrypt_oracle_def rf_encrypt_def intro!: rel_spmf_bind_reflI)
  have game1_2 [unfolded spmf_rel_eq]: "rel_spmf (=) (prf.game_1 (prf_adversary 𝒜)) game2"
    unfolding prf.game_1_def game2_def prf_adversary_def
    by(rewrite in "if _ then  else _" rf_encrypt_def)
      (auto simp add: Let_def 𝒜 if_distribs intro!: rel_spmf_bindI[OF bisim2] rel_spmf_bind_reflI rel_spmf_bindI[OF bisim1])

  define game2_a where "game2_a = do {
    r  spmf_of_set (nlists UNIV len);
    (((p0, p1), σ), s1)  exec_gpv rf_encrypt 𝒜1 Map.empty;
    let bad = r  dom s1;
    if valid_plain p0  valid_plain p1 then do {
      b  coin_spmf;
      let pb = (if b then p0 else p1);
      (pad, s2)  prf.random_oracle s1 r;
      let cipher = (r, xor_list pb pad);
      (b', s3)  exec_gpv rf_encrypt (𝒜2 cipher σ) s2;
      return_spmf (b' = b, bad)
    } else coin_spmf  (λb. return_spmf (b, bad))
  }"
  define game2_b where "game2_b = do {
    r  spmf_of_set (nlists UNIV len);
    (((p0, p1), σ), s1)  exec_gpv rf_encrypt 𝒜1 Map.empty;
    let bad = r  dom s1;
    if valid_plain p0  valid_plain p1 then do {
      b  coin_spmf;
      let pb = (if b then p0 else p1);
      pad  spmf_of_set (nlists UNIV len);
      let cipher = (r, xor_list pb pad);
      (b', s3)  exec_gpv rf_encrypt (𝒜2 cipher σ) (s1(r  pad));
      return_spmf (b' = b, bad)
    } else coin_spmf  (λb. return_spmf (b, bad))
  }"
  
  have "game2 = do {
      r  spmf_of_set (nlists UNIV len);
      (((p0, p1), σ), s1)  exec_gpv rf_encrypt 𝒜1 Map.empty;
      if valid_plain p0  valid_plain p1 then do {
        b  coin_spmf;
        let pb = (if b then p0 else p1);
        (pad, s2)  prf.random_oracle s1 r;
        let cipher = (r, xor_list pb pad);
        (b', s3)  exec_gpv rf_encrypt (𝒜2 cipher σ) s2;
        return_spmf (b' = b)
      } else coin_spmf
    }"
    including monad_normalisation by(simp add: game2_def split_def rf_encrypt_def Let_def)
  also have " = map_spmf fst game2_a" unfolding game2_a_def
    by(clarsimp simp add: map_spmf_conv_bind_spmf Let_def if_distribR if_distrib split_def cong: if_cong)
  finally have game2_2a: "game2 = "  .

  have "map_spmf snd game2_a = map_spmf snd game2_b" unfolding game2_a_def game2_b_def
    by(auto simp add: o_def Let_def split_def if_distribs weight2 split: option.split intro: bind_spmf_cong[OF refl])
  moreover
  have "rel_spmf (=) (map_spmf fst (game2_a  (snd -` {False}))) (map_spmf fst (game2_b  (snd -` {False})))"
    unfolding game2_a_def game2_b_def
    by(clarsimp simp add: restrict_bind_spmf o_def Let_def if_distribs split_def restrict_return_spmf prf.random_oracle_def intro!: rel_spmf_bind_reflI split: option.splits)
  hence "spmf game2_a (True, False) = spmf game2_b (True, False)" 
     unfolding spmf_rel_eq by(subst (1 2) spmf_map_restrict[symmetric]) simp
  ultimately
  have game2a_2b: "¦spmf (map_spmf fst game2_a) True - spmf (map_spmf fst game2_b) True¦  spmf (map_spmf snd game2_a) True"
    by(subst (1 2) spmf_conv_measure_spmf)(rule identical_until_bad; simp add: spmf.map_id[unfolded id_def] spmf_conv_measure_spmf)

  define game2_a_bad where "game2_a_bad = do {
      r  spmf_of_set (nlists UNIV len);
      (((p0, p1), σ), s1)  exec_gpv rf_encrypt 𝒜1 Map.empty;
      return_spmf (r  dom s1)
    }"
  have game2a_bad: "map_spmf snd game2_a = game2_a_bad"
    unfolding game2_a_def game2_a_bad_def
    by(auto intro!: bind_spmf_cong[OF refl] simp add: o_def weight2 Let_def split_def split: if_split)
  have card: "B :: bool list set. card (B  nlists UNIV len)  card (nlists UNIV len :: bool list set)"
    by(rule card_mono) simp_all
  then have "spmf game2_a_bad True = + x. card (dom (snd x)  nlists UNIV len) / 2 ^ len measure_spmf (exec_gpv rf_encrypt 𝒜1 Map.empty)" 
    unfolding game2_a_bad_def
    by(rewrite bind_commute_spmf)(simp add: ennreal_spmf_bind split_def map_mem_spmf_of_set[unfolded map_spmf_conv_bind_spmf] card_nlists)
  also { fix x s
    assume *: "(x, s)  set_spmf (exec_gpv rf_encrypt 𝒜1 Map.empty)"
    hence "finite (dom s)" by(rule rf_finite.exec_gpv_invariant) simp_all
    hence 1: "card (dom s  nlists UNIV len)  card (dom s)" by(intro card_mono) simp_all
    moreover from q1 *
    have "card (dom s)  q1 + card (dom (Map.empty :: (plain, plain) prf.dict))"
      by(rule rf_finite.interaction_bounded_by'_exec_gpv_count)
        (auto simp add: rf_encrypt_def eSuc_enat prf.random_oracle_def card_insert_if split: option.split_asm if_split)
    ultimately have "card (dom s  nlists UNIV len)  q1" by(simp) }
  then have "   + x. q1 / 2 ^ len measure_spmf (exec_gpv rf_encrypt 𝒜1 Map.empty)"
    by(intro nn_integral_mono_AE)(clarsimp simp add: field_simps)
  also have "  q1 / 2 ^ len"
    by(simp add: measure_spmf.emeasure_eq_measure field_simps mult_left_le weight1)
  finally have game2a_bad_bound: "spmf game2_a_bad True  q1 / 2 ^ len" by simp

  define rf_encrypt_bad
    where "rf_encrypt_bad = (λsecret (s :: (plain, plain) prf.dict, bad) plain. bind_spmf
     (spmf_of_set (nlists UNIV len)) (λr.
     bind_spmf (prf.random_oracle s r) (λ(pad, s').
     return_spmf ((r, xor_list plain pad), (s', bad  r = secret)))))"
  have rf_encrypt_bad_sticky [simp]: "s. callee_invariant (rf_encrypt_bad s) snd"
    by(unfold_locales)(auto simp add: rf_encrypt_bad_def)
  have lossless_rf_encrypt [simp]: "challenge s plain. lossless_spmf (rf_encrypt_bad challenge s plain)"
    by(clarsimp simp add: rf_encrypt_bad_def prf.random_oracle_def split: option.split)

  define game2_c where "game2_c = do {
    r  spmf_of_set (nlists UNIV len);
    (((p0, p1), σ), s1)  exec_gpv rf_encrypt 𝒜1 Map.empty;
    if valid_plain p0  valid_plain p1 then do {
      b  coin_spmf;
      let pb = (if b then p0 else p1);
      pad  spmf_of_set (nlists UNIV len);
      let cipher = (r, xor_list pb pad);
      (b', (s2, bad))  exec_gpv (rf_encrypt_bad r) (𝒜2 cipher σ) (s1(r  pad), False);
      return_spmf (b' = b, bad)
    } else coin_spmf  (λb. return_spmf (b, False))
  }"

  have bisim2c_bad: "cipher σ s x r. rel_spmf (λ(x, _) (y, _). x = y)
    (exec_gpv rf_encrypt (𝒜2 cipher σ) (s(x  r)))
    (exec_gpv (rf_encrypt_bad x) (𝒜2 cipher σ) (s(x  r), False))"
    by(rule exec_gpv_oracle_bisim[where X="λs (s', _). s = s'"])
      (auto simp add: rf_encrypt_bad_def rf_encrypt_def intro!: rel_spmf_bind_reflI)

  have game2b_c [unfolded spmf_rel_eq]: "rel_spmf (=) (map_spmf fst game2_b) (map_spmf fst game2_c)"
    by(auto simp add: game2_b_def game2_c_def o_def split_def Let_def if_distribs intro!: rel_spmf_bind_reflI rel_spmf_bindI[OF bisim2c_bad])

  define game2_d where "game2_d = do {
    r  spmf_of_set (nlists UNIV len);
    (((p0, p1), σ), s1)  exec_gpv rf_encrypt 𝒜1 Map.empty;
    if valid_plain p0  valid_plain p1 then do {
      b  coin_spmf;
      let pb = (if b then p0 else p1);
      pad  spmf_of_set (nlists UNIV len);
      let cipher = (r, xor_list pb pad);
      (b', (s2, bad))  exec_gpv (rf_encrypt_bad r) (𝒜2 cipher σ) (s1, False);
      return_spmf (b' = b, bad)
    } else coin_spmf  (λb. return_spmf (b, False))
  }"


  { fix cipher σ and x :: plain and s r
    let ?I = "(λ(x, s, bad) (y, s', bad'). (bad  bad')  (¬ bad'  x  y))"
    let ?X = "λ(s, bad) (s', bad'). bad = bad'  (z. z  x  s z = s' z)"
    have "s1 s2 x'. ?X s1 s2  rel_spmf (λ(a, s1') (b, s2'). snd s1' = snd s2'  (¬ snd s2'  a = b  ?X s1' s2'))
       (rf_encrypt_bad x s1 x') (rf_encrypt_bad x s2 x')"
      by(case_tac "x = x'")(clarsimp simp add: rf_encrypt_bad_def prf.random_oracle_def rel_spmf_return_spmf1 rel_spmf_return_spmf2 Let_def split_def bind_UNION intro!: rel_spmf_bind_reflI split: option.split)+
    with _ _ have "rel_spmf ?I
             (exec_gpv (rf_encrypt_bad x) (𝒜2 cipher σ) (s(x  r), False))
             (exec_gpv (rf_encrypt_bad x) (𝒜2 cipher σ) (s, False))"
      by(rule exec_gpv_oracle_bisim_bad_full)(auto simp add: lossless2) }
  note bisim_bad = this
  have game2c_2d_bad [unfolded spmf_rel_eq]: "rel_spmf (=) (map_spmf snd game2_c) (map_spmf snd game2_d)"
    by(auto simp add: game2_c_def game2_d_def o_def Let_def split_def if_distribs intro!: rel_spmf_bind_reflI rel_spmf_bindI[OF bisim_bad])
  moreover
  have "rel_spmf (=) (map_spmf fst (game2_c  (snd -` {False}))) (map_spmf fst (game2_d  (snd -` {False})))"
    unfolding game2_c_def game2_d_def
    by(clarsimp simp add: restrict_bind_spmf o_def Let_def if_distribs split_def restrict_return_spmf intro!: rel_spmf_bind_reflI rel_spmf_bindI[OF bisim_bad])
  hence "spmf game2_c (True, False) = spmf game2_d (True, False)"
    unfolding spmf_rel_eq by(subst (1 2) spmf_map_restrict[symmetric]) simp
  ultimately have game2c_2d: "¦spmf (map_spmf fst game2_c) True - spmf (map_spmf fst game2_d) True¦  spmf (map_spmf snd game2_c) True"
    apply(subst (1 2) spmf_conv_measure_spmf)
    apply(intro identical_until_bad) 
    apply(simp_all add: spmf.map_id[unfolded id_def] spmf_conv_measure_spmf)
    done
  { fix cipher σ and challenge :: plain and s
    have "card (nlists UNIV len  (λx. x = challenge) -` {True})  card {challenge}"
      by(rule card_mono) auto
    then have "spmf (map_spmf (snd  snd) (exec_gpv (rf_encrypt_bad challenge) (𝒜2 cipher σ) (s, False))) True  (1 / 2 ^ len) * q2"
      by(intro oi_True.interaction_bounded_by_exec_gpv_bad[OF q2])(simp_all add: rf_encrypt_bad_def o_def split_beta map_spmf_conv_bind_spmf[symmetric] spmf_map measure_spmf_of_set field_simps card_nlists)
    hence "(+ x. ennreal (indicator {True} x) measure_spmf (map_spmf (snd  snd) (exec_gpv (rf_encrypt_bad challenge) (𝒜2 cipher σ) (s, False))))  (1 / 2 ^ len) * q2"
      by(simp only: ennreal_indicator nn_integral_indicator sets_measure_spmf sets_count_space Pow_UNIV UNIV_I emeasure_spmf_single) simp }
  then have "spmf (map_spmf snd game2_d) True 
        + (r :: plain). + (((p0, p1), σ), s). (if valid_plain p0  valid_plain p1 then
             + b . + (pad :: plain). q2 / 2 ^ len measure_spmf (spmf_of_set (nlists UNIV len)) measure_spmf coin_spmf
              else 0)
           measure_spmf (exec_gpv rf_encrypt 𝒜1 Map.empty) measure_spmf (spmf_of_set (nlists UNIV len))"
      unfolding game2_d_def
      by(simp add: ennreal_spmf_bind o_def split_def Let_def if_distribs if_distrib[where f="λx. ennreal (spmf x _)"] indicator_single_Some nn_integral_mono if_mono_cong del: nn_integral_const cong: if_cong)
  also have "  + (r :: plain). + (((p0, p1), σ), s). (if valid_plain p0  valid_plain p1 then ennreal (q2 / 2 ^ len) else q2 / 2 ^ len)
                   measure_spmf (exec_gpv rf_encrypt 𝒜1 Map.empty) measure_spmf (spmf_of_set (nlists UNIV len))"
    unfolding split_def
    by(intro nn_integral_mono if_mono_cong)(auto simp add: measure_spmf.emeasure_eq_measure)
  also have "  q2 / 2 ^ len" by(simp add: split_def weight1 measure_spmf.emeasure_eq_measure)
  finally have game2_d_bad: "spmf (map_spmf snd game2_d) True  q2 / 2 ^ len" by simp

  define game3 where "game3 = do {
      (((p0, p1), σ), s1)  exec_gpv rf_encrypt 𝒜1 Map.empty;
      if valid_plain p0  valid_plain p1 then do {
        b  coin_spmf;
        let pb = (if b then p0 else p1);
        r  spmf_of_set (nlists UNIV len);
        pad  spmf_of_set (nlists UNIV len);
        let cipher = (r, xor_list pb pad);
        (b', s2)  exec_gpv rf_encrypt (𝒜2 cipher σ) s1;
        return_spmf (b' = b)
      } else coin_spmf
    }"
  have bisim2d_3: "cipher σ s r. rel_spmf (λ(x, _) (y, _). x = y)
             (exec_gpv (rf_encrypt_bad r) (𝒜2 cipher σ) (s, False))
             (exec_gpv rf_encrypt (𝒜2 cipher σ) s)"
    by(rule exec_gpv_oracle_bisim[where X="λ(s1, _) s2. s1 = s2"])(auto simp add: rf_encrypt_bad_def rf_encrypt_def intro!: rel_spmf_bind_reflI)
  have game2d_3: "rel_spmf (=) (map_spmf fst game2_d) game3"
    unfolding game2_d_def game3_def Let_def including monad_normalisation
    by(clarsimp simp add: o_def split_def if_distribs cong: if_cong intro!: rel_spmf_bind_reflI rel_spmf_bindI[OF bisim2d_3])

  have "¦spmf game2 True - 1 / 2¦ 
    ¦spmf (map_spmf fst game2_a) True - spmf (map_spmf fst game2_b) True¦ + ¦spmf (map_spmf fst game2_b) True - 1 / 2¦"
    unfolding game2_2a by(rule abs_diff_triangle_ineq2)
  also have "  q1 / 2 ^ len + ¦spmf (map_spmf fst game2_b) True - 1 / 2¦"
    using game2a_2b game2a_bad_bound unfolding game2a_bad by(intro add_right_mono) simp
  also have "¦spmf (map_spmf fst game2_b) True - 1 / 2¦ 
    ¦spmf (map_spmf fst game2_c) True - spmf (map_spmf fst game2_d) True¦ + ¦spmf (map_spmf fst game2_d) True - 1 / 2¦"
    unfolding game2b_c by(rule abs_diff_triangle_ineq2)
  also (add_left_mono_trans) have "  q2 / 2 ^ len + ¦spmf (map_spmf fst game2_d) True - 1 / 2¦"
    using game2c_2d game2_d_bad unfolding game2c_2d_bad by(intro add_right_mono) simp
  finally (add_left_mono_trans) 
  have game2: "¦spmf game2 True - 1 / 2¦  q1 / 2 ^ len + q2 / 2 ^ len +  ¦spmf game3 True - 1 / 2¦"
    using game2d_3 by(simp add: field_simps spmf_rel_eq)

  have "game3 = do {
      (((p0, p1), σ), s1)  exec_gpv rf_encrypt 𝒜1 Map.empty;
      if valid_plain p0  valid_plain p1 then do {
        b  coin_spmf;
        let pb = (if b then p0 else p1);
        r  spmf_of_set (nlists UNIV len);
        pad  map_spmf (xor_list pb) (spmf_of_set (nlists UNIV len));
        let cipher = (r, xor_list pb pad);
        (b', s2)  exec_gpv rf_encrypt (𝒜2 cipher σ) s1;
        return_spmf (b' = b)
      } else coin_spmf
    }"
    by(simp add: valid_plain_def game3_def Let_def one_time_pad del: bind_map_spmf map_spmf_of_set_inj_on cong: bind_spmf_cong_simp if_cong split: if_split)
  also have " = do {
       (((p0, p1), σ), s1)  exec_gpv rf_encrypt 𝒜1 Map.empty;
       if valid_plain p0  valid_plain p1 then do {
         b  coin_spmf;
         let pb = (if b then p0 else p1);
         r  spmf_of_set (nlists UNIV len);
         pad  spmf_of_set (nlists UNIV len);
         let cipher = (r, pad);
         (b', _)  exec_gpv rf_encrypt (𝒜2 cipher σ) s1;
         return_spmf (b' = b)
       } else coin_spmf
     }"
     by(simp add: game3_def Let_def valid_plain_def in_nlists_UNIV cong: bind_spmf_cong_simp if_cong split: if_split)
  also have " = do {
      (((p0, p1), σ), s1)  exec_gpv rf_encrypt 𝒜1 Map.empty;
      if valid_plain p0  valid_plain p1 then do {
        r  spmf_of_set (nlists UNIV len);
        pad  spmf_of_set (nlists UNIV len);
        let cipher = (r, pad);
        (b', _)  exec_gpv rf_encrypt (𝒜2 cipher σ) s1;
        map_spmf ((=) b') coin_spmf
      } else coin_spmf
    }"
    including monad_normalisation by(simp add: map_spmf_conv_bind_spmf split_def Let_def)
  also have " = coin_spmf"
    by(simp add: map_eq_const_coin_spmf Let_def split_def weight2 weight1)
  finally have game3: "game3 = coin_spmf" .
  
  have "ind_cpa.advantage 𝒜  prf.advantage (prf_adversary 𝒜) + ¦spmf (prf.game_1 (prf_adversary 𝒜)) True - 1 / 2¦"
    unfolding ind_cpa.advantage_def prf.advantage_def ind_cpa_0[unfolded spmf_rel_eq]
    by(rule abs_diff_triangle_ineq2)
  also have "¦spmf (prf.game_1 (prf_adversary 𝒜)) True - 1 / 2¦  q1 / 2 ^ len + q2 / 2 ^ len"
    using game1_2 game2 game3 by(simp add: spmf_of_set)
  also have " = (q1 + q2) / 2 ^ len" by(simp add: field_simps)
  also have "  q / 2 ^ len" using q1 + q2  q by(simp add: divide_right_mono)
  finally show ?thesis by(simp add: field_simps)
qed

lemma interaction_bounded_prf_adversary: 
  fixes q :: nat
  assumes "ind_cpa.ibounded_by 𝒜 q"
  shows "prf.ibounded_by (prf_adversary 𝒜) (1 + q)"
proof -
  fix η
  from assms have "ind_cpa.ibounded_by 𝒜 q" by blast
  then obtain q1 q2 where q: "q1 + q2  q"
    and [interaction_bound]: "interaction_any_bounded_by (fst 𝒜) q1"
       "x σ. interaction_any_bounded_by (snd 𝒜 x σ) q2"
    unfolding ind_cpa.ibounded_by_def by(auto simp add: split_beta iadd_le_enat_iff)
  show "prf.ibounded_by (prf_adversary 𝒜) (1 + q)" using q
    apply (simp only: prf_adversary_def Let_def split_def)
    apply -
    apply interaction_bound
      apply (auto simp add: iadd_SUP_le_iff SUP_le_iff add.assoc [symmetric] one_enat_def cong del: image_cong_simp cong add: SUP_cong_simp)
    done 
qed

lemma lossless_prf_adversary: "ind_cpa.lossless 𝒜  prf.lossless (prf_adversary 𝒜)"
by(fastforce simp add: prf_adversary_def Let_def split_def ind_cpa.lossless_def intro: lossless_inline)

end

locale otp_η =
  fixes f :: "security  key  bool list  bool list"
  and len :: "security  nat"
  assumes length_f: "η xs ys.  length xs = len η; length ys = len η   length (f η xs ys) = len η"
  and negligible_len [negligible_intros]: "negligible (λη. 1 / 2 ^ (len η))"
begin

interpretation otp "f η" "len η" for η by(unfold_locales)(rule length_f)
interpretation ind_cpa: ind_cpa "key_gen η" "encrypt η" "decrypt η" "valid_plain η" for η .
interpretation "prf": "prf" "key_gen η" "f η" "spmf_of_set (nlists UNIV (len η))" for η .

lemma prf_encrypt_secure_for:
  assumes [negligible_intros]: "negligible (λη. prf.advantage η (prf_adversary η (𝒜 η)))"
  and q: "η. ind_cpa.ibounded_by (𝒜 η) (q η)" and [negligible_intros]: "polynomial q"
  and lossless: "η. ind_cpa.lossless (𝒜 η)"
  shows "negligible (λη. ind_cpa.advantage η (𝒜 η))"
proof(rule negligible_mono)
  show "negligible (λη. prf.advantage η (prf_adversary η (𝒜 η)) + q η / 2 ^ len η)"
    by(intro negligible_intros)
  { fix η
    from ind_cpa.ibounded_by _ _ have "ind_cpa.ibounded_by (𝒜 η) (q η)" by blast
    moreover from lossless have "ind_cpa.lossless (𝒜 η)" by blast
    hence "lossless_gpv ℐ_full (fst (𝒜 η))" "cipher σ. lossless_gpv ℐ_full (snd (𝒜 η) cipher σ)"
      by(auto simp add: ind_cpa.lossless_def)
    ultimately have "ind_cpa.advantage η (𝒜 η)  prf.advantage η (prf_adversary η (𝒜 η)) + q η / 2 ^ len η"
      by(rule prf_encrypt_advantage) }
  hence "eventually (λη. ¦ind_cpa.advantage η (𝒜 η)¦  1 * ¦prf.advantage η (prf_adversary η (𝒜 η)) + q η / 2 ^ len η¦) at_top"
    by(simp add: always_eventually ind_cpa.advantage_nonneg prf.advantage_nonneg)
  then show "(λη. ind_cpa.advantage η (𝒜 η))  O(λη. prf.advantage η (prf_adversary η (𝒜 η)) + q η / 2 ^ len η)"
    by(intro bigoI[where c=1]) simp
qed

end

end