Theory Kyber_gpv_IND_CPA
theory Kyber_gpv_IND_CPA
imports "Game_Based_Crypto.CryptHOL_Tutorial"
Correct_new
begin
unbundle %invisible lifting_syntax
declare %invisible [[names_short]]
section ‹IND-CPA Security of Kyber›
text ‹The IND-CPA security of the Kyber PKE is based on the module-LWE.
It takes the length ‹len_plain› of the plaintexts in the security games as an input.
Note that the security proof is for the uncompressed scheme only! That means that the output
of the key generation is not compressed and the input of the encryption is not
decompressed.
The compression/decompression would entail that the decompression of the value ‹t› from the
key generation is not distributed uniformly at random any more (because of the compression error).
This prohibits the second reduction to module-LWE.
In order to avoid this, the compression and decompression in key generation and encryption
have been omitted from the second round of the NIST standardisation process onwards.›
locale kyber_new_security = kyber_cor_new _ _ _ _ _ _ "TYPE('a::qr_spec)" "TYPE('k::finite)" +
ro: random_oracle len_plain
for len_plain :: nat +
fixes type_a :: "('a :: qr_spec) itself"
and type_k :: "('k ::finite) itself"
begin
text ‹The given plaintext as a bitstring needs to be converted to an element in $R_q$.
The bitstring is respresented as an integer value by interpreting the bitstring as a binary number.
The integer is then converted to an element in $R_q$ by the function ‹to_module›.
Conversely, the bitstring representation can by extracted from the coefficient of the
element in $R_q$.›
definition bitstring_to_int:
"bitstring_to_int msg = (∑i<length msg. if msg!i then 2^i else 0)"
definition plain_to_msg :: "bitstring ⇒ 'a qr" where
"plain_to_msg msg = to_module (bitstring_to_int msg)"
definition msg_to_plain :: "'a qr ⇒ bitstring" where
"msg_to_plain msg = map (λi. i=0) (coeffs (of_qr msg))"
subsection ‹Instantiation of ‹ind_cpa› Locale with Kyber›
text ‹We only look at the uncompressed version of Kyber.
As the IND-CPA locale works over the generative probabilistic values type ‹gpv›,
we need to lift our definitions to ‹gpv›'s.›
text ‹The lifting of the key generation:›
definition gpv_key_gen where
"gpv_key_gen = lift_spmf (spmf_of_pmf pmf_key_gen)"
lemma spmf_pmf_of_set_UNIV:
"spmf_of_set (UNIV:: (('a qr,'k) vec,'k) vec set) =
spmf_of_pmf (pmf_of_set (UNIV:: (('a qr,'k) vec,'k) vec set))"
unfolding spmf_of_set_def by simp
lemma key_gen:
"gpv_key_gen = lift_spmf ( do {
A ← spmf_of_set (UNIV:: (('a qr, 'k) vec, 'k) vec set);
s ← spmf_of_pmf mlwe.beta_vec;
e ← spmf_of_pmf mlwe.beta_vec;
let t = key_gen_new A s e;
return_spmf ((A, t),s)
})"
unfolding gpv_key_gen_def pmf_key_gen_def unfolding spmf_pmf_of_set_UNIV
unfolding bind_spmf_of_pmf by (auto simp add: spmf_of_pmf_bind)
text ‹The lifting of the encryption:›
definition gpv_encrypt ::
"('a qr, 'k) pk ⇒ plain ⇒ (('a qr, 'k) vec × 'a qr, 'b, 'c) gpv" where
"gpv_encrypt pk m = lift_spmf (spmf_of_pmf (pmf_encrypt pk (plain_to_msg m)))"
text ‹The lifting of the decryption:›
definition gpv_decrypt ::
"('a qr, 'k) sk ⇒ ('a qr, 'k) cipher ⇒ (plain, ('a qr,'k) vec, bitstring) gpv" where
"gpv_decrypt sk cipher = lift_spmf (do {
let msg' = decrypt (fst cipher) (snd cipher) sk du dv ;
return_spmf (msg_to_plain (msg'))
})"
text ‹In order to verify that the plaintexts given by the adversary in the IND-CPA security game
have indeed the same length, we define the test ‹valid_plains›.›
definition valid_plains :: "plain ⇒ plain ⇒ bool" where
"valid_plains msg1 msg2 ⟷ (length msg1 = len_plain ∧ length msg2 = len_plain)"
text ‹Now we can instantiate the IND-CPA locale with the lifted Kyber algorithms.›
sublocale ind_cpa: ind_cpa_pk "gpv_key_gen" "gpv_encrypt" "gpv_decrypt" valid_plains .
subsection ‹Reduction Functions›
text ‹Since we lifted the key generation and encryption functions to ‹gpv›'s, we need to show
that they are lossless, i.e., that they have no failure.›
lemma lossless_key_gen[simp]: "lossless_gpv ℐ_full gpv_key_gen"
unfolding gpv_key_gen_def by auto
lemma lossless_encrypt[simp]: "lossless_gpv ℐ_full (gpv_encrypt pk m)"
unfolding gpv_encrypt_def by auto
lemma lossless_decrypt[simp]: "lossless_gpv ℐ_full (gpv_decrypt sk cipher)"
unfolding gpv_decrypt_def by auto
lemma finite_UNIV_lossless_spmf_of_set:
assumes "finite (UNIV :: 'b set)"
shows "lossless_gpv ℐ_full (lift_spmf (spmf_of_set (UNIV :: 'b set)))"
using assms by simp
text ‹The reduction functions give the concrete reduction of a IND-CPA adversary to a
module-LWE adversary.
The first function is for the reduction in the key generation using $m=k$, whereas the
second reduction is used in the encryption with $m=k+1$ (using the option type).›
fun kyber_reduction1 ::
"(('a qr, 'k) pk, plain, ('a qr, 'k) cipher, ('a qr,'k) vec, bitstring, 'state) ind_cpa.adversary
⇒ ('a qr, 'k,'k) mlwe.adversary"
where
"kyber_reduction1 (𝒜⇩1, 𝒜⇩2) A t = do {
(((msg1, msg2), σ), s) ← exec_gpv ro.oracle (𝒜⇩1 (A, t)) ro.initial;
try_spmf (do {
_ :: unit ← assert_spmf (valid_plains msg1 msg2);
b ← coin_spmf;
(c, s1) ← exec_gpv ro.oracle (gpv_encrypt (A,t) (if b then msg1 else msg2)) s;
(b', s2) ← exec_gpv ro.oracle (𝒜⇩2 c σ) s1;
return_spmf (b' = b)
}) (coin_spmf)
}"
fun kyber_reduction2 ::
"(('a qr, 'k) pk, plain, ('a qr, 'k) cipher, ('a qr,'k) vec, bitstring, 'state) ind_cpa.adversary
⇒ ('a qr, 'k,'k option) mlwe.adversary"
where
"kyber_reduction2 (𝒜⇩1, 𝒜⇩2) A' t' = do {
let A = transpose (χ i. A' $ (Some i));
let t = A' $ None;
(((msg1, msg2), σ),s) ← exec_gpv ro.oracle (𝒜⇩1 (A, t)) ro.initial;
try_spmf (do {
_ :: unit ← assert_spmf (valid_plains msg1 msg2);
b ← coin_spmf;
let msg = (if b then msg1 else msg2);
let u = (χ i. t' $ (Some i));
let v = (t' $ None) + to_module (round((real_of_int q)/2)) * (plain_to_msg msg);
(b', s1) ← exec_gpv ro.oracle (𝒜⇩2 (compress_vec du u, compress_poly dv v) σ) s;
return_spmf (b'=b)
}) (coin_spmf)
}"
subsection ‹IND-CPA Security Proof›
text ‹The following theorem states that if the adversary against the IND-CPA game is lossless
(that is it does not act maliciously), then the advantage in the IND-CPA game can be bounded by
two advantages against the module-LWE game.
Under the module-LWE hardness assumption, the advantage against the module-LWE is negligible.
The proof proceeds in several steps, also called game-hops.
Initially, the IND-CPA game is considered. Then we gradually alter the games and show that
either the alteration has no effect on the resulting probabilities or we can bound the change
by an advantage against the module-LWE.
In the end, the game is a simple coin toss, which we know has probability $0.5$ to guess the
correct outcome.
Finally, we can estimate the advantage against IND-CPA using the game-hops found before,
and bounding it against the advantage against module-LWE.›
theorem concrete_security_kyber:
assumes lossless: "ind_cpa.lossless 𝒜"
shows "ind_cpa.advantage (ro.oracle, ro.initial) 𝒜 ≤
mlwe.advantage (kyber_reduction1 𝒜) + mlwe.advantage' (kyber_reduction2 𝒜)"
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
and [if_distribs] = if_distrib[where f="λx. try_spmf x _"]
if_distrib[where f="weight_spmf"]
if_distrib[where f="λr. scale_spmf r _"]
text ‹First of all, we can split the IND-CPA adversary ‹𝒜› into two parts, namely the adversary
who returns two messages ‹𝒜⇩1› and the adversary who returns a guess ‹𝒜⇩2›.›
obtain 𝒜⇩1 𝒜⇩2 where 𝒜 [simp]: "𝒜 = (𝒜⇩1, 𝒜⇩2)" by (cases "𝒜")
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 ‹The initial game ‹game⇩0› is an equivalent formulation of the IND-CPA game.›
define game⇩0 where
"game⇩0 = do {
A ← spmf_of_set (UNIV:: (('a qr, 'k) vec, 'k) vec set);
s ← spmf_of_pmf mlwe.beta_vec;
e ← spmf_of_pmf mlwe.beta_vec;
let pk = (A, A *v s + e);
b ← coin_spmf;
(((msg1, msg2), σ),s) ← exec_gpv ro.oracle (𝒜⇩1 pk) ro.initial;
if valid_plains msg1 msg2
then do {
(c, s1) ← exec_gpv ro.oracle (gpv_encrypt pk (if b then msg1 else msg2)) s;
(b', s2) ← exec_gpv ro.oracle (𝒜⇩2 c σ) s1;
return_spmf (b' = b)
}
else coin_spmf
}"
have ind_cpa_game_eq_game⇩0: "run_gpv ro.oracle (ind_cpa.game 𝒜) ro.initial = game⇩0"
proof -
have *: "bind_pmf pmf_key_gen (λx. return_spmf (x, ro.initial)) ⤜
(λx. f (fst (fst x)) (snd x)) =
spmf_of_set UNIV ⤜ (λA. bind_pmf mlwe.beta_vec (λs. bind_pmf mlwe.beta_vec
(λe. f (A, A *v s + e) ro.initial)))" for f
unfolding pmf_key_gen_def spmf_pmf_of_set_UNIV bind_spmf_of_pmf key_gen_new_def Let_def
by (simp add: bind_spmf_pmf_assoc bind_assoc_pmf bind_return_pmf)
show ?thesis using *[of "(λpk state. exec_gpv ro.oracle (𝒜⇩1 pk) state ⤜
(λxa. if valid_plains (fst (fst (fst xa))) (snd (fst (fst xa)))
then coin_spmf ⤜ (λxb. exec_gpv ro.oracle (gpv_encrypt pk
(if xb then fst (fst (fst xa)) else snd (fst (fst xa)))) (snd xa) ⤜
(λx. exec_gpv ro.oracle (𝒜⇩2 (fst x) (snd (fst xa))) (snd x) ⤜
(λx. return_spmf (fst x = xb))))
else coin_spmf))"]
unfolding 𝒜 ind_cpa.game.simps unfolding game⇩0_def gpv_key_gen_def
apply (simp add: split_def try_spmf_bind_spmf_lossless try_bind_assert_spmf key_gen_def Let_def
bind_commute_spmf[of coin_spmf] if_distrib_bind_spmf2
try_gpv_bind_lossless try_bind_assert_gpv lift_bind_spmf comp_def
if_distrib_exec_gpv exec_gpv_bind_lift_spmf exec_gpv_bind if_distrib_map_spmf
del: bind_spmf_const)
apply simp
done
qed
text ‹We define encapsulate the module-LWE instance for generating a public key $t$ in the
key generation by the function ‹is_pk›. The game ‹game⇩1› depends on a function that generates a
public key.
Indeed, ‹game⇩0› corresponds to ‹game⇩1 is_pk›.›
define is_pk :: "('a qr,'k) pk spmf" where "is_pk = do {
A ← spmf_of_set (UNIV:: (('a qr, 'k) vec, 'k) vec set);
s ← spmf_of_pmf mlwe.beta_vec;
e ← spmf_of_pmf mlwe.beta_vec;
return_spmf (A, A *v s + e)}"
define game⇩1 where
"game⇩1 f = do {
pk ← f;
b ← coin_spmf;
(((msg1, msg2), σ), s) ← exec_gpv ro.oracle (𝒜⇩1 pk) ro.initial;
if valid_plains msg1 msg2
then do {
(c, s1) ← exec_gpv ro.oracle (gpv_encrypt pk (if b then msg1 else msg2)) s;
(b', s2) ← exec_gpv ro.oracle (𝒜⇩2 c σ) s1;
return_spmf (b' = b)
}
else coin_spmf
}" for f :: "('a qr,'k) pk spmf"
have game⇩0_eq_game⇩1_is_pk: "game⇩0 = game⇩1 is_pk"
by (simp add: game⇩1_def game⇩0_def is_pk_def Let_def o_def split_def if_distrib_map_spmf
bind_spmf_pmf_assoc bind_assoc_pmf bind_return_pmf)
text ‹In contrast to the generation of the public key as a module-LWE instance as in ‹is_pk›,
the function ‹rand_pk› generates a uniformly random public key.
We can now use this to do a reduction step to a module-LWE advantage.
‹game⇩1 is_pk› corresponds to a module-LWE game with module-LWE instance.
‹game⇩1 rand_pk› corresponds to a module-LWE game with random instance.
The difference of their probabilities can then be bounded by the module-LWE advantage in
lemma ‹reduction1›.
The reduction function used in this case is ‹kyber_reduction1›.›
define rand_pk :: "('a qr,'k) pk spmf" where
"rand_pk = bind_spmf (spmf_of_set UNIV) (λA. spmf_of_set UNIV ⤜ (λt. return_spmf (A, t)))"
have red11: "game⇩1 is_pk = mlwe.game (kyber_reduction1 𝒜)"
proof -
have "spmf_of_set UNIV ⤜ (λy. spmf_of_pmf mlwe.beta_vec ⤜ (λya. spmf_of_pmf mlwe.beta_vec ⤜
(λyb. exec_gpv ro.oracle (𝒜⇩1 (y, y *v ya + yb)) ro.initial ⤜
(λyc. if valid_plains (fst (fst (fst yc))) (snd (fst (fst yc)))
then coin_spmf ⤜
(λb. exec_gpv ro.oracle (gpv_encrypt (y, y *v ya + yb)
(if b then fst (fst (fst yc)) else snd (fst (fst yc)))) (snd yc) ⤜
(λp. exec_gpv ro.oracle (𝒜⇩2 (fst p) (snd (fst yc))) (snd p) ⤜
(λp. return_spmf (fst p = b))))
else coin_spmf)))) =
spmf_of_set UNIV ⤜(λA. spmf_of_pmf mlwe.beta_vec ⤜(λs. spmf_of_pmf mlwe.beta_vec ⤜
(λe. exec_gpv ro.oracle (𝒜⇩1 (A, A *v s + e)) ro.initial ⤜
(λp. if valid_plains (fst (fst (fst p))) (snd (fst (fst p)))
then coin_spmf ⤜
(λx. TRY exec_gpv ro.oracle (gpv_encrypt (A, A *v s + e)
(if x then fst (fst (fst p)) else snd (fst (fst p)))) (snd p) ⤜
(λpa. exec_gpv ro.oracle (𝒜⇩2 (fst pa) (snd (fst p))) (snd pa) ⤜
(λp. return_spmf (fst p = x))) ELSE coin_spmf)
else coin_spmf))))"
apply (subst try_spmf_bind_spmf_lossless)
subgoal by (subst lossless_exec_gpv, auto)
subgoal apply (subst try_spmf_bind_spmf_lossless)
subgoal by (subst lossless_exec_gpv, auto)
subgoal by (auto simp add: bind_commute_spmf
[of "spmf_of_set (UNIV :: ('a qr, 'k option) vec set)"])
done
done
then show ?thesis unfolding mlwe.game_def game⇩1_def is_pk_def
by (simp add: try_bind_assert_spmf bind_commute_spmf[of "coin_spmf"] split_def
if_distrib_bind_spmf2 try_spmf_bind_spmf_lossless
bind_spmf_pmf_assoc bind_assoc_pmf bind_return_pmf del: bind_spmf_const) simp
qed
have red12: "game⇩1 rand_pk = mlwe.game_random (kyber_reduction1 𝒜)"
proof -
have "spmf_of_set UNIV ⤜ (λy. spmf_of_set UNIV ⤜
(λya. exec_gpv ro.oracle (𝒜⇩1 (y, ya)) ro.initial ⤜
(λyb. if valid_plains (fst (fst (fst yb))) (snd (fst (fst yb)))
then coin_spmf ⤜
(λb. exec_gpv ro.oracle (gpv_encrypt (y, ya)
(if b then fst (fst (fst yb)) else snd (fst (fst yb)))) (snd yb) ⤜
(λp. exec_gpv ro.oracle (𝒜⇩2 (fst p) (snd (fst yb))) (snd p) ⤜
(λp. return_spmf (fst p = b))))
else coin_spmf))) =
spmf_of_set UNIV ⤜ (λA. spmf_of_set UNIV ⤜
(λb. exec_gpv ro.oracle (𝒜⇩1 (A, b)) ro.initial ⤜
(λp. if valid_plains (fst (fst (fst p))) (snd (fst (fst p)))
then coin_spmf ⤜
(λx. TRY exec_gpv ro.oracle (gpv_encrypt (A, b)
(if x then fst (fst (fst p)) else snd (fst (fst p)))) (snd p) ⤜
(λpa. exec_gpv ro.oracle (𝒜⇩2 (fst pa) (snd (fst p))) (snd pa) ⤜
(λp. return_spmf (fst p = x))) ELSE coin_spmf)
else coin_spmf)))"
apply (subst try_spmf_bind_spmf_lossless)
subgoal by (subst lossless_exec_gpv, auto)
subgoal apply (subst try_spmf_bind_spmf_lossless)
subgoal by (subst lossless_exec_gpv, auto)
subgoal by (auto simp add: bind_commute_spmf
[of "spmf_of_set (UNIV :: ('a qr, 'k option) vec set)"])
done
done
then show ?thesis unfolding mlwe.game_random_def game⇩1_def rand_pk_def
by (simp add: try_bind_assert_spmf bind_commute_spmf[of "coin_spmf"] split_def
if_distrib_bind_spmf2 try_spmf_bind_spmf_lossless
bind_spmf_pmf_assoc bind_assoc_pmf bind_return_pmf
del: bind_spmf_const) simp
qed
have reduction1: "¦spmf (game⇩1 is_pk) True - spmf (game⇩1 rand_pk) True¦ ≤
mlwe.advantage (kyber_reduction1 𝒜)"
unfolding mlwe.advantage_def red11 red12 by auto
text ‹Again, we rewrite our current game such that:
\begin{itemize}
\item the generation of the public key is outsourced to a sampling function ‹?sample›
\item the encryption is outsourced to a input function
\item ‹is_encrypt› is the appropriate input function for the encryption
\item ‹rand_encrypt› is the appropriate input function for a uniformly random $u$ and $v'$
\end{itemize}
Note that the addition of the message is not changed yet.›
define is_encrypt where
"is_encrypt A t msg = do {
r ← spmf_of_pmf mlwe.beta_vec;
e1 ← spmf_of_pmf mlwe.beta_vec;
e2 ← spmf_of_pmf mlwe.beta;
let (u,v) = ((((transpose A) *v r + e1), (scalar_product t r + e2 +
to_module (round((real_of_int q)/2)) * (plain_to_msg msg))));
return_spmf (compress_vec du u, compress_poly dv v)
}" for A ::"(('a qr,'k) vec,'k)vec" and t :: "('a qr,'k) vec" and msg :: bitstring
define rand_encrypt where
"rand_encrypt A t msg = do {
u ← spmf_of_set (UNIV :: ('a qr,'k) vec set);
v ← spmf_of_set (UNIV :: 'a qr set);
let v' = v + to_module (round((real_of_int q)/2)) * (plain_to_msg msg);
return_spmf (compress_vec du u, compress_poly dv v')
}" for A ::"(('a qr,'k) vec,'k)vec" and t :: "('a qr,'k) vec" and msg :: bitstring
let ?sample = "λf. bind_spmf (spmf_of_set (UNIV:: (('a qr, 'k) vec, 'k) vec set))
(λA. bind_spmf (spmf_of_set (UNIV:: ('a qr, 'k) vec set)) (f A))"
define game⇩2 where
"game⇩2 f A t = bind_spmf coin_spmf
(λb. bind_spmf (exec_gpv ro.oracle (𝒜⇩1 (A, t)) ro.initial)
(λ(((msg1, msg2), σ), s).
if valid_plains msg1 msg2
then let msg = if b then msg1 else msg2
in bind_spmf (f A t msg)
(λc. bind_spmf (exec_gpv ro.oracle (𝒜⇩2 c σ) s)
(λ(b', s1). return_spmf (b' = b)))
else coin_spmf))"
for f and A :: "(('a qr, 'k) vec, 'k) vec" and t :: "('a qr, 'k) vec"
text ‹Then ‹game⇩1 rand_encrypt› is the same as sampling via ‹?sample› and ‹game⇩2 is_encrypt›.›
have game⇩1_rand_pk_eq_game⇩2_is_encrypt: "game⇩1 rand_pk = ?sample (game⇩2 is_encrypt)"
unfolding game⇩1_def rand_pk_def game⇩2_def is_encrypt_def
by (simp add: game⇩1_def game⇩2_def rand_pk_def is_encrypt_def gpv_encrypt_def
encrypt_new_def pmf_encrypt_def Let_def o_def split_def if_distrib_map_spmf
bind_spmf_pmf_assoc bind_assoc_pmf bind_return_pmf)
text ‹To make the reduction work, we need to rewrite ‹is_encrypt› and ‹rand_encrypt› such that
$u$ and $v$ are in one vector only (since both need to be multiplied with $r$, thus we cannot
split the module-LWE instances). This can be done using the option type to allow for one more
index in the vector over the option type.›
define is_encrypt1 where
"is_encrypt1 A t msg = do {
r ← spmf_of_pmf mlwe.beta_vec;
e1 ← spmf_of_pmf mlwe.beta_vec;
e2 ← spmf_of_pmf mlwe.beta;
let (e :: ('a qr, 'k option) vec) = (χ i. if i= None then e2 else e1 $ (the i));
let (A' :: (('a qr,'k) vec, 'k option) vec) =
(χ i. if i = None then t else (transpose A) $ (the i));
let c = A' *v r + e;
let (u :: ('a qr, 'k) vec) = (χ i. (c $ (Some i)));
let (v :: 'a qr) = (c $ None +
to_module (round((real_of_int q)/2)) * (plain_to_msg msg));
return_spmf (compress_vec du u, compress_poly dv v)
}" for A :: "(('a qr, 'k) vec, 'k) vec" and t :: "('a qr,'k) vec" and msg :: bitstring
define rand_encrypt1 where
"rand_encrypt1 A t msg = do {
u' ← spmf_of_set (UNIV :: ('a qr,'k) vec set);
v' ← spmf_of_set (UNIV :: 'a qr set);
let (v :: 'a qr) = (v' +
to_module (round((real_of_int q)/2)) * (plain_to_msg msg));
return_spmf (compress_vec du u', compress_poly dv v)
}" for A ::"(('a qr,'k) vec,'k)vec" and t :: "('a qr,'k) vec" and msg :: bitstring
text ‹Indeed, these functions are the same as the previously defined ‹is_encrypt› and
‹rand_encrypt›.›
have is_encrypt1: "is_encrypt A t msg = is_encrypt1 A t msg" for A t msg
unfolding is_encrypt_def is_encrypt1_def Let_def
by (simp add: split_def plus_vec_def matrix_vector_mult_def scalar_product_def)
have rand_encrypt1: "rand_encrypt A t msg = rand_encrypt1 A t msg" for A t msg
unfolding rand_encrypt_def rand_encrypt1_def Let_def by simp
text ‹We also need to rewrite ‹game⇩2› to work over the option type, i.e., that $A$ and $t$ are
put in one matix $A'$. Then, ‹is_encrypt'› is an adaption to ‹is_encrypt› working with $A'$
instead of $a$ and $t$ separately.›
define game⇩3 where
"game⇩3 f = do {
b ← coin_spmf;
A' ← spmf_of_set (UNIV :: (('a qr,'k) vec, 'k option) vec set);
let A = transpose (vec_lambda (λ i. vec_nth A' (Some i)));
let t = vec_nth A' None;
(((msg1, msg2), σ),s) ← exec_gpv ro.oracle (𝒜⇩1 (A,t)) ro.initial;
if valid_plains msg1 msg2
then do {
let msg = (if b then msg1 else msg2);
c ← f A';
let (u :: ('a qr, 'k) vec) = vec_lambda (λ i. (vec_nth c (Some i)));
let (v :: 'a qr) = (vec_nth c None +
to_module (round((real_of_int q)/2)) * (plain_to_msg msg));
(b', s1) ← exec_gpv ro.oracle (𝒜⇩2 (compress_vec du u, compress_poly dv v) σ) s;
return_spmf (b' = b)
}
else coin_spmf
}" for f
define is_encrypt' where
"is_encrypt' A' = bind_spmf (spmf_of_pmf mlwe.beta_vec)
(λr. bind_spmf (mlwe.beta_vec')
(λe. return_spmf (A' *v r + e)))" for A' ::"(('a qr,'k) vec,'k option) vec"
text ‹We can write the distribution of the error and the public key as one draw from a
probability distribution over the option type.
We need this in order to show ‹?sample (game⇩2 is_encrypt) = game⇩3 (is_encrypt')›.
This corresponds to the module-LWE instance in the module-LWE advantage.›
have e_distrib: "do {
e1 ← spmf_of_pmf mlwe.beta_vec;
e2 ← spmf_of_pmf mlwe.beta;
let (e' :: ('a qr, 'k option) vec) =
(χ i. if i = None then e2 else vec_nth e1 (the i));
return_spmf e'
} = mlwe.beta_vec'"
unfolding mlwe.beta_vec' mlwe.beta_vec_def replicate_spmf_def
by (simp add: bind_commute_pmf[of "mlwe.beta"] bind_assoc_pmf bind_pmf_return_spmf
bind_return_pmf)
have pk_distrib: "do {
A ← spmf_of_set (UNIV);
t ← spmf_of_set (UNIV);
let (A' :: (('a qr,'k) vec, 'k option) vec) =
(χ i. if i = None then t else transpose A $ (the i));
return_spmf A'} =
spmf_of_set (UNIV)"
proof (intro spmf_eqI, goal_cases)
case (1 A')
let ?P = "(λ (A,t). (χ i. if i = None then t else transpose A $ (the i)))
:: ((('a qr, 'k) vec, 'k) vec × ('a qr, 'k) vec) ⇒ (('a qr, 'k) vec, 'k option) vec"
define a where "a = transpose (χ i. vec_nth A' (Some i))"
define b where "b = A' $ None"
have "(χ i. if i = None then b else transpose a $ the i) = A'"
unfolding a_def b_def
by (smt (verit, ccfv_SIG) Cart_lambda_cong Option.option.collapse
transpose_transpose vec_lambda_eta vector_component_simps(5))
moreover have "aa = a ∧ bb = b" if "(χ i. if i = None then bb else transpose aa $ the i) = A'"
for aa bb using a_def b_def that by force
ultimately have "∃! (A, t). ?P(A,t) = A'"
unfolding Ex1_def by (auto simp add: split_def)
then have "(∑x ∈ UNIV. indicat_real {Some A'} (Some (?P (fst x, snd x)))) = 1"
by (subst indicator_def, subst ex1_sum, simp_all add: split_def finite_Prod_UNIV)
then have "(∑A∈UNIV. ∑t∈UNIV. indicat_real {Some A'}
(Some (?P (A,t)))) = 1"
by (subst sum_cartesian_product'[symmetric]) (simp add: split_def )
then show ?case by (simp add: spmf_bind spmf_of_set integral_spmf_of_set)
qed
have game⇩2_eq_game⇩3_is_encrypt:
"?sample (game⇩2 is_encrypt) = game⇩3 (is_encrypt')"
proof -
have "?sample (game⇩2 is_encrypt) =
(spmf_of_set UNIV ⤜
(λA. spmf_of_set UNIV ⤜
(λt. let A' = χ i. if i = None then t else transpose A $ the i in
return_spmf A'))) ⤜
(λA'. let A = transpose (χ i. vec_nth A' (Some i));
t = A' $ None
in coin_spmf ⤜
(λb. exec_gpv ro.oracle (𝒜⇩1 (A, t)) ro.initial ⤜
(λ(((msg1, msg2), σ), s). if valid_plains msg1 msg2
then let msg = if b then msg1 else msg2
in spmf_of_pmf mlwe.beta_vec ⤜
(λr. spmf_of_pmf mlwe.beta_vec ⤜
(λe1. spmf_of_pmf mlwe.beta ⤜
(λe2. let e = χ i. if i = None then e2 else e1 $ the i;
c = A' *v r + e; u = compress_vec du (χ i. c $ Some i);
v = compress_poly dv (c $ None + to_module
(round (real_of_int q / 2)) * plain_to_msg msg)
in return_spmf (u, v)))) ⤜
(λc. exec_gpv ro.oracle (𝒜⇩2 c σ) s ⤜
(λ(b', s1). return_spmf (b' = b)))
else coin_spmf)))"
unfolding is_encrypt1 unfolding game⇩2_def is_encrypt1_def Let_def by simp
also have " … = spmf_of_set UNIV ⤜
(λA'. let A = transpose (χ i. vec_nth A' (Some i));
t = A' $ None
in coin_spmf ⤜
(λb. exec_gpv ro.oracle (𝒜⇩1 (A, t)) ro.initial ⤜
(λ(((msg1, msg2), σ), s). if valid_plains msg1 msg2
then let msg = if b then msg1 else msg2
in spmf_of_pmf mlwe.beta_vec ⤜
(λr.
(spmf_of_pmf mlwe.beta_vec ⤜
(λe1. spmf_of_pmf mlwe.beta ⤜
(λe2. let e = χ i. if i = None then e2 else e1 $ the i
in return_spmf e))) ⤜
(λe. let c = A' *v r + e; u = compress_vec du (χ i. c $ Some i);
v = compress_poly dv (c $ None + to_module
(round (real_of_int q / 2)) * plain_to_msg msg)
in return_spmf (u, v))) ⤜
(λc. exec_gpv ro.oracle (𝒜⇩2 c σ) s ⤜
(λ(b', s1). return_spmf (b' = b)))
else coin_spmf)))"
by (subst pk_distrib) (simp add: Let_def del: bind_spmf_of_pmf)
also have " … = spmf_of_set UNIV ⤜
(λA'. let A = transpose (χ i. vec_nth A' (Some i));
t = A' $ None
in coin_spmf ⤜
(λb. exec_gpv ro.oracle (𝒜⇩1 (A, t)) ro.initial ⤜
(λ(((msg1, msg2), σ),s). if valid_plains msg1 msg2
then let msg = if b then msg1 else msg2
in spmf_of_pmf mlwe.beta_vec ⤜
(λr. mlwe.beta_vec' ⤜
(λe. let c = A' *v r + e; u = compress_vec du (χ i. c $ Some i);
v = compress_poly dv (c $ None + to_module
(round (real_of_int q / 2)) * plain_to_msg msg)
in return_spmf (u, v))) ⤜
(λc. exec_gpv ro.oracle (𝒜⇩2 c σ) s ⤜
(λ(b', s1). return_spmf (b' = b)))
else coin_spmf)))"
unfolding e_distrib by simp
also have "… = game⇩3 is_encrypt'"
unfolding game⇩3_def is_encrypt'_def
by (simp add: bind_commute_spmf[of "coin_spmf"] bind_spmf_pmf_assoc)
finally show ?thesis
by blast
qed
text ‹We can write the distribution of the cipher test as one draw from a
probability distribution over the option type as well.
Using this, we can show ‹?sample (game⇩2 rand_encrypt) = game⇩3 (λ_. spmf_of_set UNIV)›.
This corresponds to the uniformly random instance in the module-LWE advantage.›
have cipher_distrib:
"do{
u ← spmf_of_set (UNIV:: ('a qr, 'k) vec set);
v ← spmf_of_set (UNIV:: 'a qr set);
return_spmf (u, v)
} = do{
c ← spmf_of_set (UNIV:: ('a qr, 'k option) vec set);
let u = χ i. c $ Some i;
v = c $ None in
return_spmf (u,v)
}" for msg :: bitstring
proof (intro spmf_eqI, unfold Let_def, goal_cases)
case (1 w)
have "(∑x∈UNIV. ∑xa∈UNIV. indicat_real {Some w} (Some (x, xa))) = 1"
proof -
have "(∑x∈UNIV. ∑xa∈UNIV. indicat_real {Some w} (Some (x, xa))) =
(∑x∈UNIV. indicat_real {Some w} (Some x))"
by (subst sum_cartesian_product'[symmetric]) simp
also have "… = 1" unfolding indicator_def
using finite_cartesian_product[OF finite_UNIV_vec finite_qr]
by (subst ex1_sum) simp_all
finally show ?thesis by blast
qed
moreover have "(∑x∈UNIV. indicat_real {Some w} (Some (χ i. x $ Some i, x $ None))) = 1"
proof (unfold indicator_def, subst ex1_sum, goal_cases)
case 1
define x where "x = (χ i. if i = None then snd w else fst w $ (the i))"
have "Some (χ i. x $ Some i, x $ None) ∈ {Some w}" by (simp add: x_def)
moreover have "(∀y. Some (χ i. y $ Some i, y $ None) ∈ {Some w} ⟶ y = x)"
by (metis (mono_tags) Option.option.exhaust Option.option.sel Product_Type.prod.sel(1)
Product_Type.prod.sel(2) calculation singletonD vec_lambda_unique)
ultimately show ?case unfolding Ex1_def by (intro exI) simp
qed simp_all
ultimately show ?case
by (simp add: spmf_bind integral_spmf_of_set)
qed
have game⇩2_eq_game⇩3_rand_encrypt:
"?sample (game⇩2 rand_encrypt) = game⇩3 (λ_. spmf_of_set UNIV)"
proof -
have "?sample (game⇩2 rand_encrypt) =
(spmf_of_set UNIV ⤜
(λA. spmf_of_set UNIV ⤜
(λt. let A' = χ i. if i = None then t else transpose A $ the i in
return_spmf A'))) ⤜
(λA'. let A = transpose (χ i. vec_nth A' (Some i));
t = A' $ None
in coin_spmf ⤜
(λb. exec_gpv ro.oracle (𝒜⇩1 (A, t)) ro.initial ⤜
(λ(((msg1, msg2), σ),s). if valid_plains msg1 msg2
then let msg = if b then msg1 else msg2
in rand_encrypt1 A t msg ⤜
(λc. exec_gpv ro.oracle (𝒜⇩2 c σ) s ⤜
(λ(b', s1). return_spmf (b' = b)))
else coin_spmf)))"
unfolding rand_encrypt1 unfolding game⇩2_def Let_def by simp
also have " … = spmf_of_set UNIV ⤜
(λA'. let A = transpose (χ i. A' $ (Some i));
t = A' $ None
in coin_spmf ⤜
(λb. exec_gpv ro.oracle (𝒜⇩1 (A, t)) ro.initial ⤜
(λ(((msg1, msg2), σ),s). if valid_plains msg1 msg2
then let msg = if b then msg1 else msg2
in do{ u ← spmf_of_set (UNIV:: ('a qr, 'k) vec set);
v ← spmf_of_set (UNIV:: 'a qr set);
return_spmf (u, v)} ⤜
(λ(u,v). let v' = (v + to_module (round((real_of_int q)/2)) *
(plain_to_msg msg))
in exec_gpv ro.oracle (𝒜⇩2 (compress_vec du u,
compress_poly dv v') σ) s ⤜
(λ(b',s1). return_spmf (b' = b)))
else coin_spmf)))"
unfolding rand_encrypt1_def by (subst pk_distrib)(simp add: Let_def del: bind_spmf_of_pmf)
also have " … = spmf_of_set UNIV ⤜
(λA'. let A = transpose (χ i. vec_nth A' (Some i));
t = A' $ None
in coin_spmf ⤜
(λb. exec_gpv ro.oracle (𝒜⇩1 (A, t)) ro.initial ⤜
(λ(((msg1, msg2), σ),s). if valid_plains msg1 msg2
then let msg = if b then msg1 else msg2
in do{ c ← spmf_of_set (UNIV:: ('a qr, 'k option) vec set);
let u = χ i. c $ Some i; v = c $ None in
return_spmf (u,v) } ⤜
(λ(u,v). let v' = (v + to_module (round((real_of_int q)/2)) *
(plain_to_msg msg))
in exec_gpv ro.oracle (𝒜⇩2 (compress_vec du u,
compress_poly dv v') σ) s ⤜
(λ(b',s1). return_spmf (b' = b)))
else coin_spmf)))"
unfolding cipher_distrib by simp
also have "… = game⇩3 (λ_. spmf_of_set UNIV)"
unfolding game⇩3_def by (simp add: bind_commute_spmf[of "coin_spmf"])
finally show ?thesis
by blast
qed
text ‹Now, we establish the correspondence between the games in the module-LWE advantage and
‹game⇩3›. Here, the rewriting needed to be done manually for some parts, as the automation could not
handle it (commutativity only between certain ‹pmf›s).›
have game⇩3_eq_mlwe_game': "game⇩3 is_encrypt' = mlwe.game' (kyber_reduction2 𝒜)"
proof -
have "mlwe.game' (kyber_reduction2 𝒜) =
spmf_of_set UNIV ⤜ (λA. spmf_of_pmf mlwe.beta_vec ⤜
(λs. exec_gpv ro.oracle (𝒜⇩1 (transpose (χ i. A $ Some i), A $ None)) ro.initial ⤜
(λy. if valid_plains (fst (fst (fst y))) (snd (fst (fst y)))
then coin_spmf ⤜
(λya. mlwe.beta_vec' ⤜
(λe. TRY exec_gpv ro.oracle (𝒜⇩2 (
compress_vec du (χ i. (A *v s) $ Some i + e $ Some i),
compress_poly dv ((A *v s) $ None + e $ None +
to_module (round (real_of_int q / 2)) *
plain_to_msg (if ya then fst (fst (fst y)) else snd (fst (fst y)))))
(snd (fst y))) (snd y) ⤜
(λp. return_spmf (fst p = ya)) ELSE coin_spmf))
else coin_spmf)))"
unfolding mlwe.game'_def
by (simp add: try_bind_assert_spmf split_def bind_commute_spmf[of "mlwe.beta_vec'"]
if_distrib_bind_spmf2 try_spmf_bind_spmf_lossless del: bind_spmf_const) simp
also have "… =
spmf_of_set (UNIV :: (('a qr,'k) vec, 'k option) vec set) ⤜
(λA. spmf_of_pmf mlwe.beta_vec ⤜
(λs. exec_gpv ro.oracle (𝒜⇩1 (transpose (χ i. A $ Some i), A $ None)) ro.initial ⤜
(λy. if valid_plains (fst (fst (fst y))) (snd (fst (fst y)))
then mlwe.beta_vec' ⤜
(λe. coin_spmf ⤜
(λb. exec_gpv ro.oracle (𝒜⇩2 (
compress_vec du (χ i. (A *v s) $ Some i + e $ Some i),
compress_poly dv ((A *v s) $ None + e $ None +
to_module (round (real_of_int q / 2)) *
plain_to_msg (if b then fst (fst (fst y)) else snd (fst (fst y)))))
(snd (fst y))) (snd y) ⤜
(λp. return_spmf (fst p = b))))
else coin_spmf)))"
apply (subst try_spmf_bind_spmf_lossless)
subgoal by (subst lossless_exec_gpv, auto)
subgoal by (auto simp add: bind_commute_spmf[of "mlwe.beta_vec'"])
done
also have "… =
spmf_of_set (UNIV :: (('a qr,'k) vec, 'k option) vec set) ⤜
(λA. exec_gpv ro.oracle (𝒜⇩1 (transpose (χ i. A $ Some i), A $ None)) ro.initial ⤜
(λp. if valid_plains (fst (fst (fst p))) (snd (fst (fst p)))
then spmf_of_pmf mlwe.beta_vec ⤜
(λs. mlwe.beta_vec' ⤜
(λe. coin_spmf ⤜
(λb. exec_gpv ro.oracle (𝒜⇩2 (
compress_vec du (χ i. (A *v s) $ Some i + e $ Some i),
compress_poly dv ((A *v s) $ None + e $ None +
to_module (round (real_of_int q / 2)) *
plain_to_msg (if b then fst (fst (fst p)) else snd (fst (fst p)))))
(snd (fst p))) (snd p) ⤜
(λb'. return_spmf (fst b' = b)))))
else coin_spmf))"
apply (subst bind_commute_spmf[of "spmf_of_pmf mlwe.beta_vec"])+
apply (subst if_distrib_bind_spmf2)
apply (subst bind_commute_spmf[of "spmf_of_pmf mlwe.beta_vec"])+
by (simp add: split_def del: bind_spmf_const)
also have "… = game⇩3 is_encrypt'"
unfolding game⇩3_def is_encrypt'_def Let_def split_def
apply (subst bind_commute_spmf[of "coin_spmf"])+
apply (subst if_distrib_bind_spmf2)
apply (subst bind_commute_spmf[of "coin_spmf"])+
apply (simp add: try_bind_assert_spmf split_def bind_commute_spmf[of "coin_spmf"]
if_distrib_bind_spmf2 bind_spmf_pmf_assoc del: bind_spmf_const)
by simp
ultimately show ?thesis by force
qed
have game⇩3_eq_mlwe_game_random':
"game⇩3 (λ_. spmf_of_set UNIV) = mlwe.game_random' (kyber_reduction2 𝒜)"
proof -
have *: "mlwe.game_random' (kyber_reduction2 𝒜) =
spmf_of_set UNIV ⤜
(λA. exec_gpv ro.oracle (𝒜⇩1 (transpose (χ i. A $ Some i), A $ None)) ro.initial ⤜
(λy. if valid_plains (fst (fst (fst y))) (snd (fst (fst y)))
then spmf_of_set UNIV ⤜
(λb. TRY coin_spmf ⤜
(λba. exec_gpv ro.oracle (𝒜⇩2 (compress_vec du (χ i. b $ Some i),
compress_poly dv (b $ None +
to_module (round (real_of_int q / 2)) * plain_to_msg
(if ba then fst (fst (fst y)) else snd (fst (fst y))))) (snd (fst y))) (snd y) ⤜
(λp. return_spmf (fst p = ba))) ELSE coin_spmf)
else coin_spmf))"
unfolding mlwe.game_random'_def
using bind_commute_spmf[of "spmf_of_set (UNIV :: ('a qr, 'k option) vec set)"]
by (simp add: try_bind_assert_spmf split_def
bind_commute_spmf[of "spmf_of_set (UNIV :: ('a qr, 'k option) vec set)"]
if_distrib_bind_spmf2 del: bind_spmf_const) simp
also have "… =
spmf_of_set UNIV ⤜
(λA. exec_gpv ro.oracle (𝒜⇩1 (transpose (χ i. A $ Some i), A $ None)) ro.initial ⤜
(λp. if valid_plains (fst (fst (fst p))) (snd (fst (fst p)))
then coin_spmf ⤜
(λba. spmf_of_set UNIV ⤜
(λb. exec_gpv ro.oracle (𝒜⇩2 (compress_vec du (χ i. b $ Some i),
compress_poly dv (b $ None + to_module
(round (real_of_int q / 2)) * plain_to_msg (if ba then fst (fst (fst p))
else snd (fst (fst p))))) (snd (fst p))) (snd p) ⤜
(λb'. return_spmf (fst b' = ba))))
else coin_spmf))"
apply (subst try_spmf_bind_spmf_lossless, simp)
apply (subst try_spmf_bind_spmf_lossless)
subgoal by (subst lossless_exec_gpv, auto)
subgoal by (auto simp add: bind_commute_spmf
[of "spmf_of_set (UNIV :: ('a qr, 'k option) vec set)"])
done
then show ?thesis unfolding game⇩3_def *
by (simp add: try_bind_assert_spmf split_def bind_commute_spmf[of "coin_spmf"]
if_distrib_bind_spmf2 del: bind_spmf_const) simp
qed
text ‹This finishes the second reduction step. In this case, the reduction function was
‹kyber_reduction2›.›
have reduction2: "¦spmf (game⇩3 is_encrypt') True - spmf (game⇩3 (λ_. spmf_of_set UNIV)) True¦ ≤
mlwe.advantage' (kyber_reduction2 𝒜)"
unfolding game⇩3_eq_mlwe_game' game⇩3_eq_mlwe_game_random' mlwe.advantage'_def
by simp
text ‹Now that $u$ and $v$ are generated uniformly at random, we need to show that adding the
message will again result in a uniformly random variable. The reason is that we work over the
finite space $R_q$.
‹game⇩4› is the game where the message is no longer added, but the ciphertext is uniformly at
random.›
define game⇩4 where
"game⇩4 = do {
b ← coin_spmf;
A' ← spmf_of_set (UNIV :: (('a qr,'k) vec, 'k option) vec set);
let A = transpose (χ i. vec_nth A' (Some i));
let t = A' $ None;
(((msg1, msg2), σ), s) ← exec_gpv ro.oracle (𝒜⇩1 (A,t)) ro.initial;
if valid_plains msg1 msg2
then do {
let msg = (if b then msg1 else msg2);
c ← spmf_of_set UNIV;
let u = (χ i. c $ Some i);
let v = c $ None;
(b', s1) ← exec_gpv ro.oracle (𝒜⇩2 (compress_vec du u, compress_poly dv v) σ) s;
return_spmf (b' = b)
}
else coin_spmf
}"
text ‹Adding the message does not change the uniform distribution.
This is needed to show that ‹game⇩3 (λ_. spmf_of_set UNIV) = game⇩4›.›
have indep_of_msg:
"do {c ← spmf_of_set UNIV;
let u = χ i. c $ Some i;
v = c $ None + to_module (round (real_of_int q / 2)) * plain_to_msg msg
in return_spmf (u, v)} =
do {c ← spmf_of_set UNIV;
let u = χ i. c $ Some i; v = c $ None
in return_spmf (u, v)}" for msg::bitstring
proof (intro spmf_eqI, goal_cases)
case (1 y)
define msg' where "msg' = to_module (round (real_of_int q / 2)) * plain_to_msg msg"
have "(∑x∈UNIV. of_bool ((χ i. x $ Some i, x $ None + msg') = y)) = 1"
proof (intro ex1_sum, goal_cases)
case 1
define x where "x = (χ i. if i = None then snd y - msg' else (fst y) $ (the i))"
have "(χ i. x $ Some i, x $ None + msg') = y" unfolding x_def by simp
moreover have "(∀ya. (χ i. ya $ Some i, ya $ None + msg') = y ⟶ ya = x)"
unfolding x_def
by (metis (mono_tags, lifting) Groups.group_add_class.add.right_cancel
Option.option.exhaust calculation fst_conv snd_conv vec_lambda_unique x_def)
ultimately show ?case unfolding Ex1_def by (intro exI) simp
qed (simp add: finite_vec)
moreover have "… = (∑x∈UNIV. of_bool ((χ i. x $ Some i, x $ None) = y))"
proof (subst ex1_sum, goal_cases)
case 1
define x where "x = (χ i. if i = None then snd y else (fst y) $ (the i))"
have "(χ i. x $ Some i, x $ None) = y" unfolding x_def by simp
moreover have "(∀ya. (χ i. ya $ Some i, ya $ None) = y ⟶ ya = x)"
unfolding x_def
by (metis (mono_tags, lifting)
Option.option.exhaust calculation fst_conv snd_conv vec_lambda_unique x_def)
ultimately show ?case unfolding Ex1_def by (intro exI) simp
qed (simp_all add: finite_vec)
ultimately have "(∑x∈UNIV. of_bool ((χ i. x $ Some i, x $ None + msg') = y)) =
(∑x∈UNIV. of_bool ((χ i. x $ Some i, x $ None) = y))"
by (smt (verit))
then show ?case unfolding msg'_def[symmetric]
by (simp add: spmf_bind integral_spmf_of_set indicator_def del: sum_of_bool_eq)
qed
have game⇩3_eq_game⇩4: "game⇩3 (λ_. spmf_of_set UNIV) = game⇩4"
proof -
have "game⇩3 (λ_. spmf_of_set UNIV) = coin_spmf ⤜
(λb. spmf_of_set UNIV ⤜
(λA'. let A = transpose (χ i. A' $ Some i); t = A' $ None
in exec_gpv ro.oracle (𝒜⇩1 (A, t)) ro.initial ⤜
(λ(((msg1, msg2), σ),s).
if valid_plains msg1 msg2
then let msg = if b then msg1 else msg2 in
do {c ← spmf_of_set UNIV;
let u = χ i. c $ Some i;
v = c $ None + to_module (round (real_of_int q / 2)) * plain_to_msg msg
in return_spmf (u, v)} ⤜
(λ (u,v). exec_gpv ro.oracle
(𝒜⇩2 (compress_vec du u, compress_poly dv v) σ) s ⤜
(λ(b', s1). return_spmf (b' = b)))
else coin_spmf)))"
unfolding game⇩3_def by simp
also have "… = coin_spmf ⤜
(λb. spmf_of_set UNIV ⤜
(λA'. let A = transpose (χ i. A' $ Some i); t = A' $ None
in exec_gpv ro.oracle (𝒜⇩1 (A, t)) ro.initial ⤜
(λ(((msg1, msg2), σ), s).
if valid_plains msg1 msg2
then let msg = if b then msg1 else msg2 in
do {c ← spmf_of_set UNIV;
let u = χ i. c $ Some i; v = c $ None
in return_spmf (u, v)} ⤜
(λ (u,v). exec_gpv ro.oracle (𝒜⇩2
(compress_vec du u, compress_poly dv v) σ) s ⤜
(λ(b', s1). return_spmf (b' = b)))
else coin_spmf)))"
unfolding indep_of_msg by simp
also have "… = game⇩4"
unfolding game⇩4_def by simp
finally show ?thesis by blast
qed
text ‹Finally, we can show that ‹game⇩4› is the same as a coin flip. Therefore,
the probability to return true is exactly $0.5$.›
have game⇩4_eq_coin: "game⇩4 = coin_spmf"
proof -
have "game⇩4 = spmf_of_set UNIV ⤜
(λy. exec_gpv ro.oracle (𝒜⇩1 (transpose (χ i. y $ Some i), y $ None)) ro.initial ⤜
(λy. if valid_plains (fst (fst (fst y))) (snd (fst (fst y)))
then spmf_of_set UNIV ⤜
(λya. exec_gpv ro.oracle (𝒜⇩2 (compress_vec du (χ i. ya $ Some i),
compress_poly dv (ya $ None)) (snd (fst y))) (snd y) ⤜
(λy. coin_spmf))
else coin_spmf))"
unfolding game⇩4_def by (simp add: bind_commute_spmf[of "coin_spmf"] split_def
if_distrib_bind_spmf2 bind_coin_spmf_eq_const bind_spmf_coin del: bind_spmf_const)
also have "… = spmf_of_set UNIV ⤜
(λy. exec_gpv ro.oracle (𝒜⇩1 (transpose (χ i. y $ Some i), y $ None)) ro.initial ⤜
(λy. if valid_plains (fst (fst (fst y))) (snd (fst (fst y)))
then coin_spmf
else coin_spmf))"
by (subst bind_spmf_coin) (subst lossless_exec_gpv, auto)
also have "… = spmf_of_set UNIV ⤜
(λy. exec_gpv ro.oracle (𝒜⇩1 (transpose (χ i. y $ Some i), y $ None)) ro.initial ⤜
(λy. coin_spmf))"
by simp
also have "… = coin_spmf"
by (subst bind_spmf_coin) (subst lossless_exec_gpv, auto)
finally show ?thesis by auto
qed
have spmf_game⇩4: "spmf (game⇩4) True = 1/2" unfolding game⇩4_eq_coin
spmf_coin_spmf by simp
text ‹In the end, we assemble all the steps proven before in order to bound the advantage against
IND-CPA.›
have "ind_cpa.advantage (ro.oracle, ro.initial) 𝒜 = ¦spmf (game⇩0) True - 1/2¦"
unfolding ind_cpa.advantage.simps ind_cpa_game_eq_game⇩0 ..
also have "… ≤ ¦spmf (game⇩1 is_pk) True - spmf (game⇩1 rand_pk) True¦ +
¦spmf (game⇩1 rand_pk) True - 1/2¦"
unfolding game⇩0_eq_game⇩1_is_pk by simp
also have "… ≤ mlwe.advantage (kyber_reduction1 𝒜) + ¦spmf (game⇩1 rand_pk) True - 1/2¦"
by (simp add: reduction1 𝒜[symmetric] del: 𝒜)
also have "… ≤ mlwe.advantage (kyber_reduction1 𝒜) +
¦spmf (?sample (game⇩2 is_encrypt)) True - spmf (?sample (game⇩2 is_encrypt)) True ¦ +
¦spmf (?sample (game⇩2 is_encrypt)) True - 1/2¦"
using game⇩1_rand_pk_eq_game⇩2_is_encrypt by simp
also have "… ≤ mlwe.advantage (kyber_reduction1 𝒜) +
¦spmf (game⇩3 is_encrypt') True - spmf (game⇩3 (λ_. spmf_of_set UNIV)) True ¦ +
¦spmf (game⇩3 (λ_. spmf_of_set UNIV)) True - 1/2¦"
using game⇩2_eq_game⇩3_is_encrypt game⇩2_eq_game⇩3_rand_encrypt by simp
also have "… ≤ mlwe.advantage (kyber_reduction1 𝒜) +
mlwe.advantage' (kyber_reduction2 𝒜) +
¦spmf (game⇩3 (λ_. spmf_of_set UNIV)) True - 1/2¦"
using reduction2 by simp
also have "… ≤ mlwe.advantage (kyber_reduction1 𝒜) +
mlwe.advantage' (kyber_reduction2 𝒜) +
¦spmf (game⇩4) True - 1/2¦"
unfolding game⇩3_eq_game⇩4 by simp
also have "… ≤ mlwe.advantage (kyber_reduction1 𝒜) +
mlwe.advantage' (kyber_reduction2 𝒜)"
unfolding spmf_game⇩4 by simp
finally show ?thesis by simp
qed
end
end