# Theory Diffie_Hellman

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

section ‹Specifying security using games›

theory Diffie_Hellman imports
CryptHOL.Cyclic_Group_SPMF
CryptHOL.Computational_Model
begin

subsection ‹The DDH game›

locale ddh =
fixes 𝒢 :: "'grp cyclic_group" (structure)
begin

type_synonym 'grp' adversary = "'grp' ⇒ 'grp' ⇒ 'grp' ⇒ bool spmf"

definition ddh_0 :: "'grp adversary ⇒ bool spmf"
where "ddh_0 𝒜 = do {
x ← sample_uniform (order 𝒢);
y ← sample_uniform (order 𝒢);
𝒜 (❙g [^] x) (❙g [^] y) (❙g [^] (x * y))
}"

definition ddh_1 :: "'grp adversary ⇒ bool spmf"
where "ddh_1 𝒜 = do {
x ← sample_uniform (order 𝒢);
y ← sample_uniform (order 𝒢);
z ← sample_uniform (order 𝒢);
𝒜 (❙g [^] x) (❙g [^] y) (❙g [^] z)
}"

where "advantage 𝒜 = ¦spmf (ddh_0 𝒜) True - spmf (ddh_1 𝒜) True¦"

definition lossless :: "'grp adversary ⇒ bool"
where "lossless 𝒜 ⟷ (∀α β γ. lossless_spmf (𝒜 α β γ))"

lemma lossless_ddh_0:
"⟦ lossless 𝒜; 0 < order 𝒢 ⟧
⟹ lossless_spmf (ddh_0 𝒜)"
by(auto simp add: lossless_def ddh_0_def split_def Let_def)

lemma lossless_ddh_1:
"⟦ lossless 𝒜; 0 < order 𝒢 ⟧
⟹ lossless_spmf (ddh_1 𝒜)"
by(auto simp add: lossless_def ddh_1_def split_def Let_def)

end

subsection ‹The LCDH game›

locale lcdh =
fixes 𝒢 :: "'grp cyclic_group" (structure)
begin

type_synonym 'grp' adversary = "'grp' ⇒ 'grp' ⇒ 'grp' set spmf"

definition lcdh :: "'grp adversary ⇒ bool spmf"
where "lcdh 𝒜 = do {
x ← sample_uniform (order 𝒢);
y ← sample_uniform (order 𝒢);
zs ← 𝒜 (❙g [^] x) (❙g [^] y);
return_spmf (❙g [^] (x * y) ∈ zs)
}"

where "advantage 𝒜 = spmf (lcdh 𝒜) True"

definition lossless :: "'grp adversary ⇒ bool"
where "lossless 𝒜 ⟷ (∀α β. lossless_spmf (𝒜 α β))"

lemma lossless_lcdh:
"⟦ lossless 𝒜; 0 < order 𝒢 ⟧
⟹ lossless_spmf (lcdh 𝒜)"
by(auto simp add: lossless_def lcdh_def split_def Let_def)

end

end


# Theory IND_CCA2

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

theory IND_CCA2 imports
CryptHOL.Computational_Model
CryptHOL.Negligible
CryptHOL.Environment_Functor
begin

locale pk_enc =
fixes key_gen :: "security ⇒ ('ekey × 'dkey) spmf" ― ‹probabilistic›
and encrypt :: "security ⇒ 'ekey ⇒ 'plain ⇒ 'cipher spmf"  ― ‹probabilistic›
and decrypt :: "security ⇒ 'dkey ⇒ 'cipher ⇒ 'plain option" ― ‹deterministic, but not used›
and valid_plain :: "security ⇒ 'plain ⇒ bool" ― ‹checks whether a plain text is valid, i.e., has the right format›

subsection ‹The IND-CCA2 game for public-key encryption›

text ‹
We model an IND-CCA2 security game in the multi-user setting as described in
\cite{BellareBoldyrevaMicali2000EUROCRYPT}.
›

locale ind_cca2 = pk_enc +
constrains key_gen :: "security ⇒ ('ekey × 'dkey) spmf"
and encrypt :: "security ⇒ 'ekey ⇒ 'plain ⇒ 'cipher spmf"
and decrypt :: "security ⇒ 'dkey ⇒ 'cipher ⇒ 'plain option"
and valid_plain :: "security ⇒ 'plain ⇒ bool"
begin

type_synonym ('ekey', 'dkey', 'cipher') state_oracle = "('ekey' × 'dkey' × 'cipher' list) option"

fun decrypt_oracle
:: "security ⇒ ('ekey, 'dkey, 'cipher) state_oracle ⇒ 'cipher
⇒ ('plain option × ('ekey, 'dkey, 'cipher) state_oracle) spmf"
where
"decrypt_oracle η None cipher = return_spmf (None, None)"
| "decrypt_oracle η (Some (ekey, dkey, cstars)) cipher = return_spmf
(if cipher ∈ set cstars then None else decrypt η dkey cipher, Some (ekey, dkey, cstars))"

fun ekey_oracle
:: "security ⇒ ('ekey, 'dkey, 'cipher) state_oracle ⇒ unit ⇒ ('ekey × ('ekey, 'dkey, 'cipher) state_oracle) spmf"
where
"ekey_oracle η None _ = do {
(ekey, dkey) ← key_gen η;
return_spmf (ekey, Some (ekey, dkey, []))
}"
| "ekey_oracle η (Some (ekey, rest)) _ = return_spmf (ekey, Some (ekey, rest))"

lemma ekey_oracle_conv:
"ekey_oracle η σ x =
(case σ of None ⇒ map_spmf (λ(ekey, dkey). (ekey, Some (ekey, dkey, []))) (key_gen η)
| Some (ekey, rest) ⇒ return_spmf (ekey, Some (ekey, rest)))"
by(cases σ)(auto simp add: map_spmf_conv_bind_spmf split_def)

context notes bind_spmf_cong[fundef_cong] begin
function encrypt_oracle
:: "bool ⇒ security ⇒ ('ekey, 'dkey, 'cipher) state_oracle ⇒ 'plain × 'plain
⇒ ('cipher × ('ekey, 'dkey, 'cipher) state_oracle) spmf"
where
"encrypt_oracle b η None m01 = do { (_, σ) ← ekey_oracle η None (); encrypt_oracle b η σ m01 }"
| "encrypt_oracle b η (Some (ekey, dkey, cstars)) (m0, m1) =
(if valid_plain η m0 ∧ valid_plain η m1 then do {
let pb = (if b then m0 else m1);
cstar ← encrypt η ekey pb;
return_spmf (cstar, Some (ekey, dkey, cstar # cstars))
} else return_pmf None)"
by pat_completeness auto
termination by(relation "Wellfounded.measure (λ(b, η, σ, m01). case σ of None ⇒ 1 | _ ⇒ 0)") auto
end

subsubsection ‹Single-user setting›

type_synonym ('plain', 'cipher') call⇩1 = "unit + 'cipher' + 'plain' × 'plain'"
type_synonym ('ekey', 'plain', 'cipher') ret⇩1 = "'ekey' + 'plain' option + 'cipher'"

definition oracle⇩1 :: "bool ⇒ security
⇒ (('ekey, 'dkey, 'cipher) state_oracle, ('plain, 'cipher) call⇩1, ('ekey, 'plain, 'cipher) ret⇩1) oracle'"
where "oracle⇩1 b η = ekey_oracle η ⊕⇩O (decrypt_oracle η ⊕⇩O encrypt_oracle b η)"

lemma oracle⇩1_simps [simp]:
"oracle⇩1 b η s (Inl x) = map_spmf (apfst Inl) (ekey_oracle η s x)"
"oracle⇩1 b η s (Inr (Inl y)) = map_spmf (apfst (Inr ∘ Inl)) (decrypt_oracle η s y)"
"oracle⇩1 b η s (Inr (Inr z)) = map_spmf (apfst (Inr ∘ Inr)) (encrypt_oracle b η s z)"
by(simp_all add: oracle⇩1_def spmf.map_comp apfst_compose o_def)

type_synonym ('ekey', 'plain', 'cipher') adversary⇩1' =
"(bool, ('plain', 'cipher') call⇩1, ('ekey', 'plain', 'cipher') ret⇩1) gpv"
type_synonym ('ekey', 'plain', 'cipher') adversary⇩1 =
"security ⇒ ('ekey', 'plain', 'cipher') adversary⇩1'"

definition ind_cca2⇩1 :: "('ekey, 'plain, 'cipher) adversary⇩1 ⇒ security ⇒ bool spmf"
where
"ind_cca2⇩1 𝒜 η = TRY do {
b ← coin_spmf;
(guess, s) ← exec_gpv (oracle⇩1 b η) (𝒜 η) None;
return_spmf (guess = b)
} ELSE coin_spmf"

where "advantage⇩1 𝒜 η = ¦spmf (ind_cca2⇩1 𝒜 η) True - 1/2¦"

abbreviation secure_for⇩1 :: "('ekey, 'plain, 'cipher) adversary⇩1 ⇒ bool"
where "secure_for⇩1 𝒜 ≡ negligible (advantage⇩1 𝒜)"

definition ibounded_by⇩1' :: "('ekey, 'plain, 'cipher) adversary⇩1' ⇒ nat ⇒ bool"
where "ibounded_by⇩1' 𝒜 q = interaction_any_bounded_by 𝒜 q"

abbreviation ibounded_by⇩1 :: "('ekey, 'plain, 'cipher) adversary⇩1 ⇒ (security ⇒ nat) ⇒ bool"
where "ibounded_by⇩1 ≡ rel_envir ibounded_by⇩1'"

definition lossless⇩1' :: "('ekey, 'plain, 'cipher) adversary⇩1' ⇒ bool"
where "lossless⇩1' 𝒜 = lossless_gpv ℐ_full 𝒜"

abbreviation lossless⇩1 :: "('ekey, 'plain, 'cipher) adversary⇩1 ⇒ bool"
where "lossless⇩1 ≡ pred_envir lossless⇩1'"

lemma lossless_decrypt_oracle [simp]: "lossless_spmf (decrypt_oracle η σ cipher)"
by(cases "(η, σ, cipher)" rule: decrypt_oracle.cases) simp_all

lemma lossless_ekey_oracle [simp]:
"lossless_spmf (ekey_oracle η σ x) ⟷ (σ = None ⟶ lossless_spmf (key_gen η))"
by(cases "(η, σ, x)" rule: ekey_oracle.cases)(auto)

lemma lossless_encrypt_oracle [simp]:
"⟦ σ = None ⟹ lossless_spmf (key_gen η);
⋀ekey m. valid_plain η m ⟹ lossless_spmf (encrypt η ekey m) ⟧
⟹ lossless_spmf (encrypt_oracle b η σ (m0, m1)) ⟷ valid_plain η m0 ∧ valid_plain η m1"
apply(cases "(b, η, σ, (m0, m1))" rule: encrypt_oracle.cases)
apply(auto simp add: split_beta dest: lossless_spmfD_set_spmf_nonempty split: if_split_asm)
done

subsubsection ‹Multi-user setting›

definition oracle⇩n :: "bool ⇒ security
⇒ ('i ⇒ ('ekey, 'dkey, 'cipher) state_oracle, 'i × ('plain, 'cipher) call⇩1, ('ekey, 'plain, 'cipher) ret⇩1) oracle'"
where "oracle⇩n b η = family_oracle (λ_. oracle⇩1 b η)"

lemma oracle⇩n_apply [simp]:
"oracle⇩n b η s (i, x) = map_spmf (apsnd (fun_upd s i)) (oracle⇩1 b η (s i) x)"

type_synonym ('i, 'ekey', 'plain', 'cipher') adversary⇩n' =
"(bool, 'i × ('plain', 'cipher') call⇩1, ('ekey', 'plain', 'cipher') ret⇩1) gpv"
type_synonym ('i, 'ekey', 'plain', 'cipher') adversary⇩n =
"security ⇒ ('i, 'ekey', 'plain', 'cipher') adversary⇩n'"

definition ind_cca2⇩n :: "('i, 'ekey, 'plain, 'cipher) adversary⇩n ⇒ security ⇒ bool spmf"
where
"ind_cca2⇩n 𝒜 η = TRY do {
b ← coin_spmf;
(guess, σ) ← exec_gpv (oracle⇩n b η) (𝒜 η) (λ_. None);
return_spmf (guess = b)
} ELSE coin_spmf"

where "advantage⇩n 𝒜 η = ¦spmf (ind_cca2⇩n 𝒜 η) True - 1/2¦"

abbreviation secure_for⇩n :: "('i, 'ekey, 'plain, 'cipher) adversary⇩n ⇒ bool"
where "secure_for⇩n 𝒜 ≡ negligible (advantage⇩n 𝒜)"

definition ibounded_by⇩n' :: "('i, 'ekey, 'plain, 'cipher) adversary⇩n' ⇒ nat ⇒ bool"
where "ibounded_by⇩n' 𝒜 q = interaction_any_bounded_by 𝒜 q"

abbreviation ibounded_by⇩n :: "('i, 'ekey, 'plain, 'cipher) adversary⇩n ⇒ (security ⇒ nat) ⇒ bool"
where "ibounded_by⇩n ≡ rel_envir ibounded_by⇩n'"

definition lossless⇩n' :: "('i, 'ekey, 'plain, 'cipher) adversary⇩n' ⇒ bool"
where "lossless⇩n' 𝒜 = lossless_gpv ℐ_full 𝒜"

abbreviation lossless⇩n :: "('i, 'ekey, 'plain, 'cipher) adversary⇩n ⇒ bool"
where "lossless⇩n ≡ pred_envir lossless⇩n'"

definition cipher_queries :: "('i ⇒ ('ekey, 'dkey, 'cipher) state_oracle) ⇒ 'cipher set"
where "cipher_queries ose = (⋃(_, _, ciphers)∈ran ose. set ciphers)"

lemma cipher_queriesI:
"⟦ ose n = Some (ek, dk, ciphers); x ∈ set ciphers ⟧ ⟹ x ∈ cipher_queries ose"

lemma cipher_queriesE:
assumes "x ∈ cipher_queries ose"
obtains (cipher_queries) n ek dk ciphers where "ose n = Some (ek, dk, ciphers)" "x ∈ set ciphers"
using assms by(auto simp add: cipher_queries_def ran_def)

lemma cipher_queries_updE:
assumes "x ∈ cipher_queries (ose(n ↦ (ek, dk, ciphers)))"
obtains (old) "x ∈ cipher_queries ose" "x ∉ set ciphers" | (new) "x ∈ set ciphers"
using assms by(cases "x ∈ set ciphers")(fastforce elim!: cipher_queriesE split: if_split_asm intro: cipher_queriesI)+

lemma cipher_queries_empty [simp]: "cipher_queries Map.empty = {}"

end

end


# Theory IND_CCA2_sym

(* Title: IND_CCA2_sym.thy
Author: Andreas Lochbihler, ETH Zurich
Author: S. Reza Sefidgar, ETH Zurich *)

subsection ‹The IND-CCA2 security for symmetric encryption schemes›

theory IND_CCA2_sym imports
CryptHOL.Computational_Model
begin

locale ind_cca =
fixes key_gen :: "'key spmf"
and encrypt :: "'key ⇒ 'message ⇒ 'cipher spmf"
and decrypt :: "'key ⇒ 'cipher ⇒ 'message option"
and msg_predicate :: "'message ⇒ bool"
begin

"(bool, 'message' × 'message' + 'cipher', 'cipher' option + 'message' option) gpv"

definition oracle_encrypt :: "'key ⇒ bool ⇒ ('message × 'message, 'cipher option, 'cipher set) callee"
where
"oracle_encrypt k b L = (λ(msg1, msg0).
(case msg_predicate msg1 ∧ msg_predicate msg0 of
True ⇒ do {
c ← encrypt k (if b then msg1 else msg0);
return_spmf (Some c, {c} ∪ L)
}
| False ⇒ return_spmf (None, L)))"

lemma lossless_oracle_encrypt [simp]:
assumes "lossless_spmf (encrypt k m1)" and "lossless_spmf (encrypt k m0)"
shows "lossless_spmf (oracle_encrypt k b L (m1, m0))"
using assms by (simp add: oracle_encrypt_def split: bool.split)

definition oracle_decrypt :: "'key ⇒ ('cipher, 'message option, 'cipher set) callee"
where "oracle_decrypt k L c = return_spmf (if c ∈ L then None else decrypt k c, L)"

lemma lossless_oracle_decrypt [simp]: "lossless_spmf (oracle_decrypt k L c)"

definition game :: "('message, 'cipher) adversary ⇒ bool spmf"
where
"game 𝒜 = do {
key ← key_gen;
b ← coin_spmf;
(b', L') ← exec_gpv (oracle_encrypt key b ⊕⇩O oracle_decrypt key) 𝒜 {};
return_spmf (b = b')
}"

where "advantage 𝒜 = ¦spmf (game 𝒜) True - 1 / 2¦"

end

end


# Theory IND_CPA

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

theory IND_CPA imports
CryptHOL.Generative_Probabilistic_Value
CryptHOL.Computational_Model
CryptHOL.Negligible
begin

subsection ‹The IND-CPA game for symmetric encryption schemes›

locale ind_cpa =
fixes key_gen :: "'key spmf" ― ‹probabilistic›
and encrypt :: "'key ⇒ 'plain ⇒ 'cipher spmf"  ― ‹probabilistic›
and decrypt :: "'key ⇒ 'cipher ⇒ 'plain option" ― ‹deterministic, but not used›
and valid_plain :: "'plain ⇒ bool" ― ‹checks whether a plain text is valid, i.e., has the right format›
begin

text ‹
We cannot incorporate the predicate @{term valid_plain} in the type @{typ "'plain"} of plaintexts,
because the single @{typ "'plain"} must contain plaintexts for all values of the security parameter,
as HOL does not have dependent types.  Consequently, the oracle has to ensure that the received
plaintexts are valid.
›

type_synonym ('plain', 'cipher', 'state) adversary =
"(('plain' × 'plain') × 'state, 'plain', 'cipher') gpv
× ('cipher' ⇒ 'state ⇒ (bool, 'plain', 'cipher') gpv)"

definition encrypt_oracle :: "'key ⇒ unit ⇒ 'plain ⇒ ('cipher × unit) spmf"
where
"encrypt_oracle key σ plain = do {
cipher ← encrypt key plain;
return_spmf (cipher, ())
}"

definition ind_cpa :: "('plain, 'cipher, 'state) adversary ⇒ bool spmf"
where
"ind_cpa 𝒜 = do {
let (𝒜1, 𝒜2) = 𝒜;
key ← key_gen;
b ← coin_spmf;
(guess, _) ← exec_gpv (encrypt_oracle key) (do {
((m0, m1), σ) ← 𝒜1;
if valid_plain m0 ∧ valid_plain m1 then do {
cipher ← lift_spmf (encrypt key (if b then m0 else m1));
𝒜2 cipher σ
} else lift_spmf coin_spmf
}) ();
return_spmf (guess = b)
}"

where "advantage 𝒜 = ¦spmf (ind_cpa 𝒜) True - 1/2¦"

definition ibounded_by :: "('plain, 'cipher, 'state) adversary ⇒ enat ⇒ bool"
where
"ibounded_by = (λ(𝒜1, 𝒜2) q.
(∃q1 q2. interaction_any_bounded_by 𝒜1 q1 ∧ (∀cipher σ. interaction_any_bounded_by (𝒜2 cipher σ) q2) ∧ q1 + q2 ≤ q))"

lemma ibounded_byE [consumes 1, case_names ibounded_by, elim?]:
assumes "ibounded_by (𝒜1, 𝒜2) q"
obtains q1 q2
where "q1 + q2 ≤ q"
and "interaction_any_bounded_by 𝒜1 q1"
and "⋀cipher σ. interaction_any_bounded_by (𝒜2 cipher σ) q2"
using assms by(auto simp add: ibounded_by_def)

lemma ibounded_byI [intro?]:
"⟦ interaction_any_bounded_by 𝒜1 q1; ⋀cipher σ. interaction_any_bounded_by (𝒜2 cipher σ) q2; q1 + q2 ≤ q ⟧
⟹ ibounded_by (𝒜1, 𝒜2) q"

definition lossless :: "('plain, 'cipher, 'state) adversary ⇒ bool"
where "lossless = (λ(𝒜1, 𝒜2). lossless_gpv ℐ_full 𝒜1 ∧ (∀cipher σ. lossless_gpv ℐ_full (𝒜2 cipher σ)))"

end

end


# Theory IND_CPA_PK

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

theory IND_CPA_PK imports
CryptHOL.Computational_Model
CryptHOL.Negligible
begin

subsection ‹The IND-CPA game for public-key encryption with oracle access›

