Theory Diffie_Hellman
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)
}"
definition advantage :: "'grp adversary ⇒ real"
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)
}"
definition advantage :: "'grp adversary ⇒ real"
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
theory IND_CCA2 imports
CryptHOL.Computational_Model
CryptHOL.Negligible
CryptHOL.Environment_Functor
begin
locale pk_enc =
fixes 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"
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"
definition advantage⇩1 :: "('ekey, 'plain, 'cipher) adversary⇩1 ⇒ advantage"
where "advantage⇩1 𝒜 η = ¦spmf (ind_cca2⇩1 𝒜 η) True - 1/2¦"
lemma advantage⇩1_nonneg: "advantage⇩1 𝒜 η ≥ 0" by(simp add: advantage⇩1_def)
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)"
by(simp add: oracle⇩n_def)
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"
definition advantage⇩n :: "('i, 'ekey, 'plain, 'cipher) adversary⇩n ⇒ advantage"
where "advantage⇩n 𝒜 η = ¦spmf (ind_cca2⇩n 𝒜 η) True - 1/2¦"
lemma advantage⇩n_nonneg: "advantage⇩n 𝒜 η ≥ 0" by(simp add: advantage⇩n_def)
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"
by(auto simp add: cipher_queries_def ran_def)
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 = {}"
by(simp add: cipher_queries_def)
end
end
Theory IND_CCA2_sym
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
type_synonym ('message', 'cipher') adversary =
"(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)"
by(simp add: oracle_decrypt_def)
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')
}"
definition advantage :: "('message, 'cipher) adversary ⇒ real"
where "advantage 𝒜 = ¦spmf (game 𝒜) True - 1 / 2¦"
lemma advantage_nonneg: "0 ≤ advantage 𝒜" by(simp add: advantage_def)
end
end
Theory IND_CPA
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"
and encrypt :: "'key ⇒ 'plain ⇒ 'cipher spmf"
and decrypt :: "'key ⇒ 'cipher ⇒ 'plain option"
and valid_plain :: "'plain ⇒ bool"
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)
}"
definition advantage :: "('plain, 'cipher, 'state) adversary ⇒ real"
where "advantage 𝒜 = ¦spmf (ind_cpa 𝒜) True - 1/2¦"
lemma advantage_nonneg: "advantage 𝒜 ≥ 0" by(simp add: advantage_def)
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"
by(auto simp add: ibounded_by_def)
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
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"
and aencrypt :: "'pubkey ⇒ 'plain ⇒ ('cipher, 'call, 'ret) gpv"
and adecrypt :: "'privkey ⇒ 'cipher ⇒ ('plain, 'call, 'ret) gpv"
and valid_plains :: "'plain ⇒ 'plain ⇒ bool"
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¦"
lemma advantage_nonneg: "advantage oracle σ 𝒜 ≥ 0" by(simp add: advantage_def)
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"
by(auto simp add: ibounded_by_def)
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
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"
and aencrypt :: "'pub_key ⇒ 'plain ⇒ 'cipher spmf"
and adecrypt :: "'priv_key ⇒ 'cipher ⇒ 'plain option"
and valid_plains :: "'plain ⇒ 'plain ⇒ bool"
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]
definition advantage :: "('pub_key, 'plain, 'cipher, 'state) adversary ⇒ real"
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
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"
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)"
by(simp_all add: oracle⇩1_def)
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)
}"
definition advantage⇩1 :: "('vkey, 'message, 'signature) adversary⇩1 ⇒ advantage"
where "advantage⇩1 𝒜 η = spmf (suf_cma⇩1 𝒜 η) True"
lemma advantage⇩1_nonneg: "advantage⇩1 𝒜 η ≥ 0" by(simp add: advantage⇩1_def pmf_nonneg)
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)"
by(simp add: oracle⇩n_def)
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)
}"
definition advantage⇩n :: "('i, 'vkey, 'message, 'signature) adversary⇩n ⇒ advantage"
where "advantage⇩n 𝒜 η = spmf (suf_cma⇩n 𝒜 η) True"
lemma advantage⇩n_nonneg: "advantage⇩n 𝒜 η ≥ 0" by(simp add: advantage⇩n_def pmf_nonneg)
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
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)"
by(simp add: lossless_spmf_def)
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
}"
definition advantage :: "('domain, 'range) adversary ⇒ real"
where "advantage 𝒜 = ¦spmf (game_0 𝒜) True - spmf (game_1 𝒜) True¦"
lemma advantage_nonneg: "advantage 𝒜 ≥ 0"
by(simp add: advantage_def)
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
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)"
by(simp add: lossless_spmf_def)
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
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
}"
definition advantage_single :: "('c_a, 'guess, 'call, 'ret) adversary_single ⇒ real"
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
}"
definition advantage_multi :: "('c_a, 'guess, 'call, 'ret) adversary_many ⇒ real"
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)"
shows "advantage_multi 𝒜 ≤ advantage_single (reduction q 𝒜) * q"
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})"
by(simp add: measure_pair_spmf_times spmf_conv_measure_spmf[symmetric] spmf_of_set)
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}"
by (auto simp add: vimage_def)
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'")
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]) }
ultimately show ?thesis unfolding advantage_multi_def advantage_single_def
by(simp add: mult_right_mono)
qed
end
end
Theory Unpredictable_Function
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'
}"
definition advantage :: "('x, 'hash) adversary ⇒ real"
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)
}"
definition advantage1 :: "('x, 'hash) adversary1 ⇒ real"
where "advantage1 𝒜 = spmf (game1 𝒜) True"
lemma advantage_advantage1:
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
by(simp add: oracle_flag_def eval_oracle_def fun_eq_iff)
have "game 𝒜 = game_multi (λ_. 𝒜)"
by(auto simp add: game_multi_def game_def bind_map_spmf intro!: bind_spmf_cong[OF refl])
hence "advantage 𝒜 = advantage_multi (λ_. 𝒜)" by(simp add: advantage_def advantage_multi_def)
also have "… ≤ advantage_single (reduction q (λ_. 𝒜)) * q" using bound
by(rule many_single_reduction)(auto simp add: oracle_hash_def)
also have "advantage_single (reduction q (λ_. 𝒜)) = advantage1 (reduction q (λ_. 𝒜) ())" for 𝒜
unfolding advantage1_def advantage_single_def
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 Elgamal
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 𝒢))"
by(simp add: map_spmf_conv_bind_spmf key_gen_def)
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 𝒢))"
by(simp add: map_spmf_conv_bind_spmf aencrypt_def)
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 𝒢 .
fun elgamal_adversary :: "('grp pub_key, 'grp plain, 'grp cipher, 'state) ind_cpa.adversary ⇒ 'grp ddh.adversary"
where
"elgamal_adversary (𝒜1, 𝒜2) α β γ = TRY do {
b ← coin_spmf;
((msg1, msg2), σ) ← 𝒜1 α;
_ :: 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
theorem advantage_elgamal: "ind_cpa.advantage 𝒜 = ddh.advantage (elgamal_adversary 𝒜)"
including monad_normalisation
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"
by(simp add: ddh.ddh_1_def)
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"
by(simp add: sample_uniform_one_time_pad map_spmf_conv_bind_spmf[where p=coin_spmf])
also have "… = coin_spmf"
by(simp add: map_eq_const_coin_spmf try_bind_spmf_lossless2')
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)
ultimately show ?thesis by(simp add: ddh.advantage_def ind_cpa.advantage_def)
qed
end
locale elgamal_asymp =
fixes 𝒢 :: "security ⇒ 'grp cyclic_group"
assumes elgamal: "⋀η. elgamal (𝒢 η)"
begin
sublocale elgamal "𝒢 η" for η by(simp add: elgamal)
theorem elgamal_secure:
"negligible (λη. ind_cpa.advantage η (𝒜 η))" if "negligible (λη. ddh.advantage η (elgamal_adversary η (𝒜 η)))"
by(simp add: advantage_elgamal that)
end
context elgamal_base begin
lemma lossless_key_gen [simp]: "lossless_spmf (key_gen) ⟷ 0 < order 𝒢"
by(simp add: key_gen_def Let_def)
lemma lossless_aencrypt [simp]:
"lossless_spmf (aencrypt key plain) ⟷ 0 < order 𝒢"
by(simp add: aencrypt_def Let_def)
lemma lossless_elgamal_adversary:
"⟦ ind_cpa.lossless 𝒜; 0 < order 𝒢 ⟧
⟹ ddh.lossless (elgamal_adversary 𝒜)"
by(cases 𝒜)(simp add: ddh.lossless_def ind_cpa.lossless_def Let_def split_def)
end
end
Theory Hashed_Elgamal
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))"
by(auto simp add: invariant.simps ran_def)
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)"
by(simp add: oracle_def split: option.split)
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 𝒢"
by(simp add: aencrypt_def Let_def)
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 𝒢 .
fun elgamal_adversary
:: "('grp pub_key, plain, 'grp cipher, 'grp, bitstring, 'state) ind_cpa.adversary
⇒ 'grp lcdh.adversary"
where
"elgamal_adversary (𝒜1, 𝒜2) α β = do {
(((msg1, msg2), σ), s) ← exec_gpv hash.oracle (𝒜1 α) hash.initial;
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)
lemma advantage_elgamal:
includes lifting_syntax
assumes lossless: "ind_cpa.lossless 𝒜"
shows "ind_cpa.advantage hash.oracle hash.initial 𝒜 ≤ lcdh.advantage (elgamal_adversary 𝒜)"
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)"
by(auto simp add: ind_cpa.lossless_def)
text ‹We change the adversary's oracle to record the queries made by the adversary›
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)
including monad_normalisation by(simp add: bind_rpv_def nat_pow_pow)
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);
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
by unfold_locales(auto simp add: hash_oracle''_def)
{ 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)
have inv: "callee_invariant hash_oracle'' ?bad"
by(unfold_locales)(auto simp add: hash_oracle''_def split: option.split_asm)
have "rel_spmf (λ(win, bad) (win', bad'). bad = bad' ∧ (¬ bad' ⟶ win = win')) (game2 x y) (game1 x y)"
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
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 }
hence "rel_spmf (λ(win, bad) (win', bad'). (bad ⟷ bad') ∧ (¬ bad' ⟶ win ⟷ win')) (?sample game2) (?sample game1)"
by(intro rel_spmf_bind_reflI)
hence "¦measure (measure_spmf (?sample game2)) {(x, _). x} - measure (measure_spmf (?sample game1)) {(y, _). y}¦
≤ measure (measure_spmf (?sample game2)) {(_, bad). bad}"
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
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 𝒜)"
using game23 by(simp add: o_def)
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
including monad_normalisation
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¦"
using game0 by(simp add: ind_cpa_pk.advantage_def game01 o_def)
also have "… = ¦1 / 2 - spmf (map_spmf fst (?sample game1)) True¦"
by(simp add: abs_minus_commute)
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
finally show ?thesis by(simp add: lcdh.advantage_def)
qed
end
context elgamal_base begin
lemma lossless_key_gen [simp]: "lossless_spmf key_gen ⟷ 0 < order 𝒢"
by(simp add: key_gen_def Let_def)
lemma lossless_elgamal_adversary:
"⟦ ind_cpa.lossless 𝒜; ⋀η. 0 < order 𝒢 ⟧
⟹ lcdh.lossless (elgamal_adversary 𝒜)"
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
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'
by(simp add: spmf_bind integral_spmf_of_set sum_Un spmf_of_set field_simps)(simp add: field_simps card_Un_disjoint)
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"
definition advantage :: "'a adversary ⇒ real" where
"advantage 𝒜 = ¦spmf (prp_game 𝒜) True - spmf (prf_game 𝒜) True¦"
lemma advantage_nonneg: "0 ≤ advantage 𝒜" by(simp add: advantage_def)
lemma advantage_le_1: "advantage 𝒜 ≤ 1"
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))))))"
have rp_bad_simps: "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))))))"
for bad σ x by(simp add: rp_bad_def)
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"
unfolding rp rp_bad_def
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)
let ?bad1 = "collision" and ?bad2 = "fst"
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)
have [simp]: "callee_invariant_on rp_bad (λs2. ?bad2 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)
have [simp]: "ℐ ⊢c rp_bad (bad, σ2) √" if "ran σ2 ⊆ A" for bad σ2 using that
by(intro WT_calleeI)(auto simp add: rp_bad_def finite_A nonempty_A ran_def split: option.split_asm if_split_asm)
have [simp]: "lossless_spmf (rp_bad (b, σ2) x)" if "x ∈ A" "dom σ2 ⊆ A" "ran σ2 ⊆ A" for b σ2 x
using finite_A that unfolding rp_bad_def
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
by(intro fundamental_lemma[where ?bad2.0="λ(_, s2). ?bad2 s2"])(auto simp add: split_def elim: rel_spmf_mono)
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"
by(simp add: ennreal_of_nat_eq_real_of_nat ennreal_times_divide ennreal_mult''[symmetric])
finally have "¦spmf (run_gpv rp_bad 𝒜 init) True - spmf (run_gpv rf.random_oracle 𝒜 Map.empty) True¦ ≤ q * q / card A"
by simp }
ultimately show ?thesis by(simp add: advantage_def game_def)
qed
end
end
Theory PRF_UHF
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'})"
by(auto intro!: measure_spmf.finite_measure_subadditive_finite simp add: split_def assms)
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"
by(simp add: rand_def range_f_finite range_f_nonempty)
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, ()))"
definition prf'_reduction :: " ('β, 'γ) prf'.adversary ⇒ ('α, 'γ) prf.adversary"
where
"prf'_reduction 𝒜 = do {
seed ← lift_spmf seed_gen;
(b, σ) ← inline (reduction_oracle seed) 𝒜 ();
Done b
}"
theorem prf_prf'_advantage:
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
define game_semi_forgetful_bad where "game_semi_forgetful_bad = do {
seed :: 'seed ← seed_gen;
x ← exec_gpv (semi_forgetful_RO seed) 𝒜 (Map.empty, False);
return_spmf (snd x)
}"
have game_semi_forgetful_bad : "map_spmf snd game_semi_forgetful = game_semi_forgetful_bad"
unfolding game_semi_forgetful_bad_def game_semi_forgetful_def
by(simp add: map_spmf_bind_spmf o_def)
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)))"
have rel_spmf_oracle_adv:
"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)"
by(simp_all add: invar_def)
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
by(simp add: semi_forgetful_RO_def prf.random_oracle_def split_beta)
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
by(rule exec_gpv_oracle_bisim_bad_full[where ?bad1.0 = "snd" and ?bad2.0 = "λσ. ¬ inj_on (h seed) (dom σ)"])
(simp_all add: assms)
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 σ))
}"
let ?bad1 = "λx. snd (snd x)" and ?bad2 = "snd"
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)
(rule rel_spmf_bindI[OF rel_spmf_oracle_adv]; auto)
have bad1_bad2: "spmf (map_spmf (snd ∘ snd) game_semi_forgetful) True = spmf (map_spmf snd game_A) True"
using fundamental_lemma_bad[OF hop3] by(simp add: measure_map_spmf spmf_conv_measure_spmf vimage_def)
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"
using bad1_bad2 by (simp)
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
by(simp add: map_spmf_bind_spmf o_def split_def)
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"
by(simp add: hash.ε_uh_nonneg mult_left_mono)
qed(simp add: hash.ε_uh_nonneg)
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¦"
using hop1 by(simp add: prf'.advantage_def)
also have "… ≤ prf.advantage ?𝒜 + ¦spmf (prf.game_1 ?𝒜) True - spmf (prf'.game_1 𝒜) True¦"
by(simp add: prf.advantage_def)
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)
finally show ?thesis by(simp add: add_left_mono)
qed
end
end
Theory PRF_IND_CPA
subsection ‹IND-CPA from PRF›
theory PRF_IND_CPA imports
CryptHOL.GPV_Bisim
CryptHOL.List_Bits
Pseudo_Random_Function
IND_CPA
begin
text ‹
Formalises the construction from \cite{PetcherMorrisett2015POST}.
›
declare [[simproc del: let_simp]]
type_synonym key = "bool list"
type_synonym plain = "bool list"
type_synonym cipher = "bool list * bool list"
locale otp =
fixes f :: "key ⇒ bool list ⇒ bool list"
and len :: nat
assumes length_f: "⋀xs ys. ⟦ length xs = len; length ys = len ⟧ ⟹ length (f xs ys) = len"
begin
definition key_gen :: "bool list spmf"
where "key_gen = spmf_of_set (nlists UNIV len)"
definition valid_plain :: "plain ⇒ bool"
where "valid_plain plain ⟷ length plain = len"
definition encrypt :: "key ⇒ plain ⇒ cipher spmf"
where
"encrypt key plain = do {
r ← spmf_of_set (nlists UNIV len);
return_spmf (r, xor_list plain (f key r))
}"
fun decrypt :: "key ⇒ cipher ⇒ plain option"
where "decrypt key (r, c) = Some (xor_list (f key r) c)"
lemma encrypt_decrypt_correct:
"⟦ length key = len; length plain = len ⟧
⟹ encrypt key plain ⤜ (λcipher. return_spmf (decrypt key cipher)) = return_spmf (Some plain)"
by(simp add: encrypt_def zip_map2 o_def split_def bind_eq_return_spmf length_f in_nlists_UNIV xor_list_left_commute)
interpretation ind_cpa: ind_cpa key_gen encrypt decrypt valid_plain .
interpretation "prf": "prf" key_gen f "spmf_of_set (nlists UNIV len)" .
definition prf_encrypt_oracle :: "unit ⇒ plain ⇒ (cipher × unit, plain, plain) gpv"
where
"prf_encrypt_oracle x plain = do {
r ← lift_spmf (spmf_of_set (nlists UNIV len));
Pause r (λpad. Done ((r, xor_list plain pad), ()))
}"
lemma interaction_bounded_by_prf_encrypt_oracle [interaction_bound]:
"interaction_any_bounded_by (prf_encrypt_oracle σ plain) 1"
unfolding prf_encrypt_oracle_def by simp
lemma lossless_prf_encyrpt_oracle [simp]: "lossless_gpv ℐ_top (prf_encrypt_oracle s x)"
by(simp add: prf_encrypt_oracle_def)
definition prf_adversary :: "(plain, cipher, 'state) ind_cpa.adversary ⇒ (plain, plain) prf.adversary"
where
"prf_adversary 𝒜 = do {
let (𝒜1, 𝒜2) = 𝒜;
(((p1, p2), σ), n) ← inline prf_encrypt_oracle 𝒜1 ();
if valid_plain p1 ∧ valid_plain p2 then do {
b ← lift_spmf coin_spmf;
let pb = (if b then p1 else p2);
r ← lift_spmf (spmf_of_set (nlists UNIV len));
pad ← Pause r Done;
let c = (r, xor_list pb pad);
(b', _) ← inline prf_encrypt_oracle (𝒜2 c σ) n;
Done (b' = b)
} else lift_spmf coin_spmf
}"
theorem prf_encrypt_advantage:
assumes "ind_cpa.ibounded_by 𝒜 q"
and "lossless_gpv ℐ_full (fst 𝒜)"
and "⋀cipher σ. lossless_gpv ℐ_full (snd 𝒜 cipher σ)"
shows "ind_cpa.advantage 𝒜 ≤ prf.advantage (prf_adversary 𝒜) + q / 2 ^ len"
proof -
note [split del] = if_split
and [cong del] = if_weak_cong
and [simp] =
bind_spmf_const map_spmf_bind_spmf bind_map_spmf
exec_gpv_bind exec_gpv_inline
rel_spmf_bind_reflI rel_spmf_reflI
obtain 𝒜1 𝒜2 where 𝒜: "𝒜 = (𝒜1, 𝒜2)" by(cases "𝒜")
from ‹ind_cpa.ibounded_by _ _›
obtain q1 q2 :: nat
where q1: "interaction_any_bounded_by 𝒜1 q1"
and q2: "⋀cipher σ. interaction_any_bounded_by (𝒜2 cipher σ) q2"
and "q1 + q2 ≤ q"
unfolding 𝒜 by(rule ind_cpa.ibounded_byE)(auto simp add: iadd_le_enat_iff)
from 𝒜 assms have lossless1: "lossless_gpv ℐ_full 𝒜1"
and lossless2: "⋀cipher σ. lossless_gpv ℐ_full (𝒜2 cipher σ)" by simp_all
have weight1: "⋀oracle s. (⋀s x. lossless_spmf (oracle s x))
⟹ weight_spmf (exec_gpv oracle 𝒜1 s) = 1"
by(rule lossless_weight_spmfD)(rule lossless_exec_gpv[OF lossless1], simp_all)
have weight2: "⋀oracle s cipher σ. (⋀s x. lossless_spmf (oracle s x))
⟹ weight_spmf (exec_gpv oracle (𝒜2 cipher σ) s) = 1"
by(rule lossless_weight_spmfD)(rule lossless_exec_gpv[OF lossless2], simp_all)
let ?oracle1 = "λkey (s', s) y. map_spmf (λ((x, s'), s). (x, (), ())) (exec_gpv (prf.prf_oracle key) (prf_encrypt_oracle () y) ())"
have bisim1: "⋀key. rel_spmf (λ(x, _) (y, _). x = y)
(exec_gpv (ind_cpa.encrypt_oracle key) 𝒜1 ())
(exec_gpv (?oracle1 key) 𝒜1 ((), ()))"
using TrueI
by(rule exec_gpv_oracle_bisim)(auto simp add: encrypt_def prf_encrypt_oracle_def ind_cpa.encrypt_oracle_def prf.prf_oracle_def o_def)
have bisim2: "⋀key cipher σ. rel_spmf (λ(x, _) (y, _). x = y)
(exec_gpv (ind_cpa.encrypt_oracle key) (𝒜2 cipher σ) ())
(exec_gpv (?oracle1 key) (𝒜2 cipher σ) ((), ()))"
using TrueI
by(rule exec_gpv_oracle_bisim)(auto simp add: encrypt_def prf_encrypt_oracle_def ind_cpa.encrypt_oracle_def prf.prf_oracle_def o_def)
have ind_cpa_0: "rel_spmf (=) (ind_cpa.ind_cpa 𝒜) (prf.game_0 (prf_adversary 𝒜))"
unfolding IND_CPA.ind_cpa.ind_cpa_def 𝒜 key_gen_def Let_def prf_adversary_def Pseudo_Random_Function.prf.game_0_def
apply(simp)
apply(rewrite in "bind_spmf _ ⌑" bind_commute_spmf)
apply(rule rel_spmf_bind_reflI)
apply(rule rel_spmf_bindI[OF bisim1])
apply(clarsimp simp add: if_distribs bind_coin_spmf_eq_const')
apply(auto intro: rel_spmf_bindI[OF bisim2] intro!: rel_spmf_bind_reflI simp add: encrypt_def prf.prf_oracle_def cong del: if_cong)
done
define rf_encrypt where "rf_encrypt = (λs plain. bind_spmf (spmf_of_set (nlists UNIV len)) (λr :: bool list.
bind_spmf (prf.random_oracle s r) (λ(pad, s').
return_spmf ((r, xor_list plain pad), s')))
)"
interpret rf_finite: callee_invariant_on rf_encrypt "λs. finite (dom s)" ℐ_full
by unfold_locales(auto simp add: rf_encrypt_def dest: prf.finite.callee_invariant)
have lossless_rf_encrypt [simp]: "⋀s plain. lossless_spmf (rf_encrypt s plain)"
by(auto simp add: rf_encrypt_def)
define game2 where "game2 = do {
(((p0, p1), σ), s1) ← exec_gpv rf_encrypt 𝒜1 Map.empty;
if valid_plain p0 ∧ valid_plain p1 then do {
b ← coin_spmf;
let pb = (if b then p0 else p1);
(cipher, s2) ← rf_encrypt s1 pb;
(b', s3) ← exec_gpv rf_encrypt (𝒜2 cipher σ) s2;
return_spmf (b' = b)
} else coin_spmf
}"
let ?oracle2 = "λ(s', s) y. map_spmf (λ((x, s'), s). (x, (), s)) (exec_gpv prf.random_oracle (prf_encrypt_oracle () y) s)"
let ?I = "λ(x, _, s) (y, s'). x = y ∧ s = s'"
have bisim1: "rel_spmf ?I (exec_gpv ?oracle2 𝒜1 ((), Map.empty)) (exec_gpv rf_encrypt 𝒜1 Map.empty)"
by(rule exec_gpv_oracle_bisim[where X="λ(_, s) s'. s = s'"])
(auto simp add: rf_encrypt_def prf_encrypt_oracle_def intro!: rel_spmf_bind_reflI)
have bisim2: "⋀cipher σ s. rel_spmf ?I (exec_gpv ?oracle2 (𝒜2 cipher σ) ((), s)) (exec_gpv rf_encrypt (𝒜2 cipher σ) s)"
by(rule exec_gpv_oracle_bisim[where X="λ(_, s) s'. s = s'"])
(auto simp add: prf_encrypt_oracle_def rf_encrypt_def intro!: rel_spmf_bind_reflI)
have game1_2 [unfolded spmf_rel_eq]: "rel_spmf (=) (prf.game_1 (prf_adversary 𝒜)) game2"
unfolding prf.game_1_def game2_def prf_adversary_def
by(rewrite in "if _ then ⌑ else _" rf_encrypt_def)
(auto simp add: Let_def 𝒜 if_distribs intro!: rel_spmf_bindI[OF bisim2] rel_spmf_bind_reflI rel_spmf_bindI[OF bisim1])
define game2_a where "game2_a = do {
r ← spmf_of_set (nlists UNIV len);
(((p0, p1), σ), s1) ← exec_gpv rf_encrypt 𝒜1 Map.empty;
let bad = r ∈ dom s1;
if valid_plain p0 ∧ valid_plain p1 then do {
b ← coin_spmf;
let pb = (if b then p0 else p1);
(pad, s2) ← prf.random_oracle s1 r;
let cipher = (r, xor_list pb pad);
(b', s3) ← exec_gpv rf_encrypt (𝒜2 cipher σ) s2;
return_spmf (b' = b, bad)
} else coin_spmf ⤜ (λb. return_spmf (b, bad))
}"
define game2_b where "game2_b = do {
r ← spmf_of_set (nlists UNIV len);
(((p0, p1), σ), s1) ← exec_gpv rf_encrypt 𝒜1 Map.empty;
let bad = r ∈ dom s1;
if valid_plain p0 ∧ valid_plain p1 then do {
b ← coin_spmf;
let pb = (if b then p0 else p1);
pad ← spmf_of_set (nlists UNIV len);
let cipher = (r, xor_list pb pad);
(b', s3) ← exec_gpv rf_encrypt (𝒜2 cipher σ) (s1(r ↦ pad));
return_spmf (b' = b, bad)
} else coin_spmf ⤜ (λb. return_spmf (b, bad))
}"
have "game2 = do {
r ← spmf_of_set (nlists UNIV len);
(((p0, p1), σ), s1) ← exec_gpv rf_encrypt 𝒜1 Map.empty;
if valid_plain p0 ∧ valid_plain p1 then do {
b ← coin_spmf;
let pb = (if b then p0 else p1);
(pad, s2) ← prf.random_oracle s1 r;
let cipher = (r, xor_list pb pad);
(b', s3) ← exec_gpv rf_encrypt (𝒜2 cipher σ) s2;
return_spmf (b' = b)
} else coin_spmf
}"
including monad_normalisation by(simp add: game2_def split_def rf_encrypt_def Let_def)
also have "… = map_spmf fst game2_a" unfolding game2_a_def
by(clarsimp simp add: map_spmf_conv_bind_spmf Let_def if_distribR if_distrib split_def cong: if_cong)
finally have game2_2a: "game2 = …" .
have "map_spmf snd game2_a = map_spmf snd game2_b" unfolding game2_a_def game2_b_def
by(auto simp add: o_def Let_def split_def if_distribs weight2 split: option.split intro: bind_spmf_cong[OF refl])
moreover
have "rel_spmf (=) (map_spmf fst (game2_a ↿ (snd -` {False}))) (map_spmf fst (game2_b ↿ (snd -` {False})))"
unfolding game2_a_def game2_b_def
by(clarsimp simp add: restrict_bind_spmf o_def Let_def if_distribs split_def restrict_return_spmf prf.random_oracle_def intro!: rel_spmf_bind_reflI split: option.splits)
hence "spmf game2_a (True, False) = spmf game2_b (True, False)"
unfolding spmf_rel_eq by(subst (1 2) spmf_map_restrict[symmetric]) simp
ultimately
have game2a_2b: "¦spmf (map_spmf fst game2_a) True - spmf (map_spmf fst game2_b) True¦ ≤ spmf (map_spmf snd game2_a) True"
by(subst (1 2) spmf_conv_measure_spmf)(rule identical_until_bad; simp add: spmf.map_id[unfolded id_def] spmf_conv_measure_spmf)
define game2_a_bad where "game2_a_bad = do {
r ← spmf_of_set (nlists UNIV len);
(((p0, p1), σ), s1) ← exec_gpv rf_encrypt 𝒜1 Map.empty;
return_spmf (r ∈ dom s1)
}"
have game2a_bad: "map_spmf snd game2_a = game2_a_bad"
unfolding game2_a_def game2_a_bad_def
by(auto intro!: bind_spmf_cong[OF refl] simp add: o_def weight2 Let_def split_def split: if_split)
have card: "⋀B :: bool list set. card (B ∩ nlists UNIV len) ≤ card (nlists UNIV len :: bool list set)"
by(rule card_mono) simp_all
then have "spmf game2_a_bad True = ∫⇧+ x. card (dom (snd x) ∩ nlists UNIV len) / 2 ^ len ∂measure_spmf (exec_gpv rf_encrypt 𝒜1 Map.empty)"
unfolding game2_a_bad_def
by(rewrite bind_commute_spmf)(simp add: ennreal_spmf_bind split_def map_mem_spmf_of_set[unfolded map_spmf_conv_bind_spmf] card_nlists)
also { fix x s
assume *: "(x, s) ∈ set_spmf (exec_gpv rf_encrypt 𝒜1 Map.empty)"
hence "finite (dom s)" by(rule rf_finite.exec_gpv_invariant) simp_all
hence 1: "card (dom s ∩ nlists UNIV len) ≤ card (dom s)" by(intro card_mono) simp_all
moreover from q1 *
have "card (dom s) ≤ q1 + card (dom (Map.empty :: (plain, plain) prf.dict))"
by(rule rf_finite.interaction_bounded_by'_exec_gpv_count)
(auto simp add: rf_encrypt_def eSuc_enat prf.random_oracle_def card_insert_if split: option.split_asm if_split)
ultimately have "card (dom s ∩ nlists UNIV len) ≤ q1" by(simp) }
then have "… ≤ ∫⇧+ x. q1 / 2 ^ len ∂measure_spmf (exec_gpv rf_encrypt 𝒜1 Map.empty)"
by(intro nn_integral_mono_AE)(clarsimp simp add: field_simps)
also have "… ≤ q1 / 2 ^ len"
by(simp add: measure_spmf.emeasure_eq_measure field_simps mult_left_le weight1)
finally have game2a_bad_bound: "spmf game2_a_bad True ≤ q1 / 2 ^ len" by simp
define rf_encrypt_bad
where "rf_encrypt_bad = (λsecret (s :: (plain, plain) prf.dict, bad) plain. bind_spmf
(spmf_of_set (nlists UNIV len)) (λr.
bind_spmf (prf.random_oracle s r) (λ(pad, s').
return_spmf ((r, xor_list plain pad), (s', bad ∨ r = secret)))))"
have rf_encrypt_bad_sticky [simp]: "⋀s. callee_invariant (rf_encrypt_bad s) snd"
by(unfold_locales)(auto simp add: rf_encrypt_bad_def)
have lossless_rf_encrypt [simp]: "⋀challenge s plain. lossless_spmf (rf_encrypt_bad challenge s plain)"
by(clarsimp simp add: rf_encrypt_bad_def prf.random_oracle_def split: option.split)
define game2_c where "game2_c = do {
r ← spmf_of_set (nlists UNIV len);
(((p0, p1), σ), s1) ← exec_gpv rf_encrypt 𝒜1 Map.empty;
if valid_plain p0 ∧ valid_plain p1 then do {
b ← coin_spmf;
let pb = (if b then p0 else p1);
pad ← spmf_of_set (nlists UNIV len);
let cipher = (r, xor_list pb pad);
(b', (s2, bad)) ← exec_gpv (rf_encrypt_bad r) (𝒜2 cipher σ) (s1(r ↦ pad), False);
return_spmf (b' = b, bad)
} else coin_spmf ⤜ (λb. return_spmf (b, False))
}"
have bisim2c_bad: "⋀cipher σ s x r. rel_spmf (λ(x, _) (y, _). x = y)
(exec_gpv rf_encrypt (𝒜2 cipher σ) (s(x ↦ r)))
(exec_gpv (rf_encrypt_bad x) (𝒜2 cipher σ) (s(x ↦ r), False))"
by(rule exec_gpv_oracle_bisim[where X="λs (s', _). s = s'"])
(auto simp add: rf_encrypt_bad_def rf_encrypt_def intro!: rel_spmf_bind_reflI)
have game2b_c [unfolded spmf_rel_eq]: "rel_spmf (=) (map_spmf fst game2_b) (map_spmf fst game2_c)"
by(auto simp add: game2_b_def game2_c_def o_def split_def Let_def if_distribs intro!: rel_spmf_bind_reflI rel_spmf_bindI[OF bisim2c_bad])
define game2_d where "game2_d = do {
r ← spmf_of_set (nlists UNIV len);
(((p0, p1), σ), s1) ← exec_gpv rf_encrypt 𝒜1 Map.empty;
if valid_plain p0 ∧ valid_plain p1 then do {
b ← coin_spmf;
let pb = (if b then p0 else p1);
pad ← spmf_of_set (nlists UNIV len);
let cipher = (r, xor_list pb pad);
(b', (s2, bad)) ← exec_gpv (rf_encrypt_bad r) (𝒜2 cipher σ) (s1, False);
return_spmf (b' = b, bad)
} else coin_spmf ⤜ (λb. return_spmf (b, False))
}"
{ fix cipher σ and x :: plain and s r
let ?I = "(λ(x, s, bad) (y, s', bad'). (bad ⟷ bad') ∧ (¬ bad' ⟶ x ⟷ y))"
let ?X = "λ(s, bad) (s', bad'). bad = bad' ∧ (∀z. z ≠ x ⟶ s z = s' z)"
have "⋀s1 s2 x'. ?X s1 s2 ⟹ rel_spmf (λ(a, s1') (b, s2'). snd s1' = snd s2' ∧ (¬ snd s2' ⟶ a = b ∧ ?X s1' s2'))
(rf_encrypt_bad x s1 x') (rf_encrypt_bad x s2 x')"
by(case_tac "x = x'")(clarsimp simp add: rf_encrypt_bad_def prf.random_oracle_def rel_spmf_return_spmf1 rel_spmf_return_spmf2 Let_def split_def bind_UNION intro!: rel_spmf_bind_reflI split: option.split)+
with _ _ have "rel_spmf ?I
(exec_gpv (rf_encrypt_bad x) (𝒜2 cipher σ) (s(x ↦ r), False))
(exec_gpv (rf_encrypt_bad x) (𝒜2 cipher σ) (s, False))"
by(rule exec_gpv_oracle_bisim_bad_full)(auto simp add: lossless2) }
note bisim_bad = this
have game2c_2d_bad [unfolded spmf_rel_eq]: "rel_spmf (=) (map_spmf snd game2_c) (map_spmf snd game2_d)"
by(auto simp add: game2_c_def game2_d_def o_def Let_def split_def if_distribs intro!: rel_spmf_bind_reflI rel_spmf_bindI[OF bisim_bad])
moreover
have "rel_spmf (=) (map_spmf fst (game2_c ↿ (snd -` {False}))) (map_spmf fst (game2_d ↿ (snd -` {False})))"
unfolding game2_c_def game2_d_def
by(clarsimp simp add: restrict_bind_spmf o_def Let_def if_distribs split_def restrict_return_spmf intro!: rel_spmf_bind_reflI rel_spmf_bindI[OF bisim_bad])
hence "spmf game2_c (True, False) = spmf game2_d (True, False)"
unfolding spmf_rel_eq by(subst (1 2) spmf_map_restrict[symmetric]) simp
ultimately have game2c_2d: "¦spmf (map_spmf fst game2_c) True - spmf (map_spmf fst game2_d) True¦ ≤ spmf (map_spmf snd game2_c) True"
apply(subst (1 2) spmf_conv_measure_spmf)
apply(intro identical_until_bad)
apply(simp_all add: spmf.map_id[unfolded id_def] spmf_conv_measure_spmf)
done
{ fix cipher σ and challenge :: plain and s
have "card (nlists UNIV len ∩ (λx. x = challenge) -` {True}) ≤ card {challenge}"
by(rule card_mono) auto
then have "spmf (map_spmf (snd ∘ snd) (exec_gpv (rf_encrypt_bad challenge) (𝒜2 cipher σ) (s, False))) True ≤ (1 / 2 ^ len) * q2"
by(intro oi_True.interaction_bounded_by_exec_gpv_bad[OF q2])(simp_all add: rf_encrypt_bad_def o_def split_beta map_spmf_conv_bind_spmf[symmetric] spmf_map measure_spmf_of_set field_simps card_nlists)
hence "(∫⇧+ x. ennreal (indicator {True} x) ∂measure_spmf (map_spmf (snd ∘ snd) (exec_gpv (rf_encrypt_bad challenge) (𝒜2 cipher σ) (s, False)))) ≤ (1 / 2 ^ len) * q2"
by(simp only: ennreal_indicator nn_integral_indicator sets_measure_spmf sets_count_space Pow_UNIV UNIV_I emeasure_spmf_single) simp }
then have "spmf (map_spmf snd game2_d) True ≤
∫⇧+ (r :: plain). ∫⇧+ (((p0, p1), σ), s). (if valid_plain p0 ∧ valid_plain p1 then
∫⇧+ b . ∫⇧+ (pad :: plain). q2 / 2 ^ len ∂measure_spmf (spmf_of_set (nlists UNIV len)) ∂measure_spmf coin_spmf
else 0)
∂measure_spmf (exec_gpv rf_encrypt 𝒜1 Map.empty) ∂measure_spmf (spmf_of_set (nlists UNIV len))"
unfolding game2_d_def
by(simp add: ennreal_spmf_bind o_def split_def Let_def if_distribs if_distrib[where f="λx. ennreal (spmf x _)"] indicator_single_Some nn_integral_mono if_mono_cong del: nn_integral_const cong: if_cong)
also have "… ≤ ∫⇧+ (r :: plain). ∫⇧+ (((p0, p1), σ), s). (if valid_plain p0 ∧ valid_plain p1 then ennreal (q2 / 2 ^ len) else q2 / 2 ^ len)
∂measure_spmf (exec_gpv rf_encrypt 𝒜1 Map.empty) ∂measure_spmf (spmf_of_set (nlists UNIV len))"
unfolding split_def
by(intro nn_integral_mono if_mono_cong)(auto simp add: measure_spmf.emeasure_eq_measure)
also have "… ≤ q2 / 2 ^ len" by(simp add: split_def weight1 measure_spmf.emeasure_eq_measure)
finally have game2_d_bad: "spmf (map_spmf snd game2_d) True ≤ q2 / 2 ^ len" by simp
define game3 where "game3 = do {
(((p0, p1), σ), s1) ← exec_gpv rf_encrypt 𝒜1 Map.empty;
if valid_plain p0 ∧ valid_plain p1 then do {
b ← coin_spmf;
let pb = (if b then p0 else p1);
r ← spmf_of_set (nlists UNIV len);
pad ← spmf_of_set (nlists UNIV len);
let cipher = (r, xor_list pb pad);
(b', s2) ← exec_gpv rf_encrypt (𝒜2 cipher σ) s1;
return_spmf (b' = b)
} else coin_spmf
}"
have bisim2d_3: "⋀cipher σ s r. rel_spmf (λ(x, _) (y, _). x = y)
(exec_gpv (rf_encrypt_bad r) (𝒜2 cipher σ) (s, False))
(exec_gpv rf_encrypt (𝒜2 cipher σ) s)"
by(rule exec_gpv_oracle_bisim[where X="λ(s1, _) s2. s1 = s2"])(auto simp add: rf_encrypt_bad_def rf_encrypt_def intro!: rel_spmf_bind_reflI)
have game2d_3: "rel_spmf (=) (map_spmf fst game2_d) game3"
unfolding game2_d_def game3_def Let_def including monad_normalisation
by(clarsimp simp add: o_def split_def if_distribs cong: if_cong intro!: rel_spmf_bind_reflI rel_spmf_bindI[OF bisim2d_3])
have "¦spmf game2 True - 1 / 2¦ ≤
¦spmf (map_spmf fst game2_a) True - spmf (map_spmf fst game2_b) True¦ + ¦spmf (map_spmf fst game2_b) True - 1 / 2¦"
unfolding game2_2a by(rule abs_diff_triangle_ineq2)
also have "… ≤ q1 / 2 ^ len + ¦spmf (map_spmf fst game2_b) True - 1 / 2¦"
using game2a_2b game2a_bad_bound unfolding game2a_bad by(intro add_right_mono) simp
also have "¦spmf (map_spmf fst game2_b) True - 1 / 2¦ ≤
¦spmf (map_spmf fst game2_c) True - spmf (map_spmf fst game2_d) True¦ + ¦spmf (map_spmf fst game2_d) True - 1 / 2¦"
unfolding game2b_c by(rule abs_diff_triangle_ineq2)
also (add_left_mono_trans) have "… ≤ q2 / 2 ^ len + ¦spmf (map_spmf fst game2_d) True - 1 / 2¦"
using game2c_2d game2_d_bad unfolding game2c_2d_bad by(intro add_right_mono) simp
finally (add_left_mono_trans)
have game2: "¦spmf game2 True - 1 / 2¦ ≤ q1 / 2 ^ len + q2 / 2 ^ len + ¦spmf game3 True - 1 / 2¦"
using game2d_3 by(simp add: field_simps spmf_rel_eq)
have "game3 = do {
(((p0, p1), σ), s1) ← exec_gpv rf_encrypt 𝒜1 Map.empty;
if valid_plain p0 ∧ valid_plain p1 then do {
b ← coin_spmf;
let pb = (if b then p0 else p1);
r ← spmf_of_set (nlists UNIV len);
pad ← map_spmf (xor_list pb) (spmf_of_set (nlists UNIV len));
let cipher = (r, xor_list pb pad);
(b', s2) ← exec_gpv rf_encrypt (𝒜2 cipher σ) s1;
return_spmf (b' = b)
} else coin_spmf
}"
by(simp add: valid_plain_def game3_def Let_def one_time_pad del: bind_map_spmf map_spmf_of_set_inj_on cong: bind_spmf_cong_simp if_cong split: if_split)
also have "… = do {
(((p0, p1), σ), s1) ← exec_gpv rf_encrypt 𝒜1 Map.empty;
if valid_plain p0 ∧ valid_plain p1 then do {
b ← coin_spmf;
let pb = (if b then p0 else p1);
r ← spmf_of_set (nlists UNIV len);
pad ← spmf_of_set (nlists UNIV len);
let cipher = (r, pad);
(b', _) ← exec_gpv rf_encrypt (𝒜2 cipher σ) s1;
return_spmf (b' = b)
} else coin_spmf
}"
by(simp add: game3_def Let_def valid_plain_def in_nlists_UNIV cong: bind_spmf_cong_simp if_cong split: if_split)
also have "… = do {
(((p0, p1), σ), s1) ← exec_gpv rf_encrypt 𝒜1 Map.empty;
if valid_plain p0 ∧ valid_plain p1 then do {
r ← spmf_of_set (nlists UNIV len);
pad ← spmf_of_set (nlists UNIV len);
let cipher = (r, pad);
(b', _) ← exec_gpv rf_encrypt (𝒜2 cipher σ) s1;
map_spmf ((=) b') coin_spmf
} else coin_spmf
}"
including monad_normalisation by(simp add: map_spmf_conv_bind_spmf split_def Let_def)
also have "… = coin_spmf"
by(simp add: map_eq_const_coin_spmf Let_def split_def weight2 weight1)
finally have game3: "game3 = coin_spmf" .
have "ind_cpa.advantage 𝒜 ≤ prf.advantage (prf_adversary 𝒜) + ¦spmf (prf.game_1 (prf_adversary 𝒜)) True - 1 / 2¦"
unfolding ind_cpa.advantage_def prf.advantage_def ind_cpa_0[unfolded spmf_rel_eq]
by(rule abs_diff_triangle_ineq2)
also have "¦spmf (prf.game_1 (prf_adversary 𝒜)) True - 1 / 2¦ ≤ q1 / 2 ^ len + q2 / 2 ^ len"
using game1_2 game2 game3 by(simp add: spmf_of_set)
also have "… = (q1 + q2) / 2 ^ len" by(simp add: field_simps)
also have "… ≤ q / 2 ^ len" using ‹q1 + q2 ≤ q› by(simp add: divide_right_mono)
finally show ?thesis by(simp add: field_simps)
qed
lemma interaction_bounded_prf_adversary:
fixes q :: nat
assumes "ind_cpa.ibounded_by 𝒜 q"
shows "prf.ibounded_by (prf_adversary 𝒜) (1 + q)"
proof -
fix η
from assms have "ind_cpa.ibounded_by 𝒜 q" by blast
then obtain q1 q2 where q: "q1 + q2 ≤ q"
and [interaction_bound]: "interaction_any_bounded_by (fst 𝒜) q1"
"⋀x σ. interaction_any_bounded_by (snd 𝒜 x σ) q2"
unfolding ind_cpa.ibounded_by_def by(auto simp add: split_beta iadd_le_enat_iff)
show "prf.ibounded_by (prf_adversary 𝒜) (1 + q)" using q
apply (simp only: prf_adversary_def Let_def split_def)
apply -
apply interaction_bound
apply (auto simp add: iadd_SUP_le_iff SUP_le_iff add.assoc [symmetric] one_enat_def cong del: image_cong_simp cong add: SUP_cong_simp)
done
qed
lemma lossless_prf_adversary: "ind_cpa.lossless 𝒜 ⟹ prf.lossless (prf_adversary 𝒜)"
by(fastforce simp add: prf_adversary_def Let_def split_def ind_cpa.lossless_def intro: lossless_inline)
end
locale otp_η =
fixes f :: "security ⇒ key ⇒ bool list ⇒ bool list"
and len :: "security ⇒ nat"
assumes length_f: "⋀η xs ys. ⟦ length xs = len η; length ys = len η ⟧ ⟹ length (f η xs ys) = len η"
and negligible_len [negligible_intros]: "negligible (λη. 1 / 2 ^ (len η))"
begin
interpretation otp "f η" "len η" for η by(unfold_locales)(rule length_f)
interpretation ind_cpa: ind_cpa "key_gen η" "encrypt η" "decrypt η" "valid_plain η" for η .
interpretation "prf": "prf" "key_gen η" "f η" "spmf_of_set (nlists UNIV (len η))" for η .
lemma prf_encrypt_secure_for:
assumes [negligible_intros]: "negligible (λη. prf.advantage η (prf_adversary η (𝒜 η)))"
and q: "⋀η. ind_cpa.ibounded_by (𝒜 η) (q η)" and [negligible_intros]: "polynomial q"
and lossless: "⋀η. ind_cpa.lossless (𝒜 η)"
shows "negligible (λη. ind_cpa.advantage η (𝒜 η))"
proof(rule negligible_mono)
show "negligible (λη. prf.advantage η (prf_adversary η (𝒜 η)) + q η / 2 ^ len η)"
by(intro negligible_intros)
{ fix η
from ‹ind_cpa.ibounded_by _ _› have "ind_cpa.ibounded_by (𝒜 η) (q η)" by blast
moreover from lossless have "ind_cpa.lossless (𝒜 η)" by blast
hence "lossless_gpv ℐ_full (fst (𝒜 η))" "⋀cipher σ. lossless_gpv ℐ_full (snd (𝒜 η) cipher σ)"
by(auto simp add: ind_cpa.lossless_def)
ultimately have "ind_cpa.advantage η (𝒜 η) ≤ prf.advantage η (prf_adversary η (𝒜 η)) + q η / 2 ^ len η"
by(rule prf_encrypt_advantage) }
hence "eventually (λη. ¦ind_cpa.advantage η (𝒜 η)¦ ≤ 1 * ¦prf.advantage η (prf_adversary η (𝒜 η)) + q η / 2 ^ len η¦) at_top"
by(simp add: always_eventually ind_cpa.advantage_nonneg prf.advantage_nonneg)
then show "(λη. ind_cpa.advantage η (𝒜 η)) ∈ O(λη. prf.advantage η (prf_adversary η (𝒜 η)) + q η / 2 ^ len η)"
by(intro bigoI[where c=1]) simp
qed
end
end
Theory PRF_UPF_IND_CCA
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"
by(simp add: key_gen_def prf_key_gen_lossless upf_key_gen_lossless)
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)"
by(simp add: intercept_upf_dec_def split_beta)
lemma lossless_intercept_upf [simp]: "lossless_gpv (ℐ_full ⊕⇩ℐ ℐ_full) (intercept_upf k b LD x)"
by(cases x)(simp_all add: intercept_upf_def)
lemma results_gpv_intercept_upf [simp]: "results_gpv (ℐ_full ⊕⇩ℐ ℐ_full) (intercept_upf k b LD x) ⊆ responses_ℐ (ℐ_full ⊕⇩ℐ ℐ_full) x × UNIV"
by(cases x)(auto simp add: intercept_upf_def)
definition reduction_upf :: "(bitstring, 'hash cipher_text) ind_cca.adversary
⇒ (bitstring, 'hash) UPF.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)))"
for key L bad x' c' t' by(simp add: oracle_decrypt0'_def)
have lossless_oracle_decrypt0' [simp]: "lossless_spmf (oracle_decrypt0' k Lbad c)" for k Lbad c
by(simp add: oracle_decrypt0'_def split_def)
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))"
for key L bad x' c' t' by(simp add: oracle_decrypt1'_def)
have lossless_oracle_decrypt1' [simp]: "lossless_spmf (oracle_decrypt1' k Lbad c)" for k Lbad c
by(simp add: oracle_decrypt1'_def split_def)
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]
by(simp add: rel_spmf_return_spmf1 rel_fun_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]
by (simp add: rel_spmf_return_spmf1 rel_fun_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
have *: "rel_spmf (λ(b'1, (bad1, L1)) (b'2, (bad2, L2)). bad1 = bad2 ∧ (¬ bad2 ⟶ b'1 = b'2))
(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
by (cases k; rule exec_gpv_oracle_bisim_bad[where X="(=)" and ?bad1.0=fst and ?bad2.0=fst and ℐ = "ℐ_full ⊕⇩ℐ ℐ_full"])
(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)
have "¦measure (measure_spmf (?game1' 𝒜)) {(b, bad). b} - measure (measure_spmf (?game0' 𝒜)) {(b, bad). b}¦
≤ measure (measure_spmf (?game1' 𝒜)) {(b, bad). bad}"
by (rule fundamental_lemma[where ?bad2.0=snd])(auto intro!: rel_spmf_bind_reflI rel_spmf_bindI[OF *] simp add: game01'_def)
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)
apply(clarsimp simp add: set_spmf_of_set_finite[OF prf_domain_finite]
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
then show ?thesis including monad_normalisation
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
by (auto simp add: spmf_conv_measure_spmf measure_map_spmf vimage_def fst_def UPF.advantage_def)
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)"
by(simp add: oracle_decrypt2_def split_def)
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
:: "(bitstring, 'hash cipher_text) ind_cca.adversary ⇒ (bitstring, bitstring) PRF.adversary"
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]
by(auto simp add: rel_fun_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
ultimately show ?thesis by(simp add: PRF.advantage_def)
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);
return_spmf (b = b', bad)
}"
lemma round_3:
assumes "lossless_gpv (ℐ_full ⊕⇩ℐ ℐ_full) 𝒜"
shows "¦measure (measure_spmf (game3 𝒜)) {(b, bad). b} - spmf (game2 𝒜) True¦
≤ measure (measure_spmf (game3 𝒜)) {(b, bad). bad}"
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);
return_spmf (b = b', bad)})"
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"
by(auto simp add: rel_fun_def oracle_decrypt2_def)
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
moreover have *: "rel_spmf (λ(b'1, bad1, L1) (b'2, bad2, L2). (bad1 ⟷ bad2) ∧ (¬ bad2 ⟶ b'1 ⟷ b'2))
(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(rule exec_gpv_oracle_bisim_bad[where X="(=)" and X_bad = "λ_ _. True" and ?bad1.0=fst and ?bad2.0=fst and ℐ="ℐ_full ⊕⇩ℐ ℐ_full"])
apply(simp_all add: assms)
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}¦ ≤
measure (measure_spmf (game3 𝒜)) {(b, bad). bad}"
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
unfolding game3_def game4_def including monad_normalisation
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
lemma game3_bad:
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
proof(rule callee_invariant_on.interaction_bounded_by'_exec_gpv_bad_count)
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'
by(cases x)(simp_all add: oracle_decrypt2_def)
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
with bad
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
thus ?thesis using bad
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"
shows "ind_cca.advantage 𝒜 ≤
PRF.advantage (reduction_prf 𝒜) + UPF.advantage (reduction_upf 𝒜) +
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¦"
(is "_ ≤ ?round1 + ?rest") using abs_triangle_ineq by(simp add: ind_cca.advantage_def)
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
also have "?round3 ≤ measure (measure_spmf (game3 𝒜)) {(b, bad). bad}"
using round_3[OF lossless] .
also have "… ≤ q / card prf_domain * q" using bound by(rule game3_bad)
also have "measure (measure_spmf (game3 𝒜)) {(b, bad). b} = spmf coin_spmf True"
using round_4[OF lossless, symmetric]
by(simp add: spmf_conv_measure_spmf measure_map_spmf vimage_def fst_def)
also have "¦… - 1 / 2¦ = 0" by(simp add: spmf_of_set)
finally show ?thesis by(simp)
qed
theorem security1:
assumes lossless: "lossless_gpv (ℐ_full