locale ind_cpa_pk =
fixes key_gen :: "('pubkey × 'privkey, 'call, 'ret) gpv" ― ‹probabilistic›
and aencrypt :: "'pubkey ⇒ 'plain ⇒ ('cipher, 'call, 'ret) gpv"  ― ‹probabilistic w/ access to an oracle›
and adecrypt :: "'privkey ⇒ 'cipher ⇒ ('plain, 'call, 'ret) gpv" ― ‹not used›
and valid_plains :: "'plain ⇒ 'plain ⇒ bool" ― ‹checks whether a pair of plaintexts is valid, i.e., they have the right format›
begin

text ‹
We cannot incorporate the predicate @{term valid_plain} in the type @{typ "'plain"} of plaintexts,
because the single @{typ "'plain"} must contain plaintexts for all values of the security parameter,
as HOL does not have dependent types.  Consequently, the game has to ensure that the received
plaintexts are valid.
›

type_synonym ('pubkey', 'plain', 'cipher', 'call', 'ret', 'state) adversary =
"('pubkey' ⇒ (('plain' × 'plain') × 'state, 'call', 'ret') gpv)
× ('cipher' ⇒ 'state ⇒ (bool, 'call', 'ret') gpv)"

fun ind_cpa :: "('pubkey, 'plain, 'cipher, 'call, 'ret, 'state) adversary ⇒ (bool, 'call, 'ret) gpv"
where
"ind_cpa (𝒜1, 𝒜2) = TRY do {
(pk, sk) ← key_gen;
b ← lift_spmf coin_spmf;
((m0, m1), σ) ← (𝒜1 pk);
assert_gpv (valid_plains m0 m1);
cipher ← aencrypt pk (if b then m0 else m1);
guess ← 𝒜2 cipher σ;
Done (guess = b)
} ELSE lift_spmf coin_spmf"

definition advantage :: "('σ ⇒ 'call ⇒ ('ret × 'σ) spmf) ⇒ 'σ ⇒ ('pubkey, 'plain, 'cipher, 'call, 'ret, 'state) adversary ⇒ real"
where "advantage oracle σ 𝒜 = ¦spmf (run_gpv oracle (ind_cpa 𝒜) σ) True - 1/2¦"

definition ibounded_by :: "('call ⇒ bool) ⇒ ('pubkey, 'plain, 'cipher, 'call, 'ret, 'state) adversary ⇒ enat ⇒ bool"
where
"ibounded_by consider = (λ(𝒜1, 𝒜2) q.
(∃q1 q2. (∀pk. interaction_bounded_by consider (𝒜1 pk) q1) ∧ (∀cipher σ. interaction_bounded_by consider (𝒜2 cipher σ) q2) ∧ q1 + q2 ≤ q))"

lemma ibounded_by'E [consumes 1, case_names ibounded_by', elim?]:
assumes "ibounded_by consider (𝒜1, 𝒜2) q"
obtains q1 q2
where "q1 + q2 ≤ q"
and "⋀pk. interaction_bounded_by consider (𝒜1 pk) q1"
and "⋀cipher σ. interaction_bounded_by consider (𝒜2 cipher σ) q2"
using assms by(auto simp add: ibounded_by_def)

lemma ibounded_byI [intro?]:
"⟦ ⋀pk. interaction_bounded_by consider (𝒜1 pk) q1; ⋀cipher σ. interaction_bounded_by consider (𝒜2 cipher σ) q2; q1 + q2 ≤ q ⟧
⟹ ibounded_by consider (𝒜1, 𝒜2) q"

definition lossless :: "('pubkey, 'plain, 'cipher, 'call, 'ret, 'state) adversary ⇒ bool"
where "lossless = (λ(𝒜1, 𝒜2). (∀pk. lossless_gpv ℐ_full (𝒜1 pk)) ∧ (∀cipher σ. lossless_gpv ℐ_full (𝒜2 cipher σ)))"

end

end


# Theory IND_CPA_PK_Single

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

theory IND_CPA_PK_Single imports
CryptHOL.Computational_Model
begin

subsection ‹The IND-CPA game (public key, single instance)›

locale ind_cpa =
fixes key_gen :: "('pub_key × 'priv_key) spmf" ― ‹probabilistic›
and aencrypt :: "'pub_key ⇒ 'plain ⇒ 'cipher spmf"  ― ‹probabilistic›
and adecrypt :: "'priv_key ⇒ 'cipher ⇒ 'plain option" ― ‹deterministic, but not used›
and valid_plains :: "'plain ⇒ 'plain ⇒ bool" ― ‹checks whether a pair of plaintexts is valid, i.e., they both have the right format›
begin

text ‹
We cannot incorporate the predicate @{term valid_plain} in the type @{typ "'plain"} of plaintexts,
because the single @{typ "'plain"} must contain plaintexts for all values of the security parameter,
as HOL does not have dependent types.  Consequently, the oracle has to ensure that the received
plaintexts are valid.
›

type_synonym ('pub_key', 'plain', 'cipher', 'state) adversary =
"('pub_key' ⇒ (('plain' × 'plain') × 'state) spmf)
× ('cipher' ⇒ 'state ⇒ bool spmf)"

primrec ind_cpa :: "('pub_key, 'plain, 'cipher, 'state) adversary ⇒ bool spmf"
where
"ind_cpa (𝒜1, 𝒜2) = TRY do {
(pk, sk) ← key_gen;
((m0, m1), σ) ← 𝒜1 pk;
_ :: unit ← assert_spmf (valid_plains m0 m1);
b ← coin_spmf;
cipher ← aencrypt pk (if b then m0 else m1);
b' ← 𝒜2 cipher σ;
return_spmf (b = b')
} ELSE coin_spmf"

declare ind_cpa.simps [simp del]

where "advantage 𝒜 = ¦spmf (ind_cpa 𝒜) True - 1/2¦"

definition lossless :: "('pub_key, 'plain, 'cipher, 'state) adversary ⇒ bool"
where
"lossless 𝒜 ⟷
((∀pk. lossless_spmf (fst 𝒜 pk)) ∧
(∀cipher σ. lossless_spmf (snd 𝒜 cipher σ)))"

lemma lossless_ind_cpa:
"⟦ lossless 𝒜; lossless_spmf (key_gen) ⟧ ⟹ lossless_spmf (ind_cpa 𝒜)"
by(auto simp add: lossless_def ind_cpa_def split_def Let_def)

end

end


# Theory SUF_CMA

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

theory SUF_CMA imports
CryptHOL.Computational_Model
CryptHOL.Negligible
CryptHOL.Environment_Functor
begin

subsection ‹Strongly existentially unforgeable signature scheme›

locale sig_scheme =
fixes key_gen :: "security ⇒ ('vkey × 'sigkey) spmf"
and sign :: "security ⇒ 'sigkey ⇒ 'message ⇒ 'signature spmf"
and verify :: "security ⇒ 'vkey ⇒ 'message ⇒ 'signature ⇒ bool" ― ‹verification is deterministic›
and valid_message :: "security ⇒ 'message ⇒ bool"

locale suf_cma = sig_scheme +
constrains key_gen :: "security ⇒ ('vkey × 'sigkey) spmf"
and sign :: "security ⇒ 'sigkey ⇒ 'message ⇒ 'signature spmf"
and verify :: "security ⇒ 'vkey ⇒ 'message ⇒ 'signature ⇒ bool"
and valid_message :: "security ⇒ 'message ⇒ bool"
begin

type_synonym ('vkey', 'sigkey', 'message', 'signature') state_oracle
= "('vkey' × 'sigkey' × ('message' × 'signature') list) option"

fun vkey_oracle :: "security ⇒ (('vkey, 'sigkey, 'message, 'signature) state_oracle, unit, 'vkey) oracle'"
where
"vkey_oracle η None _ = do {
(vkey, sigkey) ← key_gen η;
return_spmf (vkey, Some (vkey, sigkey, []))
}"
| "⋀log. vkey_oracle η (Some (vkey, sigkey, log)) _ = return_spmf (vkey, Some (vkey, sigkey, log))"

context notes bind_spmf_cong[fundef_cong] begin
function sign_oracle
:: "security ⇒ (('vkey, 'sigkey, 'message, 'signature) state_oracle, 'message, 'signature) oracle'"
where
"sign_oracle η None m = do { (_, σ) ← vkey_oracle η None (); sign_oracle η σ m }"
| "⋀log. sign_oracle η (Some (vkey, skey, log)) m =
(if valid_message η m then do {
sig ← sign η skey m;
return_spmf (sig, Some (vkey, skey, (m, sig) # log))
} else return_pmf None)"
by pat_completeness auto
termination by(relation "Wellfounded.measure (λ(η, σ, m). case σ of None ⇒ 1 | _ ⇒ 0)") auto
end

lemma lossless_vkey_oracle [simp]:
"lossless_spmf (vkey_oracle η σ x) ⟷ (σ = None ⟶ lossless_spmf (key_gen η))"
by(cases "(η, σ, x)" rule: vkey_oracle.cases) auto

lemma lossless_sign_oracle [simp]:
"⟦ σ = None ⟹ lossless_spmf (key_gen η);
⋀skey m. valid_message η m ⟹ lossless_spmf (sign η skey m) ⟧
⟹ lossless_spmf (sign_oracle η σ m) ⟷ valid_message η m"
apply(cases "(η, σ, m)" rule: sign_oracle.cases)
apply(auto simp add: split_beta dest: lossless_spmfD_set_spmf_nonempty)
done

lemma lossless_sign_oracle_Some: fixes log shows
"lossless_spmf (sign_oracle η (Some (vkey, skey, log)) m) ⟷ lossless_spmf (sign η skey m) ∧ valid_message η m"
by(simp)

subsubsection ‹Single-user setting›

type_synonym 'message' call⇩1 = "unit + 'message'"
type_synonym ('vkey', 'signature') ret⇩1 = "'vkey' + 'signature'"

definition oracle⇩1 :: "security
⇒ (('vkey, 'sigkey, 'message, 'signature) state_oracle, 'message call⇩1, ('vkey, 'signature) ret⇩1) oracle'"
where "oracle⇩1 η = vkey_oracle η ⊕⇩O sign_oracle η"

lemma oracle⇩1_simps [simp]:
"oracle⇩1 η s (Inl x) = map_spmf (apfst Inl) (vkey_oracle η s x)"
"oracle⇩1 η s (Inr y) = map_spmf (apfst Inr) (sign_oracle η s y)"

type_synonym ('vkey', 'message', 'signature') adversary⇩1' =
"(('message' × 'signature'), 'message' call⇩1, ('vkey', 'signature') ret⇩1) gpv"
type_synonym ('vkey', 'message', 'signature') adversary⇩1 =
"security ⇒ ('vkey', 'message', 'signature') adversary⇩1'"

definition suf_cma⇩1 :: "('vkey, 'message, 'signature) adversary⇩1 ⇒ security ⇒ bool spmf"
where
"⋀log. suf_cma⇩1 𝒜 η = do {
((m, sig), σ) ← exec_gpv (oracle⇩1 η) (𝒜 η) None;
return_spmf (
case σ of None ⇒ False
| Some (vkey, skey, log) ⇒ verify η vkey m sig ∧ (m, sig) ∉ set log)
}"

where "advantage⇩1 𝒜 η = spmf (suf_cma⇩1 𝒜 η) True"

abbreviation secure_for⇩1 :: "('vkey, 'message, 'signature) adversary⇩1 ⇒ bool"
where "secure_for⇩1 𝒜 ≡ negligible (advantage⇩1 𝒜)"

definition ibounded_by⇩1' :: "('vkey, 'message, 'signature) adversary⇩1' ⇒ nat ⇒ bool"
where "ibounded_by⇩1' 𝒜 q = (interaction_any_bounded_by 𝒜 q)"

abbreviation ibounded_by⇩1 :: "('vkey, 'message, 'signature) adversary⇩1 ⇒ (security ⇒ nat) ⇒ bool"
where "ibounded_by⇩1 ≡ rel_envir ibounded_by⇩1'"

definition lossless⇩1' :: "('vkey, 'message, 'signature) adversary⇩1' ⇒ bool"
where "lossless⇩1' 𝒜 = (lossless_gpv ℐ_full 𝒜)"

abbreviation lossless⇩1 :: "('vkey, 'message, 'signature) adversary⇩1 ⇒ bool"
where "lossless⇩1 ≡ pred_envir lossless⇩1'"

subsubsection ‹Multi-user setting›

definition oracle⇩n :: "security
⇒ ('i ⇒ ('vkey, 'sigkey, 'message, 'signature) state_oracle, 'i × 'message call⇩1, ('vkey, 'signature) ret⇩1) oracle'"
where "oracle⇩n η = family_oracle (λ_. oracle⇩1 η)"

lemma oracle⇩n_apply [simp]:
"oracle⇩n η s (i, x) = map_spmf (apsnd (fun_upd s i)) (oracle⇩1 η (s i) x)"

type_synonym ('i, 'vkey', 'message', 'signature') adversary⇩n' =
"(('i × 'message' × 'signature'), 'i × 'message' call⇩1, ('vkey', 'signature') ret⇩1) gpv"
type_synonym ('i, 'vkey', 'message', 'signature') adversary⇩n =
"security ⇒ ('i, 'vkey', 'message', 'signature') adversary⇩n'"

definition suf_cma⇩n :: "('i, 'vkey, 'message, 'signature) adversary⇩n ⇒ security ⇒ bool spmf"
where
"⋀log. suf_cma⇩n 𝒜 η = do {
((i, m, sig), σ) ← exec_gpv (oracle⇩n η) (𝒜 η) (λ_. None);
return_spmf (
case σ i of None ⇒ False
| Some (vkey, skey, log) ⇒ verify η vkey m sig ∧ (m, sig) ∉ set log)
}"

where "advantage⇩n 𝒜 η = spmf (suf_cma⇩n 𝒜 η) True"

abbreviation secure_for⇩n :: "('i, 'vkey, 'message, 'signature) adversary⇩n ⇒ bool"
where "secure_for⇩n 𝒜 ≡ negligible (advantage⇩n 𝒜)"

definition ibounded_by⇩n' :: "('i, 'vkey, 'message, 'signature) adversary⇩n' ⇒ nat ⇒ bool"
where "ibounded_by⇩n' 𝒜 q = (interaction_any_bounded_by 𝒜 q)"

abbreviation ibounded_by⇩n :: "('i, 'vkey, 'message, 'signature) adversary⇩n ⇒ (security ⇒ nat) ⇒ bool"
where "ibounded_by⇩n ≡ rel_envir ibounded_by⇩n'"

definition lossless⇩n' :: "('i, 'vkey, 'message, 'signature) adversary⇩n' ⇒ bool"
where "lossless⇩n' 𝒜 = (lossless_gpv ℐ_full 𝒜)"

abbreviation lossless⇩n :: "('i, 'vkey, 'message, 'signature) adversary⇩n ⇒ bool"
where "lossless⇩n ≡ pred_envir lossless⇩n'"

end

end


# Theory Pseudo_Random_Function

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

theory Pseudo_Random_Function imports
CryptHOL.Computational_Model
begin

subsection ‹Pseudo-random function›

locale random_function =
fixes p :: "'a spmf"
begin

type_synonym ('b,'a') dict = "'b ⇀ 'a'"

definition random_oracle :: "('b, 'a) dict ⇒ 'b ⇒ ('a × ('b, 'a) dict) spmf"
where
"random_oracle σ x =
(case σ x of Some y ⇒ return_spmf (y, σ)
| None ⇒ p ⤜ (λy. return_spmf (y, σ(x ↦ y))))"

definition forgetful_random_oracle :: "unit ⇒ 'b ⇒ ('a × unit) spmf"
where
"forgetful_random_oracle σ x = p ⤜ (λy. return_spmf (y, ()))"

lemma weight_random_oracle [simp]:
"weight_spmf p = 1 ⟹ weight_spmf (random_oracle σ x) = 1"
by(simp add: random_oracle_def weight_bind_spmf o_def split: option.split)

lemma lossless_random_oracle [simp]:
"lossless_spmf p ⟹ lossless_spmf (random_oracle σ x)"

sublocale finite: callee_invariant_on random_oracle "λσ. finite (dom σ)" ℐ_full
by(unfold_locales)(auto simp add: random_oracle_def split: option.splits)

lemma card_dom_random_oracle:
assumes "interaction_any_bounded_by 𝒜 q"
and "(y, σ') ∈ set_spmf (exec_gpv random_oracle 𝒜 σ)"
and fin: "finite (dom σ)"
shows "card (dom σ') ≤ q + card (dom σ)"
by(rule finite.interaction_bounded_by'_exec_gpv_count[OF assms(1-2)])
(auto simp add: random_oracle_def fin card_insert_if simp del: fun_upd_apply split: option.split_asm)

end

subsection ‹Pseudo-random function›

locale "prf" =
fixes key_gen :: "'key spmf"
and "prf" :: "'key ⇒ 'domain ⇒ 'range"
and rand :: "'range spmf"
begin

sublocale random_function "rand" .

definition prf_oracle :: "'key ⇒ unit ⇒ 'domain ⇒ ('range × unit) spmf"
where "prf_oracle key σ x = return_spmf (prf key x, ())"

type_synonym ('domain', 'range') adversary = "(bool, 'domain', 'range') gpv"

definition game_0 :: "('domain, 'range) adversary ⇒ bool spmf"
where
"game_0 𝒜 = do {
key ← key_gen;
(b, _) ← exec_gpv (prf_oracle key) 𝒜 ();
return_spmf b
}"

definition game_1 :: "('domain, 'range) adversary ⇒ bool spmf"
where
"game_1 𝒜 = do {
(b, _) ← exec_gpv random_oracle 𝒜 Map.empty;
return_spmf b
}"

where "advantage 𝒜 = ¦spmf (game_0 𝒜) True - spmf (game_1 𝒜) True¦"

abbreviation lossless :: "('domain, 'range) adversary ⇒ bool"
where "lossless ≡ lossless_gpv ℐ_full"

abbreviation (input) ibounded_by :: "('domain, 'range) adversary ⇒ enat ⇒ bool"
where "ibounded_by ≡ interaction_any_bounded_by"

end

end


# Theory Pseudo_Random_Permutation

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

subsection ‹Random permutation›

theory Pseudo_Random_Permutation imports
CryptHOL.Computational_Model
begin

locale random_permutation =
fixes A :: "'b set"
begin

definition random_permutation :: "('a ⇀ 'b) ⇒ 'a ⇒ ('b × ('a ⇀ 'b)) spmf"
where
"random_permutation σ x =
(case σ x of Some y ⇒ return_spmf (y, σ)
| None ⇒ spmf_of_set (A - ran σ) ⤜ (λy. return_spmf (y, σ(x ↦ y))))"

lemma weight_random_oracle [simp]:
"⟦ finite A; A - ran σ ≠ {} ⟧ ⟹ weight_spmf (random_permutation σ x) = 1"
by(simp add: random_permutation_def weight_bind_spmf o_def split: option.split)

lemma lossless_random_oracle [simp]:
"⟦ finite A; A - ran σ ≠ {} ⟧ ⟹ lossless_spmf (random_permutation σ x)"

sublocale finite: callee_invariant_on random_permutation "λσ. finite (dom σ)" ℐ_full
by(unfold_locales)(auto simp add: random_permutation_def split: option.splits)

lemma card_dom_random_oracle:
assumes "interaction_any_bounded_by 𝒜 q"
and "(y, σ') ∈ set_spmf (exec_gpv random_permutation 𝒜 σ)"
and fin: "finite (dom σ)"
shows "card (dom σ') ≤ q + card (dom σ)"
by(rule finite.interaction_bounded_by'_exec_gpv_count[OF assms(1-2)])
(auto simp add: random_permutation_def fin card_insert_if simp del: fun_upd_apply split: option.split_asm)

end

end


# Theory Guessing_Many_One

(* Title: Guessing_Many_One.thy
Author: Andreas Lochbihler, ETH Zurich
Author: S. Reza Sefidgar, ETH Zurich *)

subsection ‹Reducing games with many adversary guesses to games with single guesses›

theory Guessing_Many_One imports
CryptHOL.Computational_Model
CryptHOL.GPV_Bisim
begin

locale guessing_many_one =
fixes init :: "('c_o × 'c_a × 's) spmf"
and "oracle" :: "'c_o ⇒ 's ⇒ 'call ⇒ ('ret × 's) spmf"
and "eval" :: "'c_o ⇒ 'c_a ⇒ 's ⇒ 'guess ⇒ bool spmf"
begin

type_synonym ('c_a', 'guess', 'call', 'ret') adversary_single = "'c_a' ⇒ ('guess', 'call', 'ret') gpv"

definition game_single :: "('c_a, 'guess, 'call, 'ret) adversary_single ⇒ bool spmf"
where
"game_single 𝒜 = do {
(c_o, c_a, s) ← init;
(guess, s') ← exec_gpv (oracle c_o) (𝒜 c_a) s;
eval c_o c_a s' guess
}"

where "advantage_single 𝒜 = spmf (game_single 𝒜) True"

type_synonym ('c_a', 'guess', 'call', 'ret') adversary_many = "'c_a' ⇒ (unit, 'call' + 'guess', 'ret' + unit) gpv"

definition eval_oracle :: "'c_o ⇒ 'c_a ⇒ bool × 's ⇒ 'guess ⇒ (unit × (bool × 's)) spmf"
where
"eval_oracle c_o c_a = (λ(b, s') guess. map_spmf (λb'. ((), (b ∨ b', s'))) (eval c_o c_a s' guess))"

definition game_multi :: "('c_a, 'guess, 'call, 'ret) adversary_many ⇒ bool spmf"
where
"game_multi 𝒜 = do {
(c_o, c_a, s) ← init;
(_, (b, _)) ← exec_gpv
(†(oracle c_o) ⊕⇩O eval_oracle c_o c_a)
(𝒜 c_a)
(False, s);
return_spmf b
}"

where "advantage_multi 𝒜 = spmf (game_multi 𝒜) True"

type_synonym 'guess' reduction_state = "'guess' + nat"

primrec process_call :: "'guess reduction_state ⇒ 'call ⇒ ('ret option × 'guess reduction_state, 'call, 'ret) gpv"
where
"process_call (Inr j) x = do {
ret ← Pause x Done;
Done (Some ret, Inr j)
}"
| "process_call (Inl guess) x = Done (None, Inl guess)"

primrec process_guess :: "'guess reduction_state ⇒ 'guess ⇒ (unit option × 'guess reduction_state, 'call, 'ret) gpv"
where
"process_guess (Inr j) guess = Done (if j > 0 then (Some (), Inr (j - 1)) else (None, Inl guess))"
| "process_guess (Inl guess) _ = Done (None, Inl guess)"

abbreviation reduction_oracle :: "'guess + nat ⇒ 'call + 'guess ⇒ (('ret + unit) option × ('guess + nat), 'call, 'ret) gpv"
where "reduction_oracle ≡ plus_intercept_stop process_call process_guess"

definition reduction :: "nat ⇒ ('c_a, 'guess, 'call, 'ret) adversary_many ⇒ ('c_a, 'guess, 'call, 'ret) adversary_single"
where
"reduction q 𝒜 c_a = do {
j_star ← lift_spmf (spmf_of_set {..<q});
(_, s) ← inline_stop reduction_oracle (𝒜 c_a) (Inr j_star);
Done (projl s)
}"

lemma many_single_reduction:
assumes bound: "⋀c_a c_o s. (c_o, c_a, s) ∈ set_spmf init ⟹ interaction_bounded_by (Not ∘ isl) (𝒜 c_a) q"
and lossless_oracle: "⋀c_a c_o s s' x. (c_o, c_a, s) ∈ set_spmf init ⟹ lossless_spmf (oracle c_o s' x)"
and lossless_eval: "⋀c_a c_o s s' guess. (c_o, c_a, s) ∈ set_spmf init ⟹ lossless_spmf (eval c_o c_a s' guess)"
including lifting_syntax
proof -
define eval_oracle'
where "eval_oracle' = (λc_o c_a ((id, occ :: nat option), s') guess.
map_spmf (λb'. case occ of Some j⇩0 ⇒ ((), (Suc id, Some j⇩0), s')
| None ⇒ ((), (Suc id, (if b' then Some id else None)), s'))
(eval c_o c_a s' guess))"
let ?multi'_body = "λc_o c_a s. exec_gpv (†(oracle c_o) ⊕⇩O eval_oracle' c_o c_a) (𝒜 c_a) ((0, None), s)"
define game_multi' where "game_multi' = (λc_o c_a s. do {
(_, ((id, j⇩0), s' :: 's)) ← ?multi'_body c_o c_a s;
return_spmf (j⇩0 ≠ None) })"

define initialize :: "('c_o ⇒ 'c_a ⇒ 's ⇒ nat ⇒ bool spmf) ⇒ bool spmf" where
"initialize body = do {
(c_o, c_a, s) ← init;
j⇩s ← spmf_of_set {..<q};
body c_o c_a s j⇩s }" for body
define body2 where "body2 c_o c_a s j⇩s = do {
(_, (id, j⇩0), s') ← ?multi'_body c_o c_a s;
return_spmf (j⇩0 = Some j⇩s) }" for c_o c_a s j⇩s
let ?game2 = "initialize body2"

define stop_oracle where "stop_oracle = (λc_o.
(λ(idgs, s) x. case idgs of Inr _ ⇒ map_spmf (λ(y, s). (Some y, (idgs, s))) (oracle c_o s x) | Inl _ ⇒ return_spmf (None, (idgs, s)))
⊕⇩O⇧S
(λ(idgs, s) guess :: 'guess. return_spmf (case idgs of Inr 0 ⇒ (None, Inl (guess, s), s) | Inr (Suc i) ⇒ (Some (), Inr i, s) | Inl _ ⇒ (None, idgs, s))))"
define body3 where "body3 c_o c_a s j⇩s = do {
(_ :: unit option, idgs, _) ← exec_gpv_stop (stop_oracle c_o) (𝒜 c_a) (Inr j⇩s, s);
(b' :: bool) ← case idgs of Inr _ ⇒ return_spmf False | Inl (g, s') ⇒ eval c_o c_a s' g;
return_spmf b' }" for c_o c_a s j⇩s
let ?game3 = "initialize body3"

{ define S :: "bool ⇒ nat × nat option ⇒ bool" where "S ≡ λb' (id, occ). b' ⟷ (∃j⇩0. occ = Some j⇩0)"
let ?S = "rel_prod S (=)"

define initial :: "nat × nat option" where "initial = (0, None)"
define result :: "nat × nat option ⇒ bool" where "result p = (snd p ≠ None)" for p
have [transfer_rule]: "(S ===> (=)) (λb. b) result" by(simp add: rel_fun_def result_def S_def)
have [transfer_rule]: "S False initial" by (simp add: S_def initial_def)

have eval_oracle'[transfer_rule]:
"((=) ===> (=) ===> ?S ===> (=) ===> rel_spmf (rel_prod (=) ?S))
eval_oracle eval_oracle'"
unfolding eval_oracle_def[abs_def] eval_oracle'_def[abs_def]
by (auto simp add: rel_fun_def S_def map_spmf_conv_bind_spmf intro!: rel_spmf_bind_reflI split: option.split)

have game_multi': "game_multi 𝒜 = bind_spmf init (λ(c_o, c_a, s). game_multi' c_o c_a s)"
unfolding game_multi_def game_multi'_def initial_def[symmetric]
by (rewrite in "case_prod ⌑" in "bind_spmf _ (case_prod ⌑)" in "_ = bind_spmf _ ⌑" split_def)
(fold result_def; transfer_prover) }
moreover
have "spmf (game_multi' c_o c_a s) True = spmf (bind_spmf (spmf_of_set {..<q}) (body2 c_o c_a s)) True * q"
if "(c_o, c_a, s) ∈ set_spmf init" for c_o c_a s
proof -
have bnd: "interaction_bounded_by (Not ∘ isl) (𝒜 c_a) q" using bound that by blast

have bound_occ: "j⇩s < q" if that: "((), (id, Some j⇩s), s') ∈ set_spmf (?multi'_body c_o c_a s)"
for s' id j⇩s
proof -
have "id ≤ q"
by(rule oi_True.interaction_bounded_by'_exec_gpv_count[OF bnd that, where count="fst ∘ fst", simplified])
(auto simp add: eval_oracle'_def split: plus_oracle_split_asm option.split_asm)
moreover let ?I = "λ((id, occ), s'). case occ of None ⇒ True | Some j⇩s ⇒ j⇩s < id"
have "callee_invariant (†(oracle c_o) ⊕⇩O eval_oracle' c_o c_a) ?I"
by(clarsimp simp add: split_def intro!: conjI[OF callee_invariant_extend_state_oracle_const'])
(unfold_locales; auto simp add: eval_oracle'_def split: option.split_asm)
from callee_invariant_on.exec_gpv_invariant[OF this that] have "j⇩s < id" by simp
ultimately show ?thesis by simp
qed

let ?M = "measure (measure_spmf (?multi'_body c_o c_a s))"
have "spmf (game_multi' c_o c_a s) True = ?M {(u, (id, j⇩0), s'). j⇩0 ≠ None}"
by(auto simp add: game_multi'_def map_spmf_conv_bind_spmf[symmetric] split_def spmf_conv_measure_spmf measure_map_spmf vimage_def)
also have "{(u, (id, j⇩0), s'). j⇩0 ≠ None} =
{((), (id, Some j⇩s), s') |j⇩s s' id. j⇩s < q} ∪ {((), (id, Some j⇩s), s') |j⇩s s' id. j⇩s ≥ q}"
(is "_ = ?A ∪ _") by auto
also have "?M … = ?M ?A"
by (rule measure_spmf.measure_zero_union)(auto simp add: measure_spmf_zero_iff dest: bound_occ)
also have "… = measure (measure_spmf (pair_spmf (spmf_of_set {..< q}) (?multi'_body c_o c_a s)))
{(j⇩s, (), (id, j⇩0), s') |j⇩s j⇩0 s' id. j⇩0 = Some j⇩s } * q"
(is "_ = measure ?M' ?B * _")
proof -
have "?B = {(j⇩s, (), (id, j⇩0), s') |j⇩s j⇩0 s' id. j⇩0 = Some j⇩s ∧ j⇩s < q} ∪
{(j⇩s, (), (id, j⇩0), s') |j⇩s j⇩0 s' id. j⇩0 = Some j⇩s ∧ j⇩s ≥ q}" (is "_ = ?Set1 ∪ ?Set2")
by auto
then have "measure ?M' ?B = measure ?M' (?Set1 ∪ ?Set2)" by simp
also have "… = measure ?M' ?Set1"
by (rule measure_spmf.measure_zero_union) (auto simp add: measure_spmf_zero_iff)
also have "… = (∑j∈{0..<q}. measure ?M' ({j} × {((), (id, Some j), s')|s' id. True}))"
by(subst measure_spmf.finite_measure_finite_Union[symmetric])
(auto intro!: arg_cong2[where f=measure] simp add: disjoint_family_on_def)
also have "… = (∑j∈{0..<q}. 1 / q * measure (measure_spmf (?multi'_body c_o c_a s)) {((), (id, Some j), s')|s' id. True})"
also have "… = 1 / q * measure (measure_spmf (?multi'_body c_o c_a s)) {((), (id, Some j⇩s), s')|j⇩s s' id. j⇩s < q}"
unfolding sum_distrib_left[symmetric]
by(subst measure_spmf.finite_measure_finite_Union[symmetric])
(auto intro!: arg_cong2[where f=measure] simp add: disjoint_family_on_def)
finally show ?thesis by simp
qed
also have "?B = (λ(j⇩s, _, (_, j⇩0), _). j⇩0 = Some j⇩s) - {True}"
also have rw2: "measure ?M' … = spmf (bind_spmf (spmf_of_set {..<q}) (body2 c_o c_a s)) True"
by (simp add: body2_def[abs_def] measure_map_spmf[symmetric] map_spmf_conv_bind_spmf
split_def pair_spmf_alt_def spmf_conv_measure_spmf[symmetric])
finally show ?thesis .
qed
hence "spmf (bind_spmf init (λ(c_a, c_o, s). game_multi' c_a c_o s)) True = spmf ?game2 True * q"
unfolding initialize_def spmf_bind[where p=init]
by (auto intro!: integral_cong_AE simp del: integral_mult_left_zero simp add: integral_mult_left_zero[symmetric])

moreover
have "ord_spmf (⟶) (body2 c_o c_a s j⇩s) (body3 c_o c_a s j⇩s)"
if init: "(c_o, c_a, s) ∈ set_spmf init" and j⇩s: "j⇩s < Suc q" for c_o c_a s j⇩s
proof -
define oracle2' where "oracle2' ≡ λ(b, (id, gs), s) guess. if id = j⇩s then do {
b' :: bool ← eval c_o c_a s guess;
return_spmf ((), (Some b', (Suc id, Some (guess, s)), s))
} else return_spmf ((), (b, (Suc id, gs), s))"

let ?R = "λ((id1, j⇩0), s1) (b', (id2, gs), s2). s1 = s2 ∧ id1 = id2 ∧ (j⇩0 = Some j⇩s ⟶ b' = Some True) ∧ (id2 ≤ j⇩s ⟶ b' = None)"
from init have "rel_spmf (rel_prod (=) ?R)
(exec_gpv (extend_state_oracle (oracle c_o) ⊕⇩O eval_oracle' c_o c_a) (𝒜 c_a) ((0, None), s))
(exec_gpv (extend_state_oracle (extend_state_oracle (oracle c_o)) ⊕⇩O oracle2') (𝒜 c_a) (None, (0, None), s))"
by(intro exec_gpv_oracle_bisim[where X="?R"])(auto simp add: oracle2'_def eval_oracle'_def spmf_rel_map map_spmf_conv_bind_spmf[symmetric] rel_spmf_return_spmf2 lossless_eval o_def intro!: rel_spmf_reflI split: option.split_asm plus_oracle_split if_split_asm)
then have "rel_spmf (⟶) (body2 c_o c_a s j⇩s)
(do {
(_, b', _, _) ← exec_gpv (††(oracle c_o) ⊕⇩O oracle2') (𝒜 c_a) (None, (0, None), s);
return_spmf (b' = Some True) })"
(is "rel_spmf _ _ ?body2'")
― ‹We do not get equality here because the right hand side may return @{const True} even
when the bad event has happened before the @{text j⇩s}-th iteration.›
unfolding body2_def by(rule rel_spmf_bindI) clarsimp
also
let ?guess_oracle = "λ((id, gs), s) guess. return_spmf ((), (Suc id, if id = j⇩s then Some (guess, s) else gs), s)"
let ?I = "λ(idgs, s). case idgs of (_, None) ⇒ False | (i, Some _) ⇒ j⇩s < i"
interpret I: callee_invariant_on "†(oracle c_o) ⊕⇩O ?guess_oracle" "?I" ℐ_full
by(simp)(unfold_locales; auto split: option.split)

let ?f = "λs. case snd (fst s) of None ⇒ return_spmf False | Some a ⇒ eval c_o c_a (snd a) (fst a)"
let ?X = "λj⇩s (b1, (id1, gs1), s1) (b2, (id2, gs2), s2). b1 = b2 ∧ id1 = id2 ∧ gs1 = gs2 ∧ s1 = s2 ∧ (b2 = None ⟷ gs2 = None) ∧ (id2 ≤ j⇩s ⟶ b2 = None)"
have "?body2' = do {
(a, r, s) ← exec_gpv (λ(r, s) x. do {
(y, s') ← (†(oracle c_o) ⊕⇩O ?guess_oracle) s x;
if ?I s' ∧ r = None then map_spmf (λr. (y, Some r, s')) (?f s') else return_spmf (y, r, s')
})
(𝒜 c_a) (None, (0, None), s);
case r of None ⇒ ?f s ⤜ return_spmf | Some r' ⇒ return_spmf r' }"
unfolding oracle2'_def spmf_rel_eq[symmetric]
by(rule rel_spmf_bindI[OF exec_gpv_oracle_bisim'[where X="?X j⇩s"]])
(auto simp add: bind_map_spmf o_def spmf.map_comp split_beta conj_comms map_spmf_conv_bind_spmf[symmetric] spmf_rel_map rel_spmf_reflI cong: conj_cong split: plus_oracle_split)
also have "… = do {
us' ← exec_gpv (†(oracle c_o) ⊕⇩O ?guess_oracle) (𝒜 c_a) ((0, None), s);
(b' :: bool) ← ?f (snd us');
return_spmf b' }"
(is "_ = ?body2''")
by(rule I.exec_gpv_bind_materialize[symmetric])(auto split: plus_oracle_split_asm option.split_asm)
also have "… = do {
us' ← exec_gpv_stop (lift_stop_oracle (†(oracle c_o) ⊕⇩O ?guess_oracle)) (𝒜 c_a) ((0, None), s);
(b' :: bool) ← ?f (snd us');
return_spmf b' }"
supply lift_stop_oracle_transfer[transfer_rule] gpv_stop_transfer[transfer_rule] exec_gpv_parametric'[transfer_rule]
by transfer simp
also let ?S = "λ((id1, gs1), s1) ((id2, gs2), s2). gs1 = gs2 ∧ (gs2 = None ⟶ s1 = s2 ∧ id1 = id2) ∧ (gs1 = None ⟷ id1 ≤ j⇩s)"
have "ord_spmf (⟶) … (exec_gpv_stop ((λ((id, gs), s) x. case gs of None ⇒ lift_stop_oracle (†(oracle c_o)) ((id, gs), s) x | Some _ ⇒ return_spmf (None, ((id, gs), s))) ⊕⇩O⇧S
(λ((id, gs), s) guess. return_spmf (if id ≥ j⇩s then None else Some (), (Suc id, if id = j⇩s then Some (guess, s) else gs), s)))
(𝒜 c_a) ((0, None), s) ⤜
(λus'. case snd (fst (snd us')) of None ⇒ return_spmf False | Some a ⇒ eval c_o c_a (snd a) (fst a)))"
unfolding body3_def stop_oracle_def
by(rule ord_spmf_exec_gpv_stop[where stop = "λ((id, guess), _). guess ≠ None" and S="?S", THEN ord_spmf_bindI])
(auto split: prod.split_asm plus_oracle_split_asm split!: plus_oracle_stop_split simp del: not_None_eq simp add: spmf.map_comp o_def apfst_compose ord_spmf_map_spmf1 ord_spmf_map_spmf2 split_beta ord_spmf_return_spmf2 intro!: ord_spmf_reflI)
also let ?X = "λ((id, gs), s1) (idgs, s2). s1 = s2 ∧ (case (gs, idgs) of (None, Inr id') ⇒ id' = j⇩s - id ∧ id ≤ j⇩s | (Some gs, Inl gs') ⇒ gs = gs' ∧ id > j⇩s | _ ⇒ False)"
have "… = body3 c_o c_a s j⇩s" unfolding body3_def spmf_rel_eq[symmetric] stop_oracle_def
by(rule exec_gpv_oracle_bisim'[where X="?X", THEN rel_spmf_bindI])
(auto split: option.split_asm plus_oracle_stop_split nat.splits split!: sum.split simp add: spmf_rel_map intro!: rel_spmf_reflI)
finally show ?thesis by(rule pmf.rel_mono_strong)(auto elim!: option.rel_cases ord_option.cases)
qed
{ then have "ord_spmf (⟶) ?game2 ?game3"
by(clarsimp simp add: initialize_def intro!: ord_spmf_bind_reflI)
also
let ?X = "λ(gsid, s) (gid, s'). s = s' ∧ rel_sum (λ(g, s1) g'. g = g' ∧ s1 = s') (=) gsid gid"
have "rel_spmf (⟶) ?game3 (game_single (reduction q 𝒜))"
unfolding body3_def stop_oracle_def game_single_def reduction_def split_def initialize_def
apply(clarsimp simp add: bind_map_spmf exec_gpv_bind exec_gpv_inline intro!: rel_spmf_bind_reflI)
apply(rule rel_spmf_bindI[OF exec_gpv_oracle_bisim'[where X="?X"]])
apply(auto split: plus_oracle_stop_split elim!: rel_sum.cases simp add: map_spmf_conv_bind_spmf[symmetric] split_def spmf_rel_map rel_spmf_reflI rel_spmf_return_spmf1 lossless_eval split: nat.split)
done
finally have "ord_spmf (⟶) ?game2 (game_single (reduction q 𝒜))"
by(rule pmf.rel_mono_strong)(auto elim!: option.rel_cases ord_option.cases)
from this[THEN ord_spmf_measureD, of "{True}"]
have "spmf ?game2 True ≤ spmf (game_single (reduction q 𝒜)) True" unfolding spmf_conv_measure_spmf
by(rule ord_le_eq_trans)(auto intro: arg_cong2[where f=measure]) }
qed

end

end


# Theory Unpredictable_Function

(* Title: Unpredictable_Function.thy
Author: Andreas Lochbihler, ETH Zurich
Author: S. Reza Sefidgar, ETH Zurich *)

subsection ‹Unpredictable function›

theory Unpredictable_Function imports
Guessing_Many_One
begin

locale upf =
fixes key_gen :: "'key spmf"
and hash :: "'key ⇒ 'x ⇒ 'hash"
begin

type_synonym ('x', 'hash') adversary = "(unit, 'x' + ('x' × 'hash'), 'hash' + unit) gpv"

definition oracle_hash :: "'key ⇒ ('x, 'hash, 'x set) callee"
where
"oracle_hash k = (λL y. do {
let t = hash k y;
let L = insert y L;
return_spmf (t, L)
})"

definition oracle_flag :: "'key ⇒ ('x × 'hash, unit, bool × 'x set) callee"
where
"oracle_flag = (λkey (flg, L) (y, t).
return_spmf ((), (flg ∨ (t = (hash key y) ∧ y ∉ L), L)))"

abbreviation "oracle" :: "'key ⇒ ('x + 'x × 'hash, 'hash + unit, bool × 'x set) callee"
where "oracle key ≡ †(oracle_hash key) ⊕⇩O oracle_flag key"

definition game :: "('x, 'hash) adversary ⇒ bool spmf"
where
"game 𝒜 = do {
key ← key_gen;
(_, (flag', L')) ← exec_gpv (oracle key) 𝒜 (False, {});
return_spmf flag'
}"

where "advantage 𝒜 = spmf (game 𝒜) True"

type_synonym ('x', 'hash') adversary1 = "('x' × 'hash', 'x', 'hash') gpv"

definition game1 :: "('x, 'hash) adversary1 ⇒ bool spmf"
where
"game1 𝒜 = do {
key ← key_gen;
((m, h), L) ← exec_gpv (oracle_hash key) 𝒜 {};
return_spmf (h = hash key m ∧ m ∉ L)
}"

where "advantage1 𝒜 = spmf (game1 𝒜) True"

assumes bound: "interaction_bounded_by (Not ∘ isl) 𝒜 q"
shows "advantage 𝒜 ≤ advantage1 (guessing_many_one.reduction q (λ_ :: unit. 𝒜) ()) * q"
proof -
let ?init = "map_spmf (λkey. (key, (), {})) key_gen"
let ?oracle = "λkey . oracle_hash key"
let ?eval = "λkey (_ :: unit) L (x, h). return_spmf (h = hash key x ∧ x ∉ L)"

interpret guessing_many_one ?init ?oracle ?eval .

have [simp]: "oracle_flag key = eval_oracle key ()" for key
have "game 𝒜 = game_multi (λ_. 𝒜)"
by(auto simp add: game_multi_def game_def bind_map_spmf intro!: bind_spmf_cong[OF refl])
also have "… ≤ advantage_single (reduction q (λ_. 𝒜)) * q" using bound
also have "advantage_single (reduction q (λ_. 𝒜)) = advantage1 (reduction q (λ_. 𝒜) ())" for 𝒜
by(auto simp add: game1_def game_single_def bind_map_spmf o_def intro!: bind_spmf_cong[OF refl] arg_cong2[where f=spmf])
finally show ?thesis .
qed

end

end


# Theory Security_Spec

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

theory Security_Spec imports
Diffie_Hellman
IND_CCA2
IND_CCA2_sym
IND_CPA
IND_CPA_PK
IND_CPA_PK_Single
SUF_CMA
Pseudo_Random_Function
Pseudo_Random_Permutation
Unpredictable_Function
begin

end


# Theory Elgamal

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

section ‹Cryptographic constructions and their security›

theory Elgamal imports
CryptHOL.Cyclic_Group_SPMF
CryptHOL.Computational_Model
Diffie_Hellman
IND_CPA_PK_Single
CryptHOL.Negligible
begin

subsection ‹Elgamal encryption scheme›

locale elgamal_base =
fixes 𝒢 :: "'grp cyclic_group" (structure)
begin

type_synonym 'grp' pub_key = "'grp'"
type_synonym 'grp' priv_key = nat
type_synonym 'grp' plain = 'grp'
type_synonym 'grp' cipher = "'grp' × 'grp'"

definition key_gen :: "('grp pub_key × 'grp priv_key) spmf"
where
"key_gen = do {
x ← sample_uniform (order 𝒢);
return_spmf (❙g [^] x, x)
}"

lemma key_gen_alt:
"key_gen = map_spmf (λx. (❙g [^] x, x)) (sample_uniform (order 𝒢))"

definition aencrypt :: "'grp pub_key ⇒ 'grp ⇒ 'grp cipher spmf"
where
"aencrypt α msg = do {
y ← sample_uniform (order 𝒢);
return_spmf (❙g [^] y, (α [^] y) ⊗ msg)
}"

lemma aencrypt_alt:
"aencrypt α msg = map_spmf (λy. (❙g [^] y, (α [^] y) ⊗ msg)) (sample_uniform (order 𝒢))"

definition adecrypt :: "'grp priv_key ⇒ 'grp cipher ⇒ 'grp option"
where
"adecrypt x = (λ(β, ζ). Some (ζ ⊗ (inv (β [^] x))))"

abbreviation valid_plains :: "'grp ⇒ 'grp ⇒ bool"
where "valid_plains msg1 msg2 ≡ msg1 ∈ carrier 𝒢 ∧ msg2 ∈ carrier 𝒢"

sublocale ind_cpa: ind_cpa key_gen aencrypt adecrypt valid_plains .
sublocale ddh: ddh 𝒢 .

where
"elgamal_adversary (𝒜1, 𝒜2) α β γ = TRY do {
b ← coin_spmf;
((msg1, msg2), σ) ← 𝒜1 α;
― ‹have to check that the attacker actually sends two elements from the group; otherwise flip a coin›
_ :: unit ← assert_spmf (valid_plains msg1 msg2);
guess ← 𝒜2 (β, γ ⊗ (if b then msg1 else msg2)) σ;
return_spmf (guess = b)
} ELSE coin_spmf"

end

locale elgamal = elgamal_base + cyclic_group 𝒢
begin

proof -
obtain 𝒜1 and 𝒜2 where "𝒜 = (𝒜1, 𝒜2)" by(cases 𝒜)
note [simp] = this order_gt_0_iff_finite finite_carrier try_spmf_bind_out split_def o_def spmf_of_set bind_map_spmf weight_spmf_le_1 scale_bind_spmf bind_spmf_const
and [cong] = bind_spmf_cong_simp
have "ddh.ddh_1 (elgamal_adversary 𝒜) = TRY do {
x ← sample_uniform (order 𝒢);
y ← sample_uniform (order 𝒢);
((msg1, msg2), σ) ← 𝒜1 (❙g [^] x);
_ :: unit ← assert_spmf (valid_plains msg1 msg2);
b ← coin_spmf;
z ← map_spmf (λz. ❙g [^] z ⊗ (if b then msg1 else msg2)) (sample_uniform (order 𝒢));
guess ← 𝒜2 (❙g [^] y, z) σ;
return_spmf (guess ⟷ b)
} ELSE coin_spmf"
also have "… = TRY do {
x ← sample_uniform (order 𝒢);
y ← sample_uniform (order 𝒢);
((msg1, msg2), σ) ← 𝒜1 (❙g [^] x);
_ :: unit ← assert_spmf (valid_plains msg1 msg2);
z ← map_spmf (λz. ❙g [^] z) (sample_uniform (order 𝒢));
guess ← 𝒜2 (❙g [^] y, z) σ;
map_spmf ((=) guess) coin_spmf
} ELSE coin_spmf"
also have "… = coin_spmf"
also have "ddh.ddh_0 (elgamal_adversary 𝒜) = ind_cpa.ind_cpa 𝒜"
by(simp add: ddh.ddh_0_def IND_CPA_PK_Single.ind_cpa.ind_cpa_def key_gen_def aencrypt_def nat_pow_pow eq_commute)
qed

end

locale elgamal_asymp =
fixes 𝒢 :: "security ⇒ 'grp cyclic_group"
assumes elgamal: "⋀η. elgamal (𝒢 η)"
begin

sublocale elgamal "𝒢 η" for η by(simp add: elgamal)

theorem elgamal_secure:

end

context elgamal_base begin

lemma lossless_key_gen [simp]: "lossless_spmf (key_gen) ⟷ 0 < order 𝒢"

lemma lossless_aencrypt [simp]:
"lossless_spmf (aencrypt key plain) ⟷ 0 < order 𝒢"

"⟦ ind_cpa.lossless 𝒜; 0 < order 𝒢 ⟧
by(cases 𝒜)(simp add: ddh.lossless_def ind_cpa.lossless_def Let_def split_def)

end

end


# Theory Hashed_Elgamal

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

subsection ‹Hashed Elgamal in the Random Oracle Model›

theory Hashed_Elgamal imports
CryptHOL.GPV_Bisim
CryptHOL.Cyclic_Group_SPMF
CryptHOL.List_Bits
IND_CPA_PK
Diffie_Hellman
begin

type_synonym bitstring = "bool list"

locale hash_oracle = fixes len :: "nat" begin

type_synonym 'a state = "'a ⇀ bitstring"

definition "oracle" :: "'a state ⇒ 'a ⇒ (bitstring × 'a state) spmf"
where
"oracle σ x =
(case σ x of None ⇒ do {
bs ← spmf_of_set (nlists UNIV len);
return_spmf (bs, σ(x ↦ bs))
} | Some bs ⇒ return_spmf (bs, σ))"

abbreviation (input) initial :: "'a state" where "initial ≡ Map.empty"

inductive invariant :: "'a state ⇒ bool"
where
invariant: "⟦ finite (dom σ); length  ran σ ⊆ {len} ⟧ ⟹ invariant σ"

lemma invariant_initial [simp]: "invariant initial"
by(rule invariant.intros) auto

lemma invariant_update [simp]: "⟦ invariant σ; length bs = len ⟧ ⟹ invariant (σ(x ↦ bs))"

lemma invariant [intro!, simp]: "callee_invariant oracle invariant"
by unfold_locales(simp_all add: oracle_def in_nlists_UNIV split: option.split_asm)

lemma invariant_in_dom [simp]: "callee_invariant oracle (λσ. x ∈ dom σ)"
by unfold_locales(simp_all add: oracle_def split: option.split_asm)

lemma lossless_oracle [simp]: "lossless_spmf (oracle σ x)"

lemma card_dom_state:
assumes σ': "(x, σ') ∈ set_spmf (exec_gpv oracle gpv σ)"
and ibound: "interaction_any_bounded_by gpv n"
shows "card (dom σ') ≤ n + card (dom σ)"
proof(cases "finite (dom σ)")
case True
interpret callee_invariant_on "oracle" "λσ. finite (dom σ)" ℐ_full
by unfold_locales(auto simp add: oracle_def split: option.split_asm)
from ibound σ' _ _ _ True show ?thesis
by(rule interaction_bounded_by'_exec_gpv_count)(auto simp add: oracle_def card_insert_if simp del: fun_upd_apply split: option.split_asm)
next
case False
interpret callee_invariant_on "oracle" "λσ'. dom σ ⊆ dom σ'" ℐ_full
by unfold_locales(auto simp add: oracle_def split: option.split_asm)
from σ' have "dom σ ⊆ dom σ'" by(rule exec_gpv_invariant) simp_all
with False have "infinite (dom σ')" by(auto intro: finite_subset)
with False show ?thesis by simp
qed

end

locale elgamal_base =
fixes 𝒢 :: "'grp cyclic_group" (structure)
and len_plain :: "nat"
begin

sublocale hash: hash_oracle "len_plain" .
abbreviation hash :: "'grp ⇒ (bitstring, 'grp, bitstring) gpv"
where "hash x ≡ Pause x Done"

type_synonym 'grp' pub_key = "'grp'"
type_synonym 'grp' priv_key = nat
type_synonym plain = bitstring
type_synonym 'grp' cipher = "'grp' × bitstring"

definition key_gen :: "('grp pub_key × 'grp priv_key) spmf"
where
"key_gen = do {
x ← sample_uniform (order 𝒢);
return_spmf (❙g [^] x, x)
}"

definition aencrypt :: "'grp pub_key ⇒ plain ⇒ ('grp cipher, 'grp, bitstring) gpv"
where
"aencrypt α msg = do {
y ← lift_spmf (sample_uniform (order 𝒢));
h ← hash (α [^] y);
Done (❙g [^] y, h [⊕] msg)
}"

definition adecrypt :: "'grp priv_key ⇒ 'grp cipher ⇒ (plain, 'grp, bitstring) gpv"
where
"adecrypt x = (λ(β, ζ). do {
h ← hash (β [^] x);
Done (ζ [⊕] h)
})"

definition valid_plains :: "plain ⇒ plain ⇒ bool"
where "valid_plains msg1 msg2 ⟷ length msg1 = len_plain ∧ length msg2 = len_plain"

lemma lossless_aencrypt [simp]: "lossless_gpv ℐ (aencrypt α msg) ⟷ 0 < order 𝒢"

lemma interaction_bounded_by_aencrypt [interaction_bound, simp]:
"interaction_bounded_by (λ_. True) (aencrypt α msg) 1"
unfolding aencrypt_def by interaction_bound(simp add: one_enat_def SUP_le_iff)

sublocale ind_cpa: ind_cpa_pk "lift_spmf key_gen" aencrypt adecrypt valid_plains .
sublocale lcdh: lcdh 𝒢 .

:: "('grp pub_key, plain, 'grp cipher, 'grp, bitstring, 'state) ind_cpa.adversary
where
"elgamal_adversary (𝒜1, 𝒜2) α β = do {
(((msg1, msg2), σ), s) ← exec_gpv hash.oracle (𝒜1 α) hash.initial;
― ‹have to check that the attacker actually sends an element from the group; otherwise stop early›
TRY do {
_ :: unit ← assert_spmf (valid_plains msg1 msg2);
h' ← spmf_of_set (nlists UNIV len_plain);
(guess, s') ← exec_gpv hash.oracle (𝒜2 (β, h') σ) s;
return_spmf (dom s')
} ELSE return_spmf (dom s)
}"

end

locale elgamal = elgamal_base +
assumes cyclic_group: "cyclic_group 𝒢"
begin

interpretation cyclic_group 𝒢 by(fact cyclic_group)

includes lifting_syntax
assumes lossless: "ind_cpa.lossless 𝒜"
proof -
note [cong del] = if_weak_cong and [split del] = if_split
and [simp] = map_lift_spmf gpv.map_id lossless_weight_spmfD map_spmf_bind_spmf bind_spmf_const
obtain 𝒜1 𝒜2 where 𝒜 [simp]: "𝒜 = (𝒜1, 𝒜2)" by(cases "𝒜")

interpret cyclic_group: cyclic_group 𝒢 by(rule cyclic_group)
from finite_carrier have [simp]: "order 𝒢 > 0" using order_gt_0_iff_finite by(simp)

from lossless have lossless1 [simp]: "⋀pk. lossless_gpv ℐ_full (𝒜1 pk)"
and lossless2 [simp]: "⋀σ cipher. lossless_gpv ℐ_full (𝒜2 σ cipher)"

define hash_oracle' where "hash_oracle' = (λσ x. do {
h ← hash x;
Done (h, insert x σ)
})"
have [simp]: "lossless_gpv ℐ_full (hash_oracle' σ x)" for σ x by(simp add: hash_oracle'_def)
have [simp]: "lossless_gpv ℐ_full (inline hash_oracle' (𝒜1 α) s)" for α s
by(rule lossless_inline[where ℐ=ℐ_full]) simp_all
define game0 where "game0 = TRY do {
(pk, _) ← lift_spmf key_gen;
b ← lift_spmf coin_spmf;
(((msg1, msg2), σ), s) ← inline hash_oracle' (𝒜1 pk) {};
assert_gpv (valid_plains msg1 msg2);
cipher ← aencrypt pk (if b then msg1 else msg2);
(guess, s') ← inline hash_oracle' (𝒜2 cipher σ) s;
Done (guess = b)
} ELSE lift_spmf coin_spmf"
{ define cr where "cr = (λ_ :: unit. λ_ :: 'a set. True)"
have [transfer_rule]: "cr () {}" by(simp add: cr_def)
have [transfer_rule]: "((=) ===> cr ===> cr) (λ_ σ. σ) insert" by(simp add: rel_fun_def cr_def)
have [transfer_rule]: "(cr ===> (=) ===> rel_gpv (rel_prod (=) cr) (=)) id_oracle hash_oracle'"
unfolding hash_oracle'_def id_oracle_def[abs_def] bind_gpv_Pause bind_rpv_Done by transfer_prover
have "ind_cpa.ind_cpa 𝒜 = game0" unfolding game0_def 𝒜 ind_cpa_pk.ind_cpa.simps
by(transfer fixing: 𝒢 len_plain 𝒜1 𝒜2)(simp add: bind_map_gpv o_def ind_cpa_pk.ind_cpa.simps split_def) }
note game0 = this
have game0_alt_def: "game0 = do {
x ← lift_spmf (sample_uniform (order 𝒢));
b ← lift_spmf coin_spmf;
(((msg1, msg2), σ), s) ← inline hash_oracle' (𝒜1 (❙g [^] x)) {};
TRY do {
_ :: unit ← assert_gpv (valid_plains msg1 msg2);
cipher ← aencrypt (❙g [^] x) (if b then msg1 else msg2);
(guess, s') ← inline hash_oracle' (𝒜2 cipher σ) s;
Done (guess = b)
} ELSE lift_spmf coin_spmf
}"
by(simp add: split_def game0_def key_gen_def lift_spmf_bind_spmf bind_gpv_assoc try_gpv_bind_lossless[symmetric])

define hash_oracle'' where "hash_oracle'' = (λ(s, σ) (x :: 'a). do {
(h, σ') ← case σ x of
None ⇒ bind_spmf (spmf_of_set (nlists UNIV len_plain)) (λbs. return_spmf (bs, σ(x ↦ bs)))
| Some (bs :: bitstring) ⇒ return_spmf (bs, σ);
return_spmf (h, insert x s, σ')
})"
have *: "exec_gpv hash.oracle (inline hash_oracle' 𝒜 s) σ =
map_spmf (λ(a, b, c). ((a, b), c)) (exec_gpv hash_oracle'' 𝒜 (s, σ))" for 𝒜 σ s
by(simp add: hash_oracle'_def hash_oracle''_def hash.oracle_def Let_def exec_gpv_inline exec_gpv_bind o_def split_def cong del: option.case_cong_weak)
have [simp]: "lossless_spmf (hash_oracle'' s plain)" for s plain
by(simp add: hash_oracle''_def Let_def split: prod.split option.split)
have [simp]: "lossless_spmf (exec_gpv hash_oracle'' (𝒜1 α) s)" for s α
by(rule lossless_exec_gpv[where ℐ=ℐ_full]) simp_all
have [simp]: "lossless_spmf (exec_gpv hash_oracle'' (𝒜2 σ cipher) s)" for σ cipher s
by(rule lossless_exec_gpv[where ℐ=ℐ_full]) simp_all

let ?sample = "λf. bind_spmf (sample_uniform (order 𝒢)) (λx. bind_spmf (sample_uniform (order 𝒢)) (f x))"
define game1 where "game1 = (λ(x :: nat) (y :: nat). do {
b ← coin_spmf;
(((msg1, msg2), σ), (s, s_h)) ← exec_gpv hash_oracle'' (𝒜1 (❙g [^] x)) ({}, hash.initial);
TRY do {
_ :: unit ← assert_spmf (valid_plains msg1 msg2);
(h, s_h') ← hash.oracle s_h (❙g [^] (x * y));
let cipher = (❙g [^] y, h [⊕] (if b then msg1 else msg2));
(guess, (s', s_h'')) ← exec_gpv hash_oracle'' (𝒜2 cipher σ) (s, s_h');
return_spmf (guess = b, ❙g [^] (x * y) ∈ s')
} ELSE do {
b ← coin_spmf;
return_spmf (b, ❙g [^] (x * y) ∈ s)
}
})"
have game01: "run_gpv hash.oracle game0 hash.initial = map_spmf fst (?sample game1)"
apply(simp add: exec_gpv_bind split_def bind_gpv_assoc aencrypt_def game0_alt_def game1_def o_def bind_map_spmf if_distribs * try_bind_assert_gpv try_bind_assert_spmf lossless_inline[where ℐ=ℐ_full] bind_rpv_def nat_pow_pow del: bind_spmf_const)

define game2 where "game2 = (λ(x :: nat) (y :: nat). do {
b ← coin_spmf;
(((msg1, msg2), σ), (s, s_h)) ← exec_gpv hash_oracle'' (𝒜1 (❙g [^] x)) ({}, hash.initial);
TRY do {
_ :: unit ← assert_spmf (valid_plains msg1 msg2);
h ← spmf_of_set (nlists UNIV len_plain);
― ‹We do not do the lookup in ‹s_h› here, so the rest differs only if the adversary guessed ‹y››
let cipher = (❙g [^] y, h [⊕] (if b then msg1 else msg2));
(guess, (s', s_h')) ← exec_gpv hash_oracle'' (𝒜2 cipher σ) (s, s_h);
return_spmf (guess = b, ❙g [^] (x * y) ∈ s')
} ELSE do {
b ← coin_spmf;
return_spmf (b, ❙g [^] (x * y) ∈ s)
}
})"
interpret inv'': callee_invariant_on "hash_oracle''" "λ(s, s_h). s = dom s_h" ℐ_full
by unfold_locales(auto simp add: hash_oracle''_def split: option.split_asm if_split)
have in_encrypt_oracle: "callee_invariant hash_oracle'' (λ(s, _). x ∈ s)" for x

{ fix x y :: nat
let ?bad = "λ(s, s_h). ❙g [^] (x * y) ∈ s"
let ?X = "λ(s, s_h) (s', s_h'). s = dom s_h ∧ s' = s ∧ s_h = s_h'(❙g [^] (x * y) := None)"
have bisim:
"rel_spmf (λ(a, s1') (b, s2'). ?bad s1' = ?bad s2' ∧ (¬ ?bad s2' ⟶ a = b ∧ ?X s1' s2'))
(hash_oracle'' s1 plain) (hash_oracle'' s2 plain)"
if "?X s1 s2" for s1 s2 plain using that
by(auto split: prod.splits intro!: rel_spmf_bind_reflI simp add: hash_oracle''_def rel_spmf_return_spmf2 fun_upd_twist split: option.split dest!: fun_upd_eqD)
by(unfold_locales)(auto simp add: hash_oracle''_def split: option.split_asm)
unfolding game1_def game2_def
apply(clarsimp simp add: split_def o_def hash.oracle_def rel_spmf_bind_reflI if_distribs intro!: rel_spmf_bind_reflI simp del: bind_spmf_const)
apply(rule rel_spmf_try_spmf)
subgoal for b msg1 msg2 σ s s_h
apply(rule rel_spmf_bind_reflI)
apply(drule inv''.exec_gpv_invariant; clarsimp)
apply(cases "s_h (❙g [^] (x * y))")
subgoal ― ‹case @{const None}›
apply(clarsimp intro!: rel_spmf_bind_reflI)
apply(rule rel_spmf_bindI)
apply(rule exec_gpv_oracle_bisim_bad_full[OF _ _ bisim inv inv, where R="λ(x, s1) (y, s2). ?bad s1 = ?bad s2 ∧ (¬ ?bad s2 ⟶ x = y)"]; clarsimp simp add: fun_upd_idem; fail)
apply clarsimp
done
subgoal by(auto intro!: rel_spmf_bindI1 rel_spmf_bindI2 lossless_exec_gpv[where ℐ=ℐ_full] dest!: callee_invariant_on.exec_gpv_invariant[OF in_encrypt_oracle])
done
subgoal by(rule rel_spmf_reflI) simp
done }
by(intro rel_spmf_bind_reflI)
hence "¦measure (measure_spmf (?sample game2)) {(x, _). x} - measure (measure_spmf (?sample game1)) {(y, _). y}¦
unfolding split_def by(rule fundamental_lemma)
moreover have "measure (measure_spmf (?sample game2)) {(x, _). x} = spmf (map_spmf fst (?sample game2)) True"
and "measure (measure_spmf (?sample game1)) {(y, _). y} = spmf (map_spmf fst (?sample game1)) True"
and "measure (measure_spmf (?sample game2)) {(_, bad). bad} = spmf (map_spmf snd (?sample game2)) True"
unfolding spmf_conv_measure_spmf measure_map_spmf by(rule arg_cong2[where f=measure]; fastforce)+
ultimately have hop23: "¦spmf (map_spmf fst (?sample game2)) True - spmf (map_spmf fst (?sample game1)) True¦ ≤ spmf (map_spmf snd (?sample game2)) True" by simp

define game3
where "game3 = (λf :: _ ⇒ _ ⇒ _ ⇒ bitstring spmf ⇒ _ spmf. λ(x :: nat) (y :: nat). do {
b ← coin_spmf;
(((msg1, msg2), σ), (s, s_h)) ← exec_gpv hash_oracle'' (𝒜1 (❙g [^] x)) ({}, hash.initial);
TRY do {
_ :: unit ← assert_spmf (valid_plains msg1 msg2);
h' ← f b msg1 msg2 (spmf_of_set (nlists UNIV len_plain));
let cipher = (❙g [^] y, h');
(guess, (s', s_h')) ← exec_gpv hash_oracle'' (𝒜2 cipher σ) (s, s_h);
return_spmf (guess = b, ❙g [^] (x * y) ∈ s')
} ELSE do {
b ← coin_spmf;
return_spmf (b, ❙g [^] (x * y) ∈ s)
}
})"
let ?f = "λb msg1 msg2. map_spmf (λh. (if b then msg1 else msg2) [⊕] h)"
have "game2 x y = game3 ?f x y" for x y
unfolding game2_def game3_def by(simp add: Let_def bind_map_spmf xor_list_commute o_def nat_pow_pow)
also have "game3 ?f x y = game3 (λ_ _ _ x. x) x y" for x y (* optimistic sampling *)
unfolding game3_def
by(auto intro!: try_spmf_cong bind_spmf_cong[OF refl] if_cong[OF refl] simp add: split_def one_time_pad valid_plains_def simp del: map_spmf_of_set_inj_on bind_spmf_const split: if_split)
finally have game23: "game2 x y = game3 (λ_ _ _ x. x) x y" for x y .

define hash_oracle''' where "hash_oracle''' = (λ(σ :: 'a ⇒ _). hash.oracle σ)"
{ define bisim where "bisim = (λσ (s :: 'a set, σ' :: 'a ⇀ bitstring). s = dom σ ∧ σ = σ')"
have [transfer_rule]: "bisim Map_empty ({}, Map_empty)" by(simp add: bisim_def)
have [transfer_rule]: "(bisim ===> (=) ===> rel_spmf (rel_prod (=) bisim)) hash_oracle''' hash_oracle''"
by(auto simp add: hash_oracle''_def split_def hash_oracle'''_def spmf_rel_map hash.oracle_def rel_fun_def bisim_def split: option.split intro!: rel_spmf_bind_reflI)
have * [transfer_rule]: "(bisim ===> (=)) dom fst" by(simp add: bisim_def rel_fun_def)
have * [transfer_rule]: "(bisim ===> (=)) (λx. x) snd" by(simp add: rel_fun_def bisim_def)
have "game3 (λ_ _ _ x. x) x y = do {
b ← coin_spmf;
(((msg1, msg2), σ), s) ← exec_gpv hash_oracle''' (𝒜1 (❙g [^] x)) hash.initial;
TRY do {
_ :: unit ← assert_spmf (valid_plains msg1 msg2);
h' ← spmf_of_set (nlists UNIV len_plain);
let cipher = (❙g [^] y, h');
(guess, s') ← exec_gpv hash_oracle''' (𝒜2 cipher σ) s;
return_spmf (guess = b, ❙g [^] (x * y) ∈ dom s')
} ELSE do {
b ← coin_spmf;
return_spmf (b, ❙g [^] (x * y) ∈ dom s)
}
}" for x y
unfolding game3_def Map_empty_def[symmetric] split_def fst_conv snd_conv prod.collapse
by(transfer fixing: 𝒜1 𝒢 len_plain x y 𝒜2) simp
moreover have "map_spmf snd (… x y) = do {
zs ← elgamal_adversary 𝒜 (❙g [^] x) (❙g [^] y);
return_spmf (❙g [^] (x * y) ∈ zs)
}" for x y
by(simp add: o_def split_def hash_oracle'''_def map_try_spmf map_scale_spmf)
(simp add: o_def map_try_spmf map_scale_spmf map_spmf_conv_bind_spmf[symmetric] spmf.map_comp map_const_spmf_of_set)
ultimately have "map_spmf snd (?sample (game3 (λ_ _ _ x. x))) = lcdh.lcdh (elgamal_adversary 𝒜)"
by(simp add: o_def lcdh.lcdh_def Let_def nat_pow_pow) }
then have game2_snd: "map_spmf snd (?sample game2) = lcdh.lcdh (elgamal_adversary 𝒜)"

have "map_spmf fst (game3 (λ_ _ _ x. x) x y) = do {
(((msg1, msg2), σ), (s, s_h)) ← exec_gpv hash_oracle'' (𝒜1 (❙g [^] x)) ({}, hash.initial);
TRY do {
_ :: unit ← assert_spmf (valid_plains msg1 msg2);
h' ← spmf_of_set (nlists UNIV len_plain);
(guess, (s', s_h')) ← exec_gpv hash_oracle'' (𝒜2 (❙g [^] y, h') σ) (s, s_h);
map_spmf ((=) guess) coin_spmf
} ELSE coin_spmf
}" for x y
by(simp add: game3_def o_def split_def map_spmf_conv_bind_spmf try_spmf_bind_out weight_spmf_le_1 scale_bind_spmf try_spmf_bind_out1 bind_scale_spmf)
then have game3_fst: "map_spmf fst (game3 (λ_ _ _ x. x) x y) = coin_spmf" for x y
by(simp add: o_def if_distribs spmf.map_comp map_eq_const_coin_spmf split_def)

have "ind_cpa.advantage hash.oracle hash.initial 𝒜 = ¦spmf (map_spmf fst (?sample game1)) True - 1 / 2¦"
also have "… = ¦1 / 2 - spmf (map_spmf fst (?sample game1)) True¦"
also have "1 / 2 = spmf (map_spmf fst (?sample game2)) True"
by(simp add: game23 o_def game3_fst spmf_of_set)
also note hop23 also note game2_snd
qed

end

context elgamal_base begin

lemma lossless_key_gen [simp]: "lossless_spmf key_gen ⟷ 0 < order 𝒢"

"⟦ ind_cpa.lossless 𝒜; ⋀η. 0 < order 𝒢 ⟧
by(cases 𝒜)(auto simp add: lcdh.lossless_def ind_cpa.lossless_def split_def Let_def intro!: lossless_exec_gpv[where ℐ=ℐ_full] lossless_inline)

end

end


# Theory RP_RF

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

subsection ‹The random-permutation random-function switching lemma›

theory RP_RF imports
Pseudo_Random_Function
Pseudo_Random_Permutation
CryptHOL.GPV_Bisim
begin

lemma rp_resample:
assumes "B ⊆ A ∪ C" "A ∩ C = {}" "C ⊆ B" and finB: "finite B"
shows "bind_spmf (spmf_of_set B) (λx. if x ∈ A then spmf_of_set C else return_spmf x) = spmf_of_set C"
proof(cases "C = {} ∨ A ∩ B = {}")
case False
define A' where "A' ≡ A ∩ B"
from False have C: "C ≠ {}" and A': "A' ≠ {}" by(auto simp add: A'_def)
have B: "B = A' ∪ C" using assms by(auto simp add: A'_def)
with finB have finA: "finite A'" and finC: "finite C" by simp_all
from assms have A'C: "A' ∩ C = {}" by(auto simp add: A'_def)
have "bind_spmf (spmf_of_set B) (λx. if x ∈ A then spmf_of_set C else return_spmf x) =
bind_spmf (spmf_of_set B) (λx. if x ∈ A' then spmf_of_set C else return_spmf x)"
by(rule bind_spmf_cong[OF refl])(simp add: set_spmf_of_set finB A'_def)
also have "… = spmf_of_set C" (is "?lhs = ?rhs")
proof(rule spmf_eqI)
fix i
have "(∑x∈C. spmf (if x ∈ A' then spmf_of_set C else return_spmf x) i) = indicator C i" using finA finC
by(simp add: disjoint_notin1[OF A'C] indicator_single_Some sum_mult_indicator[of C "λ_. 1 :: real" "λ_. _" "λx. x", simplified] split: split_indicator cong: conj_cong sum.cong)
then show "spmf ?lhs i = spmf ?rhs i" using B finA finC A'C C A'
qed
finally show ?thesis .
qed(use assms in ‹auto 4 3 cong: bind_spmf_cong_simp simp add: subsetD bind_spmf_const spmf_of_set_empty disjoint_notin1 intro!: arg_cong[where f=spmf_of_set]›)

locale rp_rf =
rp: random_permutation A +
rf: random_function "spmf_of_set A"
for A :: "'a set"
+
assumes finite_A: "finite A"
and nonempty_A: "A ≠ {}"
begin

type_synonym 'a' adversary = "(bool, 'a', 'a') gpv"

definition game :: "bool ⇒ 'a adversary ⇒ bool spmf" where
"game b 𝒜 = run_gpv (if b then rp.random_permutation else rf.random_oracle) 𝒜 Map.empty"

abbreviation prp_game :: "'a adversary ⇒ bool spmf" where "prp_game ≡ game True"
abbreviation prf_game :: "'a adversary ⇒ bool spmf" where "prf_game ≡ game False"

"advantage 𝒜 = ¦spmf (prp_game 𝒜) True - spmf (prf_game 𝒜) True¦"

by(auto simp add: advantage_def intro!: abs_leI)(metis diff_0_right diff_left_mono order_trans pmf_le_1 pmf_nonneg) +

context includes ℐ.lifting begin
lift_definition ℐ :: "('a, 'a) ℐ" is "(λx. if x ∈ A then A else {})" .
lemma outs_ℐ_ℐ [simp]: "outs_ℐ ℐ = A" by transfer auto
lemma responses_ℐ_ℐ [simp]: "responses_ℐ ℐ x = (if x ∈ A then A else {})" by transfer simp
lifting_update ℐ.lifting
lifting_forget ℐ.lifting
end

lemma rp_rf:
assumes bound: "interaction_any_bounded_by 𝒜 q"
and lossless: "lossless_gpv ℐ 𝒜"
and WT: "ℐ ⊢g 𝒜 √"
shows "advantage 𝒜 ≤ q * q / card A"
including lifting_syntax
proof -
let ?run = "λb. exec_gpv (if b then rp.random_permutation else rf.random_oracle) 𝒜 Map.empty"
define rp_bad :: "bool × ('a ⇀ 'a) ⇒ 'a ⇒ ('a × (bool × ('a ⇀ 'a))) spmf"
where "rp_bad = (λ(bad, σ) x. case σ x of Some y ⇒ return_spmf (y, (bad, σ))
| None ⇒ bind_spmf (spmf_of_set A) (λy. if y ∈ ran σ then map_spmf (λy'. (y', (True, σ(x ↦ y')))) (spmf_of_set (A - ran σ)) else return_spmf (y, (bad, (σ(x ↦ y))))))"
| None ⇒ bind_spmf (spmf_of_set A) (λy. if y ∈ ran σ then map_spmf (λy'. (y', (True, σ(x ↦ y')))) (spmf_of_set (A - ran σ)) else return_spmf (y, (bad, (σ(x ↦ y))))))"

let ?S = "rel_prod2 (=)"
define init :: "bool × ('a ⇀ 'a)" where "init = (False, Map.empty)"
have rp: "rp.random_permutation = (λσ x. case σ x of Some y ⇒ return_spmf (y, σ)
| None ⇒ bind_spmf (bind_spmf (spmf_of_set A) (λy. if y ∈ ran σ then spmf_of_set (A - ran σ) else return_spmf y)) (λy. return_spmf (y, σ(x ↦ y))))"
by(subst rp_resample)(auto simp add: finite_A rp.random_permutation_def[abs_def])
have [transfer_rule]: "(?S ===> (=) ===> rel_spmf (rel_prod (=) ?S)) rp.random_permutation rp_bad"
by(auto simp add: rel_fun_def map_spmf_conv_bind_spmf split: option.split intro!: rel_spmf_bind_reflI)
have [transfer_rule]: "?S Map.empty init" by(simp add: init_def)
have "spmf (prp_game 𝒜) True = spmf (run_gpv rp_bad 𝒜 init) True"
unfolding vimage_def game_def if_True by transfer_prover
moreover {
define collision :: "('a ⇀ 'a) ⇒ bool" where "collision m ⟷ ¬ inj_on m (dom m)" for m
have [simp]: "¬ collision Map.empty" by(simp add: collision_def)
have [simp]: "⟦ collision m; m x = None ⟧ ⟹ collision (m(x := y))" for m x y
by(auto simp add: collision_def fun_upd_idem dom_minus fun_upd_image dest: inj_on_fun_updD)
have collision_map_updI: "⟦ m x = None; y ∈ ran m ⟧ ⟹ collision (m(x ↦ y))" for m x y
by(auto simp add: collision_def ran_def intro: rev_image_eqI)
have collision_map_upd_iff: "¬ collision m ⟹ collision (m(x ↦ y)) ⟷ y ∈ ran m ∧ m x ≠ Some y" for m x y
by(auto simp add: collision_def ran_def fun_upd_idem intro: inj_on_fun_updI rev_image_eqI dest: inj_on_eq_iff)

and ?X = "λσ1 (bad, σ2). σ1 = σ2 ∧ ¬ collision σ1 ∧ ¬ bad"
and ?I1 = "λσ1. dom σ1 ⊆ A ∧ ran σ1 ⊆ A"
and ?I2 = "λ(bad, σ2). dom σ2 ⊆ A ∧ ran σ2 ⊆ A"
let ?X_bad = "λσ1 s2. ?I1 σ1 ∧ ?I2 s2"
have [simp]: "ℐ ⊢c rf.random_oracle s1 √" if "ran s1 ⊆ A" for s1 using that
by(intro WT_calleeI)(auto simp add: rf.random_oracle_def[abs_def] finite_A nonempty_A ran_def split: option.split_asm)
have [simp]: "callee_invariant_on rf.random_oracle ?I1 ℐ"
by(unfold_locales)(auto simp add: rf.random_oracle_def finite_A split: option.split_asm)
then interpret rf: callee_invariant_on rf.random_oracle ?I1 ℐ .
have [simp]: "ℐ ⊢c rp_bad s2 √ " if "ran (snd s2) ⊆ A" for s2 using that
by(intro WT_calleeI)(auto simp add: rp_bad_def finite_A split: prod.split_asm option.split_asm if_split_asm intro: ranI)
have [simp]: "callee_invariant_on rf.random_oracle (λσ1. ?bad1 σ1 ∧ ?I1 σ1) ℐ"
by(unfold_locales)(clarsimp simp add: rf.random_oracle_def finite_A  split: option.split_asm)+
have [simp]: "callee_invariant_on rp_bad (λs2. ?I2 s2) ℐ"
by(unfold_locales)(auto 4 3 simp add: rp_bad_simps finite_A split: option.splits if_split_asm iff del: domIff)
by(unfold_locales)(auto 4 3 simp add: rp_bad_simps finite_A split: option.splits if_split_asm iff del: domIff)
have [simp]: "ℐ ⊢c rp_bad (bad, σ2) √" if "ran σ2 ⊆ A" for bad σ2 using that
have [simp]: "lossless_spmf (rp_bad (b, σ2) x)" if "x ∈ A" "dom σ2 ⊆ A" "ran σ2 ⊆ A" for b σ2 x
by(clarsimp simp add: nonempty_A dom_subset_ran_iff eq_None_iff_not_dom split: option.split)
have "rel_spmf (λ(b1, σ1) (b2, state2). (?bad1 σ1 ⟷ ?bad2 state2) ∧ (if ?bad2 state2 then ?X_bad σ1 state2 else b1 = b2 ∧ ?X σ1 state2))
((if False then rp.random_permutation else rf.random_oracle) s1 x) (rp_bad s2 x)"
if "?X s1 s2" "x ∈ outs_ℐ ℐ" "?I1 s1" "?I2 s2" for s1 s2 x using that finite_A
by(auto split!: option.split simp add: rf.random_oracle_def rp_bad_def rel_spmf_return_spmf1 collision_map_updI dom_subset_ran_iff eq_None_iff_not_dom collision_map_upd_iff intro!: rel_spmf_bind_reflI)
with _ _ have "rel_spmf
(λ(b1, σ1) (b2, state2). (?bad1 σ1 ⟷ ?bad2 state2) ∧ (if ?bad2 state2 then ?X_bad σ1 state2 else b1 = b2 ∧ ?X σ1 state2))
(?run False) (exec_gpv rp_bad 𝒜 init)"
by(rule exec_gpv_oracle_bisim_bad_invariant[where ℐ = ℐ and ?I1.0 = "?I1" and ?I2.0="?I2"])(auto simp add: init_def WT lossless finite_A nonempty_A)
then have "¦spmf (map_spmf fst (?run False)) True - spmf (run_gpv rp_bad 𝒜 init) True¦ ≤ spmf (map_spmf (?bad1 ∘ snd) (?run False)) True"
unfolding spmf_conv_measure_spmf measure_map_spmf vimage_def
also have "ennreal … ≤ ennreal (q / card A) * (enat q)" unfolding if_False using bound _ _ _ _ _ _ _ WT
by(rule rf.interaction_bounded_by_exec_gpv_bad_count[where count="λs. card (dom s)"])
(auto simp add: rf.random_oracle_def finite_A nonempty_A card_insert_if finite_subset[OF _ finite_A] map_spmf_conv_bind_spmf[symmetric] spmf.map_comp o_def collision_map_upd_iff map_mem_spmf_of_set card_gt_0_iff card_mono field_simps Int_absorb2 intro: card_ran_le_dom[OF finite_subset, OF _ finite_A, THEN order_trans] split: option.splits)
hence "spmf (map_spmf (?bad1 ∘ snd) (?run False)) True ≤ q * q / card A"
finally have "¦spmf (run_gpv rp_bad 𝒜 init) True - spmf (run_gpv rf.random_oracle 𝒜 Map.empty) True¦ ≤ q * q / card A"
by simp }
qed

end

end


# Theory PRF_UHF

(* Title: PRF_UHF.thy
Author: Bhargav Bhatt, ETH Zurich
Author: Andreas Lochbihler, ETH Zurich *)

subsection ‹Extending the input length of a PRF using a universal hash function›

text ‹ This example is taken from \cite[\S 4.2]{Shoup2004IACR}.›

theory PRF_UHF imports
CryptHOL.GPV_Bisim
Pseudo_Random_Function
begin

locale "hash" =
fixes seed_gen :: "'seed spmf"
and "hash" :: "'seed ⇒ 'domain ⇒ 'range"
begin

definition game_hash :: " 'domain ⇒ 'domain ⇒ bool spmf"
where
"game_hash w w' = do {
seed ← seed_gen;
return_spmf (hash seed w = hash seed w' ∧ w ≠ w')
}"

definition game_hash_set :: "'domain set ⇒ bool spmf"
where
"game_hash_set W = do {
seed  ← seed_gen;
return_spmf (¬ inj_on (hash seed) W)
}"

definition ε_uh :: "real"
where "ε_uh  = (SUP w w'. spmf (game_hash w w') True)"

lemma ε_uh_nonneg : "ε_uh ≥ 0"
by(auto 4 3 intro!: cSUP_upper2 bdd_aboveI2[where M=1] cSUP_least pmf_le_1 pmf_nonneg simp add: ε_uh_def)

lemma hash_ineq_card:
assumes "finite W"
shows "spmf (game_hash_set W) True ≤ ε_uh * card W * card W"
proof -
let ?M = "measure (measure_spmf seed_gen)"
have bound: "?M {x. hash x w = hash x w' ∧ w ≠ w'} ≤ ε_uh" for w w'
proof -
have "?M {x. hash x w = hash x w' ∧ w ≠ w'} = spmf (game_hash w w') True"
by(simp add: game_hash_def spmf_conv_measure_spmf map_spmf_conv_bind_spmf[symmetric] measure_map_spmf vimage_def)
also have "… ≤ ε_uh" unfolding ε_uh_def
by(auto intro!: cSUP_upper2 bdd_aboveI[where M=1] cSUP_least simp add: pmf_le_1)
finally show ?thesis .
qed

have "spmf (game_hash_set W) True = ?M {x. ∃xa∈W. ∃y∈W. hash x xa = hash x y ∧ xa ≠ y}"
by(auto simp add: game_hash_set_def inj_on_def map_spmf_conv_bind_spmf[symmetric] spmf_conv_measure_spmf measure_map_spmf vimage_def)
also have "{x. ∃xa∈W. ∃y∈W. hash x xa = hash x y ∧ xa ≠ y} = (⋃(w, w') ∈ W× W. {x. hash x w = hash x w' ∧ w ≠ w'})"
by(auto)
also have "?M … ≤ (∑(w, w')∈W × W. ?M {x. hash x w = hash x w' ∧ w ≠ w'})"
also have "… ≤ (∑(w, w')∈W × W. ε_uh)" by(rule sum_mono)(clarsimp simp add: bound)
also have "… =  ε_uh * card(W) * card(W)" by(simp add: card_cartesian_product)
finally show ?thesis .
qed

end

locale prf_hash =
fixes f :: "'key ⇒ 'α ⇒ 'γ"
and h :: "'seed ⇒ 'β ⇒ 'α"
and key_gen :: "'key spmf"
and seed_gen :: "'seed spmf"
and range_f :: "'γ set"
assumes lossless_seed_gen: "lossless_spmf seed_gen"
and range_f_finite: "finite range_f"
and range_f_nonempty: "range_f ≠ {}"
begin

definition rand :: "'γ spmf"
where "rand = spmf_of_set range_f"

lemma lossless_rand [simp]: "lossless_spmf rand"

definition key_seed_gen :: "('key * 'seed) spmf"
where
"key_seed_gen = do {
k ← key_gen;
s :: 'seed ← seed_gen;
return_spmf (k, s)
}"

interpretation "prf": "prf" key_gen f rand .
interpretation hash: hash "seed_gen" "h".

fun f' :: "'key × 'seed ⇒ 'β ⇒ 'γ"
where "f' (key, seed) x = f key (h seed x)"

interpretation "prf'": "prf" key_seed_gen f' rand .

definition reduction_oracle :: "'seed ⇒ unit ⇒ 'β ⇒ ('γ × unit, 'α, 'γ) gpv"
where "reduction_oracle seed x b = Pause (h seed b) (λx. Done (x, ()))"

where
"prf'_reduction 𝒜 = do {
seed  ← lift_spmf seed_gen;
(b, σ) ← inline (reduction_oracle seed) 𝒜 ();
Done b
}"

assumes "prf'.lossless 𝒜"
and bounded: "prf'.ibounded_by 𝒜 q"
shows "prf'.advantage 𝒜  ≤ prf.advantage (prf'_reduction 𝒜) + hash.ε_uh * q * q"
including lifting_syntax
proof -
let ?𝒜 = "prf'_reduction 𝒜"

{ define cr where "cr = (λ_ :: unit × unit. λ_ :: unit. True)"
have [transfer_rule]: "cr ((), ()) ()" by(simp add: cr_def)
have "prf.game_0 ?𝒜 = prf'.game_0 𝒜"
unfolding prf'.game_0_def prf.game_0_def prf'_reduction_def unfolding key_seed_gen_def
by(simp add: exec_gpv_bind split_def exec_gpv_inline reduction_oracle_def bind_map_spmf prf.prf_oracle_def prf'.prf_oracle_def[abs_def])
(transfer_prover) }
note hop1 = this[symmetric]

define semi_forgetful_RO where "semi_forgetful_RO = (λseed :: 'seed. λ(σ :: 'α ⇀ 'β × 'γ, b :: bool). λx.
case σ (h seed x) of Some (a, y) ⇒ return_spmf (y, (σ, a ≠ x ∨ b))
| None ⇒ bind_spmf rand (λy. return_spmf (y, (σ(h seed x ↦ (x, y)), b))))"

define game_semi_forgetful where "game_semi_forgetful = do {
seed :: 'seed ← seed_gen;
(b, rep) ← exec_gpv (semi_forgetful_RO seed) 𝒜 (Map.empty, False);
return_spmf (b, rep)
}"

have bad_semi_forgetful [simp]: "callee_invariant (semi_forgetful_RO seed) snd" for seed
by(unfold_locales)(auto simp add: semi_forgetful_RO_def split: option.split_asm)
have lossless_semi_forgetful [simp]: "lossless_spmf (semi_forgetful_RO seed s1 x)" for seed s1 x
by(simp add: semi_forgetful_RO_def split_def split: option.split)

{ define cr
where "cr = (λ(_ :: unit, σ) (σ' :: 'α ⇒ ('β × 'γ) option, _ :: bool). σ = map_option snd ∘ σ')"
define initial where "initial = (Map.empty :: 'α ⇒ ('β × 'γ) option, False)"
have [transfer_rule]: "cr ((), Map.empty) initial" by(simp add: cr_def initial_def fun_eq_iff)
have [transfer_rule]:  "((=) ===> cr ===> (=) ===> rel_spmf (rel_prod (=) cr))
(λy p ya. do {y ← prf.random_oracle (snd p) (h y ya); return_spmf (fst y, (), snd y) })
semi_forgetful_RO"
by(auto simp add: semi_forgetful_RO_def cr_def prf.random_oracle_def rel_fun_def fun_eq_iff split: option.split intro!: rel_spmf_bind_reflI)
have "prf.game_1 ?𝒜 = map_spmf fst game_semi_forgetful"
unfolding prf.game_1_def prf'_reduction_def game_semi_forgetful_def
by(simp add: exec_gpv_bind exec_gpv_inline split_def bind_map_spmf map_spmf_bind_spmf o_def map_spmf_conv_bind_spmf reduction_oracle_def initial_def[symmetric])
(transfer_prover) }
note hop2 = this

seed :: 'seed ← seed_gen;
x ← exec_gpv (semi_forgetful_RO seed) 𝒜 (Map.empty, False);
return_spmf (snd x)
}"

have bad_random_oracle_A [simp]: "callee_invariant prf.random_oracle (λσ. ¬ inj_on (h seed) (dom σ))" for seed
by unfold_locales(auto simp add: prf.random_oracle_def split: option.split_asm)

define invar
where "invar = (λseed (σ1, b) (σ2 :: 'β ⇒ 'γ option). ¬ b ∧ dom σ1 = h seed  dom σ2 ∧
(∀x ∈ dom σ2. σ1 (h seed x) = map_option (Pair x) (σ2 x)))"

"rel_spmf (λ(x, s1) (y, s2). snd s1 ≠ inj_on (h seed) (dom s2) ∧ (inj_on (h seed) (dom s2) ⟶ x = y ∧ invar seed s1 s2))
(exec_gpv (semi_forgetful_RO seed) 𝒜 (Map.empty, False))
(exec_gpv prf.random_oracle 𝒜 Map.empty)"
if seed: "seed ∈ set_spmf seed_gen" for seed
proof -
have invar_initial [simp]: "invar seed (Map.empty, False) Map.empty" by(simp add: invar_def)
have invarD_inj: "inj_on (h seed) (dom s2)" if "invar seed bs1 s2" for bs1 s2
using that by(auto intro!: inj_onI simp add: invar_def)(metis domI domIff option.map_sel prod.inject)

let ?R = "λ(a, s1) (b, s2 :: 'β ⇒ 'γ option).
snd s1 = (¬ inj_on (h seed) (dom s2)) ∧
(¬ ¬ inj_on (h seed) (dom s2) ⟶ a = b ∧ invar seed s1 s2)"

have step: "rel_spmf ?R (semi_forgetful_RO seed σ1b x) (prf.random_oracle s2 x)"
if X: "invar seed σ1b s2" for s2 σ1b x
proof -
obtain σ1 b where [simp]: "σ1b = (σ1, b)" by(cases σ1b)
from X have not_b: "¬ b"
and dom: "dom σ1 = h seed  dom s2"
and eq: "∀x∈dom s2. σ1 (h seed x) = map_option (Pair x) (s2 x)"
from X have inj: "inj_on (h seed) (dom s2)" by(rule invarD_inj)

have not_in_image: "h seed x ∉ h seed  (dom s2 - {x})" if "σ1 (h seed x) = None"
proof (rule notI)
assume "h seed x ∈ h seed  (dom s2 - {x})"
then obtain y where "y ∈ dom s2" and hx_hy: "h seed x = h seed y" by (auto)
then have "σ1 (h seed y) = None" using that by (auto)
then have "h seed y ∉ h seed  dom s2" using dom by (auto)
then have "y ∉ dom s2" by (auto)
then show False using ‹y ∈ dom s2› by(auto)
qed

show ?thesis
proof(cases "σ1 (h seed x)")
case σ1: None
hence s2: "s2 x = None" using dom by(auto)
have "insert (h seed x) (dom σ1) = insert (h seed x) (h seed  dom s2)" by(simp add: dom)
then have invar_update: "invar seed (σ1(h seed x ↦ (x, bs)), False) (s2(x ↦ bs))" for bs
using inj not_b not_in_image σ1 dom
by(auto simp add: invar_def domIff eq) (metis domI domIff imageI)
with σ1 s2 show ?thesis using inj not_b not_in_image
by(auto simp add: semi_forgetful_RO_def prf.random_oracle_def intro: rel_spmf_bind_reflI)
next
case σ1: (Some "by")
show ?thesis
proof(cases "s2 x")
case s2: (Some z)
with eq σ1 have "by = (x, z)" by(auto simp add: domIff)
thus ?thesis using σ1 inj not_b s2 X
next
case s2: None
from σ1 dom obtain y where y: "y ∈ dom s2" and *: "h seed x = h seed y"
by(metis domIff imageE option.distinct(1))
from y obtain z where z: "s2 y = Some z" by auto
from eq z σ1 have "by": "by = (y, z)" by(auto simp add: * domIff)
from y s2 have xny: "x ≠ y" by auto
with y * have "h seed x ∈ h seed  (dom s2 - {x})" by auto
then show ?thesis using σ1 s2 not_b "by" xny inj
by(simp add: semi_forgetful_RO_def prf.random_oracle_def split_beta)(rule rel_spmf_bindI2; simp)
qed
qed
qed
from invar_initial _ step show ?thesis
qed

define game_A where "game_A = do {
seed :: 'seed ← seed_gen;
(b, σ) ← exec_gpv prf.random_oracle 𝒜 Map.empty;
return_spmf (b, ¬ inj_on (h seed) (dom σ))
}"

have hop3: "rel_spmf (λx xa. (?bad1 x ⟷ ?bad2 xa) ∧ (¬ ?bad2 xa ⟶ fst x ⟷ fst xa)) game_semi_forgetful game_A"
unfolding game_semi_forgetful_def game_A_def
by(clarsimp simp add: restrict_bind_spmf split_def map_spmf_bind_spmf restrict_return_spmf o_def intro!: rel_spmf_bind_reflI simp del: bind_return_spmf)
have bad1_bad2: "spmf (map_spmf (snd ∘ snd) game_semi_forgetful) True = spmf (map_spmf snd game_A) True"
have bound_bad1_event: "¦spmf (map_spmf fst game_semi_forgetful) True - spmf (map_spmf fst game_A) True¦ ≤ spmf (map_spmf (snd ∘ snd) game_semi_forgetful) True"
using fundamental_lemma[OF hop3] by(simp add: measure_map_spmf spmf_conv_measure_spmf vimage_def)

then have bound_bad2_event : "¦spmf (map_spmf fst game_semi_forgetful) True - spmf (map_spmf fst game_A) True¦ ≤ spmf (map_spmf snd game_A) True"

define game_B where "game_B = do {
(b, σ) ← exec_gpv prf.random_oracle 𝒜 Map.empty;
hash.game_hash_set (dom σ)
}"

have game_A_game_B: "map_spmf snd game_A = game_B"
unfolding game_B_def game_A_def hash.game_hash_set_def including monad_normalisation

have game_B_bound : "spmf game_B True ≤ hash.ε_uh * q * q" unfolding game_B_def
proof(rule spmf_bind_leI, clarify)
fix b σ
assume *: "(b, σ) ∈ set_spmf (exec_gpv prf.random_oracle 𝒜 Map.empty)"
have "finite (dom σ)" by(rule prf.finite.exec_gpv_invariant[OF *]) simp_all
then have "spmf (hash.game_hash_set (dom σ)) True ≤ hash.ε_uh * (card (dom σ) * card (dom σ))"
using hash.hash_ineq_card[of "dom σ"] by simp
also have p1: "card (dom σ) ≤ q + card (dom (Map.empty :: 'β ⇒ 'γ option))"
by(rule prf.card_dom_random_oracle[OF bounded *]) simp
then have "card (dom σ) * card (dom σ) ≤ q * q" using mult_le_mono by auto
finally show "spmf (hash.game_hash_set (dom σ)) True ≤ hash.ε_uh * q * q"

have hop4: "prf'.game_1 𝒜 = map_spmf fst game_A"
by(simp add: game_A_def prf'.game_1_def map_spmf_bind_spmf o_def split_def bind_spmf_const lossless_seed_gen lossless_weight_spmfD)

have "prf'.advantage 𝒜 ≤ ¦spmf (prf.game_0 ?𝒜) True - spmf (prf'.game_1 𝒜) True¦"
also have "… ≤ prf.advantage ?𝒜 + ¦spmf (prf.game_1 ?𝒜) True - spmf (prf'.game_1 𝒜) True¦"
also have "¦spmf (prf.game_1 ?𝒜) True - spmf (prf'.game_1 𝒜) True¦ ≤
¦spmf (map_spmf fst game_semi_forgetful) True - spmf (prf'.game_1 𝒜) True¦"
using hop2 by simp
also have "… ≤ hash.ε_uh * q * q"
using game_A_game_B game_B_bound bound_bad2_event hop4 by(simp)
qed

end

end


# 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));
}"

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)"

where
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));
let c = (r, xor_list pb pad);
(b', _) ← inline prf_encrypt_oracle (𝒜2 c σ) n;
Done (b' = b)
} else lift_spmf coin_spmf
}"

assumes "ind_cpa.ibounded_by 𝒜 q"
and "lossless_gpv ℐ_full (fst 𝒜)"
and "⋀cipher σ. lossless_gpv ℐ_full (snd 𝒜 cipher σ)"
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"
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(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)"

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"
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;
} 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));
} 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
}"
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"

r ← spmf_of_set (nlists UNIV len);
(((p0, p1), σ), s1) ← exec_gpv rf_encrypt 𝒜1 Map.empty;
return_spmf (r ∈ dom s1)
}"
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)"
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)"
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

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').
have lossless_rf_encrypt [simp]: "⋀challenge s plain. lossless_spmf (rf_encrypt_bad challenge s plain)"

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);
} 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'"])

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);
} else coin_spmf ⤜ (λb. return_spmf (b, False))
}"

{ fix cipher σ and x :: plain and s r
have "⋀s1 s2 x'. ?X s1 s2 ⟹ rel_spmf (λ(a, s1') (b, s2'). snd s1' = snd s2' ∧ (¬ snd s2' ⟶ a = b ∧ ?X s1' s2'))
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))"
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)
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"
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¦"
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¦"
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);
(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);
(b', _) ← exec_gpv rf_encrypt (𝒜2 cipher σ) s1;
map_spmf ((=) b') coin_spmf
} else coin_spmf
}"
also have "… = coin_spmf"
by(simp add: map_eq_const_coin_spmf Let_def split_def weight2 weight1)
finally have game3: "game3 = coin_spmf" .

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

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"
show "prf.ibounded_by (prf_adversary 𝒜) (1 + q)" using q
apply (simp only: prf_adversary_def Let_def split_def)
apply -
apply interaction_bound
done
qed

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:
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 σ)"
ultimately have "ind_cpa.advantage η (𝒜 η) ≤ prf.advantage η (prf_adversary η (𝒜 η)) + q η / 2 ^ len η"
hence "eventually (λη. ¦ind_cpa.advantage η (𝒜 η)¦ ≤ 1 * ¦prf.advantage η (prf_adversary η (𝒜 η)) + q η / 2 ^ len η¦) at_top"
then show "(λη. ind_cpa.advantage η (𝒜 η)) ∈ O(λη. prf.advantage η (prf_adversary η (𝒜 η)) + q η / 2 ^ len η)"
by(intro bigoI[where c=1]) simp
qed

end

end


# Theory PRF_UPF_IND_CCA

(* Title: PRF_UPF_IND_CCA.thy
Author: Andreas Lochbihler, ETH Zurich
Author: S. Reza Sefidgar, ETH Zurich *)

subsection ‹IND-CCA from a PRF and an unpredictable function›

theory PRF_UPF_IND_CCA
imports
Pseudo_Random_Function
CryptHOL.List_Bits
Unpredictable_Function
IND_CCA2_sym
CryptHOL.Negligible
begin

text ‹Formalisation of Shoup's construction of an IND-CCA secure cipher from a PRF and an unpredictable function \cite[\S 7]{Shoup2004IACR}.›

type_synonym bitstring = "bool list"

locale simple_cipher =
PRF: "prf" prf_key_gen prf_fun "spmf_of_set (nlists UNIV prf_clen)" +
UPF: upf upf_key_gen upf_fun
for prf_key_gen :: "'prf_key spmf"
and prf_fun :: "'prf_key ⇒ bitstring ⇒ bitstring"
and prf_domain :: "bitstring set"
and prf_range :: "bitstring set"
and prf_dlen :: nat
and prf_clen :: nat
and upf_key_gen :: "'upf_key spmf"
and upf_fun :: "'upf_key ⇒ bitstring ⇒ 'hash"
+
assumes prf_domain_finite: "finite prf_domain"
assumes prf_domain_nonempty: "prf_domain ≠ {}"
assumes prf_domain_length:  "x ∈ prf_domain ⟹ length x = prf_dlen"
assumes prf_codomain_length:
"⟦ key_prf ∈ set_spmf prf_key_gen; m ∈ prf_domain ⟧ ⟹ length (prf_fun key_prf m) = prf_clen"
assumes prf_key_gen_lossless: "lossless_spmf prf_key_gen"
assumes upf_key_gen_lossless: "lossless_spmf upf_key_gen"
begin

type_synonym 'hash' cipher_text = "bitstring × bitstring × 'hash'"

definition key_gen :: "('prf_key × 'upf_key) spmf" where
"key_gen = do {
k_prf ← prf_key_gen;
k_upf :: 'upf_key ← upf_key_gen;
return_spmf (k_prf, k_upf)
}"

lemma lossless_key_gen [simp]: "lossless_spmf key_gen"

fun encrypt :: "('prf_key × 'upf_key) ⇒ bitstring ⇒ 'hash cipher_text spmf"
where
"encrypt (k_prf, k_upf) m = do {
x ← spmf_of_set prf_domain;
let c = prf_fun k_prf x [⊕] m;
let t = upf_fun k_upf (x @ c);
return_spmf ((x, c, t))
}"

lemma lossless_encrypt [simp]: "lossless_spmf (encrypt k m)"
by (cases k) (simp add: Let_def prf_domain_nonempty prf_domain_finite split: bool.split)

fun decrypt :: "('prf_key × 'upf_key) ⇒ 'hash cipher_text ⇒ bitstring option"
where
"decrypt (k_prf, k_upf) (x, c, t) = (
if upf_fun k_upf (x @ c) = t ∧ length x = prf_dlen then
Some (prf_fun k_prf x [⊕] c)
else
None
)"

lemma cipher_correct:
"⟦ k ∈ set_spmf key_gen; length m = prf_clen ⟧
⟹ encrypt k m ⤜ (λc. return_spmf (decrypt k c)) = return_spmf (Some m)"
by (cases k) (simp add: prf_domain_nonempty prf_domain_finite prf_domain_length
prf_codomain_length key_gen_def bind_eq_return_spmf Let_def)

declare encrypt.simps[simp del]

sublocale ind_cca: ind_cca key_gen encrypt decrypt "λm. length m = prf_clen" .
interpretation ind_cca': ind_cca key_gen encrypt "λ _ _. None" "λm. length m = prf_clen" .

definition intercept_upf_enc
:: "'prf_key ⇒ bool ⇒ 'hash cipher_text set × 'hash cipher_text set ⇒ bitstring × bitstring
⇒ ('hash cipher_text option × ('hash cipher_text set × 'hash cipher_text set),
bitstring + (bitstring × 'hash), 'hash + unit) gpv"
where
"intercept_upf_enc k b = (λ(L, D) (m1, m0).
(case (length m1 = prf_clen ∧ length m0 = prf_clen) of
False ⇒ Done (None, L, D)
| True ⇒ do {
x ← lift_spmf (spmf_of_set prf_domain);
let c = prf_fun k x [⊕] (if b then m1 else m0);
t ← Pause (Inl (x @ c)) Done;
Done ((Some (x, c, projl t)), (insert (x, c, projl t) L, D))
}))"

definition intercept_upf_dec
:: "'hash cipher_text set × 'hash cipher_text set ⇒ 'hash cipher_text
⇒ (bitstring option × ('hash cipher_text set × 'hash cipher_text set),
bitstring + (bitstring × 'hash), 'hash + unit) gpv"
where
"intercept_upf_dec = (λ(L, D) (x, c, t).
if (x, c, t) ∈ L ∨ length x ≠ prf_dlen then Done (None, (L, D)) else do {
Pause (Inr (x @ c, t)) Done;
Done (None, (L, insert (x, c, t) D))
})"

definition intercept_upf ::
"'prf_key ⇒ bool ⇒ 'hash cipher_text set × 'hash cipher_text set ⇒ bitstring × bitstring + 'hash cipher_text
⇒ (('hash cipher_text option + bitstring option) × ('hash cipher_text set × 'hash cipher_text set),
bitstring + (bitstring × 'hash), 'hash + unit) gpv"
where
"intercept_upf k b = plus_intercept (intercept_upf_enc k b) intercept_upf_dec"

lemma intercept_upf_simps [simp]:
"intercept_upf k b (L, D) (Inr (x, c, t)) =
(if (x, c, t) ∈ L ∨ length x ≠ prf_dlen then Done (Inr None, (L, D)) else do {
Pause (Inr (x @ c, t)) Done;
Done (Inr None, (L, insert (x, c, t) D))
})"
"intercept_upf k b (L, D) (Inl (m1, m0)) =
(case (length m1 = prf_clen ∧ length m0 = prf_clen) of
False ⇒ Done (Inl None, L, D)
| True ⇒ do {
x ← lift_spmf (spmf_of_set prf_domain);
let c = prf_fun k x [⊕] (if b then m1 else m0);
t ← Pause (Inl (x @ c)) Done;
Done (Inl (Some (x, c, projl t)), (insert (x, c, projl t) L, D))
})"
by(simp_all add: intercept_upf_def intercept_upf_dec_def intercept_upf_enc_def o_def map_gpv_bind_gpv gpv.map_id Let_def split!: bool.split)

lemma interaction_bounded_by_upf_enc_Inr [interaction_bound]:
"interaction_bounded_by (Not ∘ isl) (intercept_upf_enc k b LD mm) 0"
unfolding intercept_upf_enc_def case_prod_app
by(interaction_bound, clarsimp simp add: SUP_constant bot_enat_def split: prod.split)

lemma interaction_bounded_by_upf_dec_Inr [interaction_bound]:
"interaction_bounded_by (Not ∘ isl) (intercept_upf_dec LD c) 1"
unfolding intercept_upf_dec_def case_prod_app
by(interaction_bound, clarsimp simp add: SUP_constant split: prod.split)

lemma interaction_bounded_by_intercept_upf_Inr [interaction_bound]:
"interaction_bounded_by (Not ∘ isl) (intercept_upf k b LD x) 1"
unfolding intercept_upf_def
by interaction_bound(simp add: split_def one_enat_def SUP_le_iff split: sum.split)

lemma interaction_bounded_by_intercept_upf_Inl [interaction_bound]:
"isl x ⟹ interaction_bounded_by (Not ∘ isl) (intercept_upf k b LD x) 0"
unfolding intercept_upf_def case_prod_app
by interaction_bound(auto split: sum.split)

lemma lossless_intercept_upf_enc [simp]: "lossless_gpv (ℐ_full ⊕⇩ℐ ℐ_full) (intercept_upf_enc k b LD mm)"
by(simp add: intercept_upf_enc_def split_beta prf_domain_finite prf_domain_nonempty Let_def split: bool.split)

lemma lossless_intercept_upf_dec [simp]: "lossless_gpv (ℐ_full ⊕⇩ℐ ℐ_full) (intercept_upf_dec LD mm)"

lemma lossless_intercept_upf [simp]: "lossless_gpv (ℐ_full ⊕⇩ℐ ℐ_full) (intercept_upf k b LD x)"

lemma results_gpv_intercept_upf [simp]: "results_gpv (ℐ_full ⊕⇩ℐ ℐ_full) (intercept_upf k b LD x) ⊆ responses_ℐ (ℐ_full ⊕⇩ℐ ℐ_full) x × UNIV"

definition reduction_upf :: "(bitstring, 'hash cipher_text) ind_cca.adversary
where "reduction_upf 𝒜 = do {
k ← lift_spmf prf_key_gen;
b ← lift_spmf coin_spmf;
(_, (L, D)) ← inline (intercept_upf k b) 𝒜 ({}, {});
Done () }"

lemma lossless_reduction_upf [simp]:
"lossless_gpv (ℐ_full ⊕⇩ℐ ℐ_full) 𝒜 ⟹ lossless_gpv (ℐ_full ⊕⇩ℐ ℐ_full) (reduction_upf 𝒜)"
by(auto simp add: reduction_upf_def prf_key_gen_lossless intro: lossless_inline del: subsetI)

context includes lifting_syntax begin

lemma round_1:
assumes "lossless_gpv (ℐ_full ⊕⇩ℐ ℐ_full) 𝒜"
shows "¦spmf (ind_cca.game 𝒜) True - spmf (ind_cca'.game 𝒜) True¦ ≤ UPF.advantage (reduction_upf 𝒜)"
proof -
define oracle_decrypt0' where "oracle_decrypt0' ≡ (λkey (bad, L) (x', c', t'). return_spmf (
if (x', c', t') ∈ L ∨ length x' ≠ prf_dlen then (None, (bad, L))
else (decrypt key (x', c', t'), (bad ∨ upf_fun (snd key) (x' @ c') = t', L))))"
have oracle_decrypt0'_simps:
"oracle_decrypt0' key (bad, L) (x', c', t') = return_spmf (
if (x', c', t') ∈ L ∨ length x' ≠ prf_dlen then (None, (bad, L))
else (decrypt key (x', c', t'), (bad ∨ upf_fun (snd key) (x' @ c') = t', L)))"
have lossless_oracle_decrypt0' [simp]: "lossless_spmf (oracle_decrypt0' k Lbad c)" for k Lbad c
have callee_invariant_oracle_decrypt0' [simp]: "callee_invariant (oracle_decrypt0' k) fst" for k
by (unfold_locales) (auto simp add: oracle_decrypt0'_def split: if_split_asm)

define oracle_decrypt1'
where "oracle_decrypt1' = (λ(key :: 'prf_key × 'upf_key) (bad, L) (x', c', t').
return_spmf (None :: bitstring option,
(bad ∨ upf_fun (snd key) (x' @ c') = t' ∧ (x', c', t') ∉ L ∧ length x' = prf_dlen), L))"
have oracle_decrypt1'_simps:
"oracle_decrypt1' key (bad, L) (x', c', t') =
return_spmf (None,
(bad ∨ upf_fun (snd key) (x' @ c') = t' ∧ (x', c', t') ∉ L ∧ length x' = prf_dlen, L))"
have lossless_oracle_decrypt1' [simp]: "lossless_spmf (oracle_decrypt1' k Lbad c)" for k Lbad c
have callee_invariant_oracle_decrypt1' [simp]: "callee_invariant (oracle_decrypt1' k) fst" for k
by (unfold_locales) (auto simp add: oracle_decrypt1'_def)

define game01'
where "game01' = (λ(decrypt :: 'prf_key × 'upf_key ⇒ (bitstring × bitstring × 'hash, bitstring option, bool × (bitstring × bitstring × 'hash) set) callee) 𝒜. do {
key ← key_gen;
b ← coin_spmf;
(b', (bad', L')) ← exec_gpv (†(ind_cca.oracle_encrypt key b) ⊕⇩O decrypt key) 𝒜 (False, {});
return_spmf (b = b', bad') })"
let ?game0' = "game01' oracle_decrypt0'"
let ?game1' = "game01' oracle_decrypt1'"

have game0'_eq: "ind_cca.game 𝒜 = map_spmf fst (?game0' 𝒜)" (is ?game0)
and game1'_eq: "ind_cca'.game 𝒜 = map_spmf fst (?game1' 𝒜)" (is ?game1)
proof -
let ?S = "rel_prod2 (=)"
define initial where "initial = (False, {} :: 'hash cipher_text set)"
have [transfer_rule]: "?S {} initial" by(simp add: initial_def)

have [transfer_rule]:
"((=) ===> ?S ===> (=) ===> rel_spmf (rel_prod (=) ?S))
ind_cca.oracle_decrypt oracle_decrypt0'"
unfolding ind_cca.oracle_decrypt_def[abs_def] oracle_decrypt0'_def[abs_def]

have [transfer_rule]:
"((=) ===> ?S ===> (=) ===> rel_spmf (rel_prod (=) ?S))
ind_cca'.oracle_decrypt oracle_decrypt1'"
unfolding ind_cca'.oracle_decrypt_def[abs_def] oracle_decrypt1'_def[abs_def]

note [transfer_rule] = extend_state_oracle_transfer
show ?game0 ?game1 unfolding game01'_def ind_cca.game_def ind_cca'.game_def initial_def[symmetric]
by (simp_all add: map_spmf_bind_spmf o_def split_def) transfer_prover+
qed

(exec_gpv (†(ind_cca.oracle_encrypt k b) ⊕⇩O oracle_decrypt1' k) 𝒜 (False, {}))
(exec_gpv (†(ind_cca.oracle_encrypt k b) ⊕⇩O oracle_decrypt0' k) 𝒜 (False, {}))"
for k b
(auto intro: rel_spmf_reflI callee_invariant_extend_state_oracle_const' simp add: spmf_rel_map1 spmf_rel_map2 oracle_decrypt0'_simps oracle_decrypt1'_simps assms split: plus_oracle_split)
― ‹We cannot get rid of the losslessness assumption on @{term 𝒜} in this step, because if it
were not, then the bad event might still occur, but the adversary does not terminate in
the case of @{term "?game1'"}. Thus, the reduction does not terminate either, but it cannot
detect whether the bad event has happened. So the advantage in the UPF game could be lower than
the probability of the bad event, if the adversary is not lossless.›
have "¦measure (measure_spmf (?game1' 𝒜)) {(b, bad). b} - measure (measure_spmf (?game0' 𝒜)) {(b, bad). b}¦
also have "… = spmf (map_spmf snd (?game1' 𝒜)) True"
by (simp add: spmf_conv_measure_spmf measure_map_spmf split_def vimage_def)
also have "map_spmf snd (?game1' 𝒜) = UPF.game (reduction_upf 𝒜)"
proof -
note [split del] = if_split
have "map_spmf (λx. fst (snd x)) (exec_gpv (†(ind_cca.oracle_encrypt (k_prf, k_upf) b) ⊕⇩O oracle_decrypt1' (k_prf, k_upf)) 𝒜 (False, {})) =
map_spmf (λx. fst (snd x)) (exec_gpv (UPF.oracle k_upf) (inline (intercept_upf k_prf b) 𝒜 ({}, {})) (False, {}))"
(is "map_spmf ?fl ?lhs = map_spmf ?fr ?rhs" is "map_spmf _ (exec_gpv ?oracle_normal _ ?init_normal) = _")
for k_prf k_upf b
proof(rule map_spmf_eq_map_spmfI)
define oracle_intercept
where [simp]: "oracle_intercept = (λ(s', s) y. map_spmf (λ((x, s'), s). (x, s', s))
(exec_gpv (UPF.oracle k_upf) (intercept_upf k_prf b s' y) s))"
let ?I = "(λ((L, D), (flg, Li)).
(∀(x, c, t) ∈ L. upf_fun k_upf (x @ c) = t ∧ length x = prf_dlen) ∧
(∀e∈Li. ∃(x,c,_) ∈ L. e = x @ c) ∧
((∃(x, c, t) ∈ D. upf_fun k_upf (x @ c) = t) ⟷ flg))"
interpret callee_invariant_on oracle_intercept "?I" ℐ_full
apply(unfold_locales)
subgoal for s x y s'
apply(cases s; cases s'; cases x)
UPF.oracle_hash_def prf_domain_length exec_gpv_bind Let_def split: bool.splits)
apply(force simp add: exec_gpv_bind UPF.oracle_flag_def split: if_split_asm)
done
subgoal by simp
done

define S :: "bool × 'hash cipher_text set ⇒ ('hash cipher_text set × 'hash cipher_text set) ×  bool × bitstring set ⇒ bool"
where "S = (λ(bad, L1) ((L2, D), _). bad = (∃(x, c, t)∈D. upf_fun k_upf (x @ c) = t) ∧ L1 = L2) ↿ (λ_. True) ⊗ ?I"
define initial :: "('hash cipher_text set × 'hash cipher_text set) ×  bool × bitstring set"
where "initial = (({}, {}), (False, {}))"
have [transfer_rule]: "S ?init_normal initial" by(simp add: S_def initial_def)
have [transfer_rule]: "(S ===> (=) ===> rel_spmf (rel_prod (=) S)) ?oracle_normal oracle_intercept"
unfolding S_def
by(rule callee_invariant_restrict_relp, unfold_locales)
(auto simp add: rel_fun_def bind_spmf_of_set prf_domain_finite prf_domain_nonempty bind_spmf_pmf_assoc bind_assoc_pmf bind_return_pmf spmf_rel_map exec_gpv_bind Let_def ind_cca.oracle_encrypt_def oracle_decrypt1'_def encrypt.simps UPF.oracle_hash_def UPF.oracle_flag_def bind_map_spmf o_def split: plus_oracle_split bool.split if_split intro!: rel_spmf_bind_reflI rel_pmf_bind_reflI)
have "rel_spmf (rel_prod (=) S) ?lhs (exec_gpv oracle_intercept 𝒜 initial)"
by(transfer_prover)
then show "rel_spmf (λx y. ?fl x = ?fr y) ?lhs ?rhs"
by(auto simp add: S_def exec_gpv_inline spmf_rel_map initial_def elim: rel_spmf_mono)
qed
by(auto simp add: reduction_upf_def UPF.game_def game01'_def key_gen_def map_spmf_conv_bind_spmf split_def exec_gpv_bind intro!: bind_spmf_cong[OF refl])
qed
finally show ?thesis using game0'_eq game1'_eq
qed

definition oracle_encrypt2 ::
"('prf_key × 'upf_key) ⇒ bool ⇒ (bitstring, bitstring) PRF.dict ⇒ bitstring × bitstring
⇒ ('hash cipher_text option × (bitstring, bitstring) PRF.dict) spmf"
where
"oracle_encrypt2 = (λ(k_prf, k_upf) b D (msg1, msg0). (case (length msg1 = prf_clen ∧ length msg0 = prf_clen) of
False ⇒ return_spmf (None, D)
| True ⇒ do {
x ← spmf_of_set prf_domain;
P ← spmf_of_set (nlists UNIV prf_clen);
let p = (case D x of Some r ⇒ r | None ⇒ P);
let c = p [⊕] (if b then msg1 else msg0);
let t = upf_fun k_upf (x @ c);
return_spmf (Some (x, c, t), D(x ↦ p))
}))"

definition oracle_decrypt2:: "('prf_key × 'upf_key) ⇒ ('hash cipher_text, bitstring option, 'state) callee"
where "oracle_decrypt2 = (λkey D cipher. return_spmf (None, D))"

lemma lossless_oracle_decrypt2 [simp]: "lossless_spmf (oracle_decrypt2 k Dbad c)"

lemma callee_invariant_oracle_decrypt2 [simp]: "callee_invariant (oracle_decrypt2 key) fst"
by (unfold_locales) (auto simp add: oracle_decrypt2_def split: if_split_asm)

lemma oracle_decrypt2_parametric [transfer_rule]:
"(rel_prod P U ===> S ===> rel_prod (=) (rel_prod (=) H) ===> rel_spmf (rel_prod (=) S))
oracle_decrypt2 oracle_decrypt2"
unfolding oracle_decrypt2_def split_def relator_eq[symmetric] by transfer_prover

definition game2 :: "(bitstring, 'hash cipher_text) ind_cca.adversary ⇒ bool spmf"
where
"game2 𝒜 ≡ do {
key ← key_gen;
b ← coin_spmf;
(b', D) ← exec_gpv
(oracle_encrypt2 key b ⊕⇩O oracle_decrypt2 key) 𝒜 Map_empty;
return_spmf (b = b')
}"

fun intercept_prf ::
"'upf_key ⇒ bool ⇒ unit ⇒ (bitstring × bitstring) + 'hash cipher_text
⇒ (('hash cipher_text option + bitstring option) × unit, bitstring, bitstring) gpv"
where
"intercept_prf _ _ _ (Inr _) = Done (Inr None, ())"
| "intercept_prf k b _ (Inl (m1, m0)) = (case (length m1) = prf_clen ∧ (length m0) = prf_clen of
False ⇒ Done (Inl None, ())
| True ⇒ do {
x ← lift_spmf (spmf_of_set prf_domain);
p ← Pause x Done;
let c = p [⊕] (if b then m1 else m0);
let t = upf_fun k (x @ c);
Done (Inl (Some (x, c, t)), ())
})"

definition reduction_prf
where
"reduction_prf 𝒜 = do {
k ← lift_spmf upf_key_gen;
b ← lift_spmf coin_spmf;
(b', _) ← inline (intercept_prf k b) 𝒜 ();
Done (b' = b)
}"

lemma round_2: "¦spmf (ind_cca'.game 𝒜) True - spmf (game2 𝒜) True¦ = PRF.advantage (reduction_prf 𝒜)"
proof -
define oracle_encrypt1''
where "oracle_encrypt1'' = (λ(k_prf, k_upf) b (_ :: unit) (msg1, msg0).
case length msg1 = prf_clen ∧ length msg0 = prf_clen of
False ⇒ return_spmf (None, ())
| True ⇒ do {
x ← spmf_of_set prf_domain;
let p = prf_fun k_prf x;
let c = p [⊕] (if b then msg1 else msg0);
let t = upf_fun k_upf (x @ c);
return_spmf (Some (x, c, t), ())})"
define game1'' where "game1'' = do {
key ← key_gen;
b ← coin_spmf;
(b', D) ← exec_gpv (oracle_encrypt1'' key b ⊕⇩O oracle_decrypt2 key) 𝒜 ();
return_spmf (b = b')}"

have "ind_cca'.game 𝒜 = game1''"
proof -
define S where "S = (λ(L :: 'hash cipher_text set) (D :: unit). True)"
have [transfer_rule]: "S {} ()" by (simp add: S_def)
have [transfer_rule]:
"((=) ===> (=) ===> S ===> (=) ===> rel_spmf (rel_prod (=) S))
ind_cca'.oracle_encrypt oracle_encrypt1''"
unfolding ind_cca'.oracle_encrypt_def[abs_def] oracle_encrypt1''_def[abs_def]
by (auto simp add: rel_fun_def Let_def S_def encrypt.simps prf_domain_finite prf_domain_nonempty intro: rel_spmf_bind_reflI rel_pmf_bind_reflI split: bool.split)
have [transfer_rule]:
"((=) ===> S ===> (=) ===> rel_spmf (rel_prod (=) S))
ind_cca'.oracle_decrypt oracle_decrypt2"
unfolding ind_cca'.oracle_decrypt_def[abs_def] oracle_decrypt2_def[abs_def]
show ?thesis unfolding ind_cca'.game_def game1''_def by transfer_prover
qed

also have "… = PRF.game_0 (reduction_prf 𝒜)"
proof -
{ fix k_prf k_upf b
define oracle_normal
where "oracle_normal = oracle_encrypt1'' (k_prf, k_upf) b ⊕⇩O oracle_decrypt2 (k_prf, k_upf)"
define oracle_intercept
where "oracle_intercept = (λ(s', s :: unit) y. map_spmf (λ((x, s'), s). (x, s', s)) (exec_gpv (PRF.prf_oracle k_prf) (intercept_prf k_upf b s' y) ()))"
define initial where "initial = ()"
define S where "S = (λ(s2 :: unit, _ :: unit) (s1 :: unit). True)"
have [transfer_rule]: "S ((), ()) initial" by(simp add: S_def initial_def)
have [transfer_rule]: "(S ===> (=) ===> rel_spmf (rel_prod (=) S)) oracle_intercept oracle_normal"
unfolding oracle_normal_def oracle_intercept_def
by(auto split: bool.split plus_oracle_split simp add: S_def rel_fun_def exec_gpv_bind PRF.prf_oracle_def oracle_encrypt1''_def Let_def map_spmf_conv_bind_spmf oracle_decrypt2_def intro!: rel_spmf_bind_reflI rel_spmf_reflI)
have "map_spmf (λx. b = fst x) (exec_gpv oracle_normal 𝒜 initial) =
map_spmf (λx. b = fst (fst x)) (exec_gpv (PRF.prf_oracle k_prf) (inline (intercept_prf k_upf b) 𝒜 ()) ())"
by(transfer fixing: b 𝒜 prf_fun k_prf prf_domain prf_clen upf_fun k_upf)
(auto simp add: map_spmf_eq_map_spmf_iff exec_gpv_inline spmf_rel_map oracle_intercept_def split_def intro: rel_spmf_reflI) }
then show ?thesis unfolding game1''_def PRF.game_0_def key_gen_def reduction_prf_def
by (auto simp add: exec_gpv_bind_lift_spmf exec_gpv_bind map_spmf_conv_bind_spmf split_def eq_commute intro!: bind_spmf_cong[OF refl])
qed
also have "game2 𝒜 = PRF.game_1 (reduction_prf 𝒜)"
proof -
note [split del] = if_split
{ fix k_upf b k_prf
define oracle2
where "oracle2 = oracle_encrypt2 (k_prf, k_upf) b ⊕⇩O oracle_decrypt2 (k_prf, k_upf)"
define oracle_intercept
where "oracle_intercept = (λ(s', s) y. map_spmf (λ((x, s'), s). (x, s', s)) (exec_gpv PRF.random_oracle (intercept_prf k_upf b s' y) s))"
define S
where "S = (λ(s2 :: unit, s2') (s1 :: (bitstring, bitstring) PRF.dict). s2' = s1)"

have [transfer_rule]: "S ((), Map_empty) Map_empty" by(simp add: S_def)
have [transfer_rule]: "(S ===> (=) ===> rel_spmf (rel_prod (=) S)) oracle_intercept oracle2"
unfolding oracle2_def oracle_intercept_def
by(auto split: bool.split plus_oracle_split option.split simp add: S_def rel_fun_def exec_gpv_bind PRF.random_oracle_def oracle_encrypt2_def Let_def map_spmf_conv_bind_spmf oracle_decrypt2_def rel_spmf_return_spmf1 fun_upd_idem intro!: rel_spmf_bind_reflI rel_spmf_reflI)

have [symmetric]: "map_spmf (λx. b = fst (fst x)) (exec_gpv (PRF.random_oracle) (inline (intercept_prf k_upf b) 𝒜 ()) Map.empty) =
map_spmf (λx. b = fst x) (exec_gpv oracle2 𝒜 Map_empty)"
by(transfer fixing: b prf_clen prf_domain upf_fun k_upf 𝒜 k_prf)
(simp add: exec_gpv_inline map_spmf_conv_bind_spmf[symmetric] spmf.map_comp o_def split_def oracle_intercept_def) }
then show ?thesis
unfolding game2_def PRF.game_1_def key_gen_def reduction_prf_def
by (clarsimp simp add: exec_gpv_bind_lift_spmf exec_gpv_bind map_spmf_conv_bind_spmf split_def bind_spmf_const prf_key_gen_lossless lossless_weight_spmfD eq_commute)
qed
qed

definition oracle_encrypt3 ::
"('prf_key × 'upf_key) ⇒ bool ⇒ (bool × (bitstring, bitstring) PRF.dict) ⇒
bitstring × bitstring ⇒ ('hash cipher_text option × (bool × (bitstring, bitstring) PRF.dict)) spmf"
where
"oracle_encrypt3 = (λ(k_prf, k_upf) b (bad, D) (msg1, msg0).
(case (length msg1 = prf_clen ∧ length msg0 = prf_clen) of
False ⇒ return_spmf (None, (bad, D))
| True ⇒ do {
x ← spmf_of_set prf_domain;
P ← spmf_of_set (nlists UNIV prf_clen);
let (p, F) = (case D x of Some r ⇒ (P, True) | None ⇒ (P, False));
let c = p [⊕] (if b then msg1 else msg0);
let t = upf_fun k_upf (x @ c);
return_spmf (Some (x, c, t), (bad ∨ F, D(x ↦ p)))
}))"

lemma lossless_oracle_encrypt3 [simp]:
"lossless_spmf (oracle_encrypt3 k b D m10) "
by (cases m10) (simp add: oracle_encrypt3_def prf_domain_nonempty prf_domain_finite
split_def Let_def split: bool.splits)

lemma callee_invariant_oracle_encrypt3 [simp]: "callee_invariant (oracle_encrypt3 key b) fst"
by (unfold_locales) (auto simp add: oracle_encrypt3_def split_def Let_def split: bool.splits)

definition game3 :: "(bitstring, 'hash cipher_text) ind_cca.adversary ⇒ (bool × bool) spmf"
where
"game3 𝒜 ≡ do {
key ← key_gen;
b ← coin_spmf;
(b', (bad, D)) ← exec_gpv (oracle_encrypt3 key b ⊕⇩O oracle_decrypt2 key) 𝒜 (False, Map_empty);
}"

lemma round_3:
assumes "lossless_gpv (ℐ_full ⊕⇩ℐ ℐ_full) 𝒜"
shows "¦measure (measure_spmf (game3 𝒜)) {(b, bad). b} - spmf (game2 𝒜) True¦
proof -
define oracle_encrypt2'
where "oracle_encrypt2' = (λ(k_prf :: 'prf_key, k_upf) b (bad, D) (msg1, msg0).
case length msg1 = prf_clen ∧ length msg0 = prf_clen of
False ⇒ return_spmf (None, (bad, D))
| True ⇒ do {
x ← spmf_of_set prf_domain;
P ← spmf_of_set (nlists UNIV prf_clen);
let (p, F) = (case D x of Some r ⇒ (r, True) | None ⇒ (P, False));
let c = p [⊕] (if b then msg1 else msg0);
let t = upf_fun k_upf (x @ c);
return_spmf (Some (x, c, t), (bad ∨ F, D(x ↦ p)))
})"

have [simp]: "lossless_spmf (oracle_encrypt2' key b D msg10) " for key b D msg10
by (cases msg10) (simp add: oracle_encrypt2'_def prf_domain_nonempty prf_domain_finite
split_def Let_def split: bool.split)
have [simp]: "callee_invariant (oracle_encrypt2' key b) fst" for key b
by (unfold_locales) (auto simp add: oracle_encrypt2'_def split_def Let_def split: bool.splits)

define game2'
where "game2' = (λ𝒜. do {
key ← key_gen;
b ← coin_spmf;
(b', (bad, D)) ← exec_gpv (oracle_encrypt2' key b ⊕⇩O oracle_decrypt2 key) 𝒜 (False, Map_empty);

have game2'_eq: "game2 𝒜 = map_spmf fst (game2' 𝒜)"
proof -
define S where "S = (λ(D1 :: (bitstring, bitstring) PRF.dict) (bad :: bool, D2). D1 = D2)"
have [transfer_rule, simp]: "S Map_empty (b, Map_empty)" for b by (simp add: S_def)

have [transfer_rule]: "((=) ===> (=) ===> S ===> (=) ===> rel_spmf (rel_prod (=) S))
oracle_encrypt2 oracle_encrypt2'"
unfolding oracle_encrypt2_def[abs_def] oracle_encrypt2'_def[abs_def]
by (auto simp add: rel_fun_def Let_def split_def S_def
intro!: rel_spmf_bind_reflI split: bool.split option.split)
have [transfer_rule]: "((=) ===> S ===> (=) ===> rel_spmf (rel_prod (=) S))
oracle_decrypt2 oracle_decrypt2"

show ?thesis unfolding game2_def game2'_def
by (simp add: map_spmf_bind_spmf o_def split_def Map_empty_def[symmetric] del: Map_empty_def)
transfer_prover
qed
(exec_gpv (oracle_encrypt3 key b ⊕⇩O oracle_decrypt2 key) 𝒜 (False, Map_empty))
(exec_gpv (oracle_encrypt2' key b ⊕⇩O oracle_decrypt2 key) 𝒜 (False, Map_empty))"
for key b
apply(auto simp add: assms spmf_rel_map Let_def oracle_encrypt2'_def oracle_encrypt3_def split: plus_oracle_split prod.split bool.split option.split intro!: rel_spmf_bind_reflI rel_spmf_reflI)
done
have "¦measure (measure_spmf (game3 𝒜)) {(b, bad). b} - measure (measure_spmf (game2' 𝒜)) {(b, bad). b}¦ ≤
unfolding game2'_def game3_def
by(rule fundamental_lemma[where ?bad2.0=snd])(intro rel_spmf_bind_reflI rel_spmf_bindI[OF *]; clarsimp)
ultimately show ?thesis by(simp add: spmf_conv_measure_spmf measure_map_spmf vimage_def fst_def)
qed

lemma round_4:
assumes "lossless_gpv (ℐ_full ⊕⇩ℐ ℐ_full) 𝒜"
shows "map_spmf fst (game3 𝒜) = coin_spmf"
proof -
define oracle_encrypt4
where "oracle_encrypt4 = (λ(k_prf :: 'prf_key, k_upf) (s :: unit) (msg1 :: bitstring, msg0 :: bitstring).
case length msg1 = prf_clen ∧ length msg0 = prf_clen of
False ⇒ return_spmf (None, s)
| True ⇒ do {
x ← spmf_of_set prf_domain;
P ← spmf_of_set (nlists UNIV prf_clen);
let c = P;
let t = upf_fun k_upf (x @ c);
return_spmf (Some (x, c, t), s) })"

have [simp]: "lossless_spmf (oracle_encrypt4 k s msg10)" for k s msg10
by (cases msg10) (simp add: oracle_encrypt4_def prf_domain_finite prf_domain_nonempty
split_def Let_def split: bool.splits)

define game4 where "game4 = (λ𝒜. do {
key ← key_gen;
(b', _) ← exec_gpv (oracle_encrypt4 key ⊕⇩O oracle_decrypt2 key) 𝒜 ();
map_spmf ((=) b') coin_spmf})"

have "map_spmf fst (game3 𝒜) = game4 𝒜"
proof -
note [split del] = if_split
define S where "S = (λ(_ :: unit) (_ :: bool × (bitstring, bitstring) PRF.dict). True)"
define initial3 where "initial3 = (False, Map.empty :: (bitstring, bitstring) PRF.dict)"
have [transfer_rule]: "S () initial3" by(simp add: S_def)
have [transfer_rule]: "((=) ===> (=) ===> S ===> (=) ===> rel_spmf (rel_prod (=) S))
(λkey b. oracle_encrypt4 key) oracle_encrypt3"
proof(intro rel_funI; hypsubst)
fix key unit msg10 b Dbad
have "map_spmf fst (oracle_encrypt4 key () msg10) = map_spmf fst (oracle_encrypt3 key b Dbad msg10)"
unfolding oracle_encrypt3_def oracle_encrypt4_def
apply (clarsimp simp add: map_spmf_conv_bind_spmf Let_def split: bool.split prod.split; rule conjI; clarsimp)
apply (rewrite in "⌑ = _" one_time_pad[symmetric, where xs="if b then fst msg10 else snd msg10"])
apply(simp split: if_split)
apply(simp add: bind_map_spmf o_def option.case_distrib case_option_collapse xor_list_commute split_def cong del: option.case_cong_weak if_weak_cong)
done
then show "rel_spmf (rel_prod (=) S) (oracle_encrypt4 key unit msg10) (oracle_encrypt3 key b Dbad msg10)"
by(auto simp add: spmf_rel_eq[symmetric] spmf_rel_map S_def elim: rel_spmf_mono)
qed

show ?thesis
by (simp add: map_spmf_bind_spmf o_def split_def map_spmf_conv_bind_spmf initial3_def[symmetric] eq_commute)
transfer_prover
qed
also have "… = coin_spmf"
by(simp add: map_eq_const_coin_spmf game4_def bind_spmf_const split_def lossless_exec_gpv[OF assms] lossless_weight_spmfD)
finally  show ?thesis .
qed

assumes "interaction_bounded_by isl 𝒜 q"
shows "measure (measure_spmf (game3 𝒜)) {(b, bad). bad} ≤ q / card prf_domain * q"
proof -
have "measure (measure_spmf (game3 𝒜)) {(b, bad). bad} = spmf (map_spmf snd (game3 𝒜)) True"
by (simp add: spmf_conv_measure_spmf measure_map_spmf vimage_def snd_def)
also
have "spmf (map_spmf (fst ∘ snd) (exec_gpv (oracle_encrypt3 k b ⊕⇩O oracle_decrypt2 k) 𝒜 (False, Map.empty))) True ≤ q / card prf_domain * q"
(is "spmf (map_spmf _ (exec_gpv ?oracle _ _)) _ ≤  _")
if k: "k ∈ set_spmf key_gen" for k b
obtain k_prf k_upf where k: "k = (k_prf, k_upf)" by(cases k)
let ?I = "λ(bad, D). finite (dom D) ∧ dom D ⊆ prf_domain"
have "callee_invariant (oracle_encrypt3 k b) ?I"
by unfold_locales(clarsimp simp add: prf_domain_finite oracle_encrypt3_def Let_def split_def split: bool.splits)+
moreover have "callee_invariant (oracle_decrypt2 k) ?I"
by unfold_locales (clarsimp simp add: prf_domain_finite oracle_decrypt2_def)+
ultimately show "callee_invariant ?oracle ?I" by simp

let ?count = "λ(bad, D). card (dom D)"
show "⋀s x y s'. ⟦ (y, s') ∈ set_spmf (?oracle s x); ?I s; isl x ⟧ ⟹ ?count s' ≤ Suc (?count s)"
by(clarsimp simp add: isl_def oracle_encrypt3_def split_def Let_def card_insert_if split: bool.splits)
show "⟦ (y, s') ∈ set_spmf (?oracle s x); ?I s; ¬ isl x ⟧ ⟹ ?count s' ≤ ?count s" for s x y s'
show "spmf (map_spmf (fst ∘ snd) (?oracle s' x)) True ≤ q / card prf_domain"
if I: "?I s'" and bad: "¬ fst s'" and count: "?count s' < q + ?count (False, Map.empty)"
and x: "isl x"
for s' x
proof -
obtain bad D where s' [simp]: "s' = (bad, D)" by(cases s')
from x obtain m1 m0 where x [simp]: "x = Inl (m1, m0)" by(auto elim: islE)
have *: "(case D x of None ⇒ False | Some x ⇒ True) ⟷ x ∈ dom D" for x
by(auto split: option.split)
show ?thesis
proof(cases "length m1 = prf_clen ∧ length m0 = prf_clen")
case True
have "spmf (map_spmf (fst ∘ snd) (?oracle s' x)) True = pmf (bernoulli_pmf (card (dom D ∩ prf_domain) / card prf_domain)) True"
by(simp add: spmf.map_comp o_def oracle_encrypt3_def k * bool.case_distrib[where h="λp. spmf (map_spmf _ p) _"] option.case_distrib[where h=snd] map_spmf_bind_spmf Let_def split_beta bind_spmf_const cong: bool.case_cong option.case_cong split del: if_split split: bool.split)
(simp add: map_spmf_conv_bind_spmf[symmetric] map_mem_spmf_of_set prf_domain_finite prf_domain_nonempty)
also have "… = card (dom D ∩ prf_domain) / card prf_domain"
by(rule pmf_bernoulli_True)(auto simp add: field_simps prf_domain_finite prf_domain_nonempty card_gt_0_iff card_mono)
also have "dom D ∩ prf_domain = dom D" using I by auto
also have "card (dom D) ≤ q" using count by simp
finally show ?thesis by(simp add: divide_right_mono o_def)
next
case False
by(auto simp add: spmf.map_comp o_def oracle_encrypt3_def k split: bool.split)
qed
qed
qed(auto split: plus_oracle_split_asm simp add: oracle_decrypt2_def assms)
then have "spmf (map_spmf snd (game3 𝒜)) True ≤ q / card prf_domain * q"
by(auto 4 3 simp add: game3_def map_spmf_bind_spmf o_def split_def map_spmf_conv_bind_spmf intro: spmf_bind_leI)
finally show ?thesis .
qed

theorem security:
assumes lossless: "lossless_gpv (ℐ_full ⊕⇩ℐ ℐ_full) 𝒜"
and bound: "interaction_bounded_by isl 𝒜 q"
real q / real (card prf_domain) * real q" (is "?LHS ≤ _")
proof -
have "?LHS ≤ ¦spmf (ind_cca.game 𝒜) True - spmf (ind_cca'.game 𝒜) True¦ + ¦spmf (ind_cca'.game 𝒜) True - 1 / 2¦"
also have "?round1 ≤ UPF.advantage (reduction_upf 𝒜)"
using lossless by(rule round_1)
also have "?rest ≤ ¦spmf (ind_cca'.game 𝒜) True - spmf (game2 𝒜) True¦ + ¦spmf (game2 𝒜) True - 1 / 2¦"
(is "_ ≤ ?round2 + ?rest") using abs_triangle_ineq by simp
also have "?round2 = PRF.advantage (reduction_prf 𝒜)" by(rule round_2)
also have "?rest ≤ ¦measure (measure_spmf (game3 𝒜)) {(b, bad). b} - spmf (game2 𝒜) True¦ +
¦measure (measure_spmf (game3 𝒜)) {(b, bad). b} - 1 / 2¦"
(is "_ ≤ ?round3 + _") using abs_triangle_ineq by simp
assumes lossless: "lossless_gpv (ℐ_full