Theory Noar_Pinkas_OT
subsection ‹Noar Pinkas OT›
text‹Here we prove security for the Noar Pinkas OT from \<^cite>‹"DBLP:conf/soda/NaorP01"›.›
theory Noar_Pinkas_OT imports
Cyclic_Group_Ext
Game_Based_Crypto.Diffie_Hellman
OT_Functionalities
Semi_Honest_Def
Uniform_Sampling
begin
locale np_base =
fixes 𝒢 :: "'grp cyclic_group" (structure)
assumes finite_group: "finite (carrier 𝒢)"
and or_gt_0: "0 < order 𝒢"
and prime_order: "prime (order 𝒢)"
begin
lemma prime_field: "a < (order 𝒢) ⟹ a ≠ 0 ⟹ coprime a (order 𝒢)"
by(metis dvd_imp_le neq0_conv not_le prime_imp_coprime prime_order coprime_commute)
lemma weight_sample_uniform_units: "weight_spmf (sample_uniform_units (order 𝒢)) = 1"
using lossless_spmf_def lossless_sample_uniform_units prime_order prime_gt_1_nat by auto
definition protocol :: "('grp × 'grp) ⇒ bool ⇒ (unit × 'grp) spmf"
where "protocol M v = do {
let (m0,m1) = M;
a :: nat ← sample_uniform (order 𝒢);
b :: nat ← sample_uniform (order 𝒢);
let c⇩v = (a*b) mod (order 𝒢);
c⇩v' :: nat ← sample_uniform (order 𝒢);
r0 :: nat ← sample_uniform_units (order 𝒢);
s0 :: nat ← sample_uniform_units (order 𝒢);
let w0 = (❙g [^] a) [^] s0 ⊗ ❙g [^] r0;
let z0' = ((❙g [^] (if v then c⇩v' else c⇩v)) [^] s0) ⊗ ((❙g [^] b) [^] r0);
r1 :: nat ← sample_uniform_units (order 𝒢);
s1 :: nat ← sample_uniform_units (order 𝒢);
let w1 = (❙g [^] a) [^] s1 ⊗ ❙g [^] r1;
let z1' = ((❙g [^] ((if v then c⇩v else c⇩v'))) [^] s1) ⊗ ((❙g [^] b) [^] r1);
let enc_m0 = z0' ⊗ m0;
let enc_m1 = z1' ⊗ m1;
let out_2 = (if v then enc_m1 ⊗ inv (w1 [^] b) else enc_m0 ⊗ inv (w0 [^] b));
return_spmf ((), out_2)}"
lemma lossless_protocol: "lossless_spmf (protocol M σ)"
apply(auto simp add: protocol_def Let_def split_def lossless_sample_uniform_units or_gt_0)
using prime_order prime_gt_1_nat lossless_sample_uniform_units by simp
type_synonym 'grp' view1 = "(('grp' × 'grp') × ('grp' × 'grp' × 'grp' × 'grp')) spmf"
type_synonym 'grp' dist_adversary = "(('grp' × 'grp') × 'grp' × 'grp' × 'grp' × 'grp') ⇒ bool spmf"
definition R1 :: "('grp × 'grp) ⇒ bool ⇒ 'grp view1"
where "R1 msgs σ = do {
let (m0, m1) = msgs;
a ← sample_uniform (order 𝒢);
b ← sample_uniform (order 𝒢);
let c⇩σ = a*b;
c⇩σ' ← sample_uniform (order 𝒢);
return_spmf (msgs, (❙g [^] a, ❙g [^] b, (if σ then ❙g [^] c⇩σ' else ❙g [^] c⇩σ), (if σ then ❙g [^] c⇩σ else ❙g [^] c⇩σ')))}"
lemma lossless_R1: "lossless_spmf (R1 M σ)"
by(simp add: R1_def Let_def lossless_sample_uniform_units or_gt_0)
definition inter :: "('grp × 'grp) ⇒ 'grp view1"
where "inter msgs = do {
a ← sample_uniform (order 𝒢);
b ← sample_uniform (order 𝒢);
c ← sample_uniform (order 𝒢);
d ← sample_uniform (order 𝒢);
return_spmf (msgs, ❙g [^] a, ❙g [^] b, ❙g [^] c, ❙g [^] d)}"
definition S1 :: "('grp × 'grp) ⇒ unit ⇒ 'grp view1"
where "S1 msgs out1 = do {
let (m0, m1) = msgs;
a ← sample_uniform (order 𝒢);
b ← sample_uniform (order 𝒢);
c ← sample_uniform (order 𝒢);
return_spmf (msgs, (❙g [^] a, ❙g [^] b, ❙g [^] c, ❙g [^] (a*b)))}"
lemma lossless_S1: "lossless_spmf (S1 M out1)"
by(simp add: S1_def Let_def lossless_sample_uniform_units or_gt_0)
fun R1_inter_adversary :: "'grp dist_adversary ⇒ ('grp × 'grp) ⇒ 'grp ⇒ 'grp ⇒ 'grp ⇒ bool spmf"
where "R1_inter_adversary 𝒜 msgs α β γ = do {
c ← sample_uniform (order 𝒢);
𝒜 (msgs, α, β, γ, ❙g [^] c)}"
fun inter_S1_adversary :: "'grp dist_adversary ⇒ ('grp × 'grp) ⇒ 'grp ⇒ 'grp ⇒ 'grp ⇒ bool spmf"
where "inter_S1_adversary 𝒜 msgs α β γ = do {
c ← sample_uniform (order 𝒢);
𝒜 (msgs, α, β, ❙g [^] c, γ)}"
sublocale ddh: ddh 𝒢 .
definition R2 :: "('grp × 'grp) ⇒ bool ⇒ (bool × 'grp × 'grp × 'grp × 'grp × 'grp × 'grp × 'grp) spmf"
where "R2 M v = do {
let (m0,m1) = M;
a :: nat ← sample_uniform (order 𝒢);
b :: nat ← sample_uniform (order 𝒢);
let c⇩v = (a*b) mod (order 𝒢);
c⇩v' :: nat ← sample_uniform (order 𝒢);
r0 :: nat ← sample_uniform_units (order 𝒢);
s0 :: nat ← sample_uniform_units (order 𝒢);
let w0 = (❙g [^] a) [^] s0 ⊗ ❙g [^] r0;
let z = ((❙g [^] c⇩v') [^] s0) ⊗ ((❙g [^] b) [^] r0);
r1 :: nat ← sample_uniform_units (order 𝒢);
s1 :: nat ← sample_uniform_units (order 𝒢);
let w1 = (❙g [^] a) [^] s1 ⊗ ❙g [^] r1;
let z' = ((❙g [^] (c⇩v)) [^] s1) ⊗ ((❙g [^] b) [^] r1);
let enc_m = z ⊗ (if v then m0 else m1);
let enc_m' = z' ⊗ (if v then m1 else m0) ;
return_spmf(v, ❙g [^] a, ❙g [^] b, ❙g [^] c⇩v, w0, enc_m, w1, enc_m')}"
lemma lossless_R2: "lossless_spmf (R2 M σ)"
apply(simp add: R2_def Let_def split_def lossless_sample_uniform_units or_gt_0)
using prime_order prime_gt_1_nat lossless_sample_uniform_units by simp
definition S2 :: "bool ⇒ 'grp ⇒ (bool × 'grp × 'grp × 'grp × 'grp × 'grp × 'grp × 'grp) spmf"
where "S2 v m = do {
a :: nat ← sample_uniform (order 𝒢);
b :: nat ← sample_uniform (order 𝒢);
let c⇩v = (a*b) mod (order 𝒢);
r0 :: nat ← sample_uniform_units (order 𝒢);
s0 :: nat ← sample_uniform_units (order 𝒢);
let w0 = (❙g [^] a) [^] s0 ⊗ ❙g [^] r0;
r1 :: nat ← sample_uniform_units (order 𝒢);
s1 :: nat ← sample_uniform_units (order 𝒢);
let w1 = (❙g [^] a) [^] s1 ⊗ ❙g [^] r1;
let z' = ((❙g [^] (c⇩v)) [^] s1) ⊗ ((❙g [^] b) [^] r1);
s' ← sample_uniform (order 𝒢);
let enc_m = ❙g [^] s';
let enc_m' = z' ⊗ m ;
return_spmf(v, ❙g [^] a, ❙g [^] b, ❙g [^] c⇩v, w0, enc_m, w1, enc_m')}"
lemma lossless_S2: "lossless_spmf (S2 σ out2)"
apply(simp add: S2_def Let_def lossless_sample_uniform_units or_gt_0)
using prime_order prime_gt_1_nat lossless_sample_uniform_units by simp
sublocale sim_def: sim_det_def R1 S1 R2 S2 funct_OT_12 protocol
unfolding sim_det_def_def
by(auto simp add: lossless_R1 lossless_S1 lossless_R2 lossless_S2 lossless_protocol lossless_funct_OT_12)
end
locale np = np_base + cyclic_group 𝒢
begin
lemma protocol_inverse:
assumes "m0 ∈ carrier 𝒢" "m1 ∈ carrier 𝒢"
shows" ((❙g [^] ((a*b) mod (order 𝒢))) [^] (s1 :: nat)) ⊗ ((❙g [^] b) [^] (r1::nat)) ⊗ (if v then m0 else m1) ⊗ inv (((❙g [^] a) [^] s1 ⊗ ❙g [^] r1) [^] b)
= (if v then m0 else m1)"
(is "?lhs = ?rhs")
proof-
have 1: "(a*b)*(s1) + b*r1 =((a::nat)*(s1) + r1)*b " using mult.commute mult.assoc add_mult_distrib by auto
have "?lhs =
((❙g [^] (a*b)) [^] s1) ⊗ ((❙g [^] b) [^] r1) ⊗ (if v then m0 else m1) ⊗ inv (((❙g [^] a) [^] s1 ⊗ ❙g [^] r1) [^] b)"
by(simp add: pow_generator_mod)
also have "... = (❙g [^] ((a*b)*(s1))) ⊗ ((❙g [^] (b*r1))) ⊗ ((if v then m0 else m1) ⊗ inv (((❙g [^] ((a*(s1) + r1)*b)))))"
by(auto simp add: nat_pow_pow nat_pow_mult assms cyclic_group_assoc)
also have "... = ❙g [^] ((a*b)*(s1)) ⊗ ❙g [^] (b*r1) ⊗ ((inv (((❙g [^] ((a*(s1) + r1)*b))))) ⊗ (if v then m0 else m1))"
by(simp add: nat_pow_mult cyclic_group_commute assms)
also have "... = (❙g [^] ((a*b)*(s1) + b*r1) ⊗ inv (((❙g [^] ((a*(s1) + r1)*b))))) ⊗ (if v then m0 else m1)"
by(simp add: nat_pow_mult cyclic_group_assoc assms)
also have "... = (❙g [^] ((a*b)*(s1) + b*r1) ⊗ inv (((❙g [^] (((a*b)*(s1) + r1*b)))))) ⊗ (if v then m0 else m1)"
using 1 by (simp add: mult.commute)
ultimately show ?thesis
using l_cancel_inv assms by (simp add: mult.commute)
qed
lemma correctness:
assumes "m0 ∈ carrier 𝒢" "m1 ∈ carrier 𝒢"
shows "sim_def.correctness (m0,m1) σ"
proof-
have "protocol (m0, m1) σ = funct_OT_12 (m0, m1) σ"
proof-
have "protocol (m0, m1) σ = do {
a :: nat ← sample_uniform (order 𝒢);
b :: nat ← sample_uniform (order 𝒢);
r1 :: nat ← sample_uniform_units (order 𝒢);
s1 :: nat ← sample_uniform_units (order 𝒢);
let out_2 = ((❙g [^] ((a*b) mod (order 𝒢))) [^] s1) ⊗ ((❙g [^] b) [^] r1) ⊗ (if σ then m1 else m0) ⊗ inv (((❙g [^] a) [^] s1 ⊗ ❙g [^] r1) [^] b);
return_spmf ((), out_2)}"
by(simp add: protocol_def lossless_sample_uniform_units bind_spmf_const weight_sample_uniform_units or_gt_0)
also have "... = do {
let out_2 = (if σ then m1 else m0);
return_spmf ((), out_2)}"
by(simp add: protocol_inverse assms lossless_sample_uniform_units bind_spmf_const weight_sample_uniform_units or_gt_0)
ultimately show ?thesis by(simp add: Let_def funct_OT_12_def)
qed
thus ?thesis
by(simp add: sim_def.correctness_def)
qed
lemma security_P1:
shows "sim_def.adv_P1 msgs σ D ≤ ddh.advantage (R1_inter_adversary D msgs) + ddh.advantage (inter_S1_adversary D msgs)"
(is "?lhs ≤ ?rhs")
proof(cases σ)
case True
have "R1 msgs σ = S1 msgs out1" for out1
by(simp add: R1_def S1_def True)
then have "sim_def.adv_P1 msgs σ D = 0"
by(simp add: sim_def.adv_P1_def funct_OT_12_def)
also have "ddh.advantage A ≥ 0" for A using ddh.advantage_def by simp
ultimately show ?thesis by simp
next
case False
have bounded_advantage: "¦(a :: real) - b¦ = e1 ⟹ ¦b - c¦ = e2 ⟹ ¦a - c¦ ≤ e1 + e2"
for a b e1 c e2 by simp
also have R1_inter_dist: "¦spmf (R1 msgs False ⤜ D) True - spmf ((inter msgs) ⤜ D) True¦ = ddh.advantage (R1_inter_adversary D msgs)"
unfolding R1_def inter_def ddh.advantage_def ddh.ddh_0_def ddh.ddh_1_def Let_def split_def by(simp)
also have inter_S1_dist: "¦spmf ((inter msgs) ⤜ D) True - spmf (S1 msgs out1 ⤜ D) True¦ = ddh.advantage (inter_S1_adversary D msgs)"
for out1 including monad_normalisation
by(simp add: S1_def inter_def ddh.advantage_def ddh.ddh_0_def ddh.ddh_1_def)
ultimately have "¦spmf (R1 msgs False ⤜ (λview. D view)) True - spmf (S1 msgs out1 ⤜ (λview. D view)) True¦ ≤ ?rhs"
for out1 using R1_inter_dist by auto
thus ?thesis by(simp add: sim_def.adv_P1_def funct_OT_12_def False)
qed
lemma add_mult_one_time_pad:
assumes "s0 < order 𝒢"
and "s0 ≠ 0"
shows "map_spmf (λ c⇩v'. (((b* r0) + (s0 * c⇩v')) mod(order 𝒢))) (sample_uniform (order 𝒢)) = sample_uniform (order 𝒢)"
proof-
have "gcd s0 (order 𝒢) = 1"
using assms prime_field by simp
thus ?thesis
using add_mult_one_time_pad by force
qed
lemma security_P2:
assumes "m0 ∈ carrier 𝒢" "m1 ∈ carrier 𝒢"
shows "sim_def.perfect_sec_P2 (m0,m1) σ"
proof-
have "R2 (m0, m1) σ = S2 σ (if σ then m1 else m0)"
including monad_normalisation
proof-
have "R2 (m0, m1) σ = do {
a :: nat ← sample_uniform (order 𝒢);
b :: nat ← sample_uniform (order 𝒢);
let c⇩v = (a*b) mod (order 𝒢);
c⇩v' :: nat ← sample_uniform (order 𝒢);
r0 :: nat ← sample_uniform_units (order 𝒢);
s0 :: nat ← sample_uniform_units (order 𝒢);
let w0 = (❙g [^] a) [^] s0 ⊗ ❙g [^] r0;
let s' = (((b* r0) + ((c⇩v')*(s0))) mod(order 𝒢));
let z = ❙g [^] s' ;
r1 :: nat ← sample_uniform_units (order 𝒢);
s1 :: nat ← sample_uniform_units (order 𝒢);
let w1 = (❙g [^] a) [^] s1 ⊗ ❙g [^] r1;
let z' = ((❙g [^] (c⇩v)) [^] s1) ⊗ ((❙g [^] b) [^] r1);
let enc_m = z ⊗ (if σ then m0 else m1);
let enc_m' = z' ⊗ (if σ then m1 else m0) ;
return_spmf(σ, ❙g [^] a, ❙g [^] b, ❙g [^] c⇩v, w0, enc_m, w1, enc_m')}"
by(simp add: R2_def nat_pow_pow nat_pow_mult pow_generator_mod add.commute)
also have "... = do {
a :: nat ← sample_uniform (order 𝒢);
b :: nat ← sample_uniform (order 𝒢);
let c⇩v = (a*b) mod (order 𝒢);
r0 :: nat ← sample_uniform_units (order 𝒢);
s0 :: nat ← sample_uniform_units (order 𝒢);
let w0 = (❙g [^] a) [^] s0 ⊗ ❙g [^] r0;
s' ← map_spmf (λ c⇩v'. (((b* r0) + ((c⇩v')*(s0))) mod(order 𝒢))) (sample_uniform (order 𝒢));
let z = ❙g [^] s';
r1 :: nat ← sample_uniform_units (order 𝒢);
s1 :: nat ← sample_uniform_units (order 𝒢);
let w1 = (❙g [^] a) [^] s1 ⊗ ❙g [^] r1;
let z' = ((❙g [^] (c⇩v)) [^] s1) ⊗ ((❙g [^] b) [^] r1);
let enc_m = z ⊗ (if σ then m0 else m1);
let enc_m' = z' ⊗ (if σ then m1 else m0) ;
return_spmf(σ, ❙g [^] a, ❙g [^] b, ❙g [^] c⇩v, w0, enc_m, w1, enc_m')}"
by(simp add: bind_map_spmf o_def Let_def)
also have "... = do {
a :: nat ← sample_uniform (order 𝒢);
b :: nat ← sample_uniform (order 𝒢);
let c⇩v = (a*b) mod (order 𝒢);
r0 :: nat ← sample_uniform_units (order 𝒢);
s0 :: nat ← sample_uniform_units (order 𝒢);
let w0 = (❙g [^] a) [^] s0 ⊗ ❙g [^] r0;
s' ← (sample_uniform (order 𝒢));
let z = ❙g [^] s';
r1 :: nat ← sample_uniform_units (order 𝒢);
s1 :: nat ← sample_uniform_units (order 𝒢);
let w1 = (❙g [^] a) [^] s1 ⊗ ❙g [^] r1;
let z' = ((❙g [^] (c⇩v)) [^] s1) ⊗ ((❙g [^] b) [^] r1);
let enc_m = z ⊗ (if σ then m0 else m1);
let enc_m' = z' ⊗ (if σ then m1 else m0) ;
return_spmf(σ, ❙g [^] a, ❙g [^] b, ❙g [^] c⇩v, w0, enc_m, w1, enc_m')}"
by(simp add: add_mult_one_time_pad Let_def mult.commute cong: bind_spmf_cong_simp)
also have "... = do {
a :: nat ← sample_uniform (order 𝒢);
b :: nat ← sample_uniform (order 𝒢);
let c⇩v = (a*b) mod (order 𝒢);
r0 :: nat ← sample_uniform_units (order 𝒢);
s0 :: nat ← sample_uniform_units (order 𝒢);
let w0 = (❙g [^] a) [^] s0 ⊗ ❙g [^] r0;
r1 :: nat ← sample_uniform_units (order 𝒢);
s1 :: nat ← sample_uniform_units (order 𝒢);
let w1 = (❙g [^] a) [^] s1 ⊗ ❙g [^] r1;
let z' = ((❙g [^] (c⇩v)) [^] s1) ⊗ ((❙g [^] b) [^] r1);
enc_m ← map_spmf (λ s'. ❙g [^] s' ⊗ (if σ then m0 else m1)) (sample_uniform (order 𝒢));
let enc_m' = z' ⊗ (if σ then m1 else m0) ;
return_spmf(σ, ❙g [^] a, ❙g [^] b, ❙g [^] c⇩v, w0, enc_m, w1, enc_m')}"
by(simp add: bind_map_spmf o_def Let_def)
also have "... = do {
a :: nat ← sample_uniform (order 𝒢);
b :: nat ← sample_uniform (order 𝒢);
let c⇩v = (a*b) mod (order 𝒢);
r0 :: nat ← sample_uniform_units (order 𝒢);
s0 :: nat ← sample_uniform_units (order 𝒢);
let w0 = (❙g [^] a) [^] s0 ⊗ ❙g [^] r0;
r1 :: nat ← sample_uniform_units (order 𝒢);
s1 :: nat ← sample_uniform_units (order 𝒢);
let w1 = (❙g [^] a) [^] s1 ⊗ ❙g [^] r1;
let z' = ((❙g [^] (c⇩v)) [^] s1) ⊗ ((❙g [^] b) [^] r1);
enc_m ← map_spmf (λ s'. ❙g [^] s') (sample_uniform (order 𝒢));
let enc_m' = z' ⊗ (if σ then m1 else m0) ;
return_spmf(σ, ❙g [^] a, ❙g [^] b, ❙g [^] c⇩v, w0, enc_m, w1, enc_m')}"
by(simp add: sample_uniform_one_time_pad assms)
ultimately show ?thesis by(simp add: S2_def Let_def bind_map_spmf o_def)
qed
thus ?thesis
by(simp add: sim_def.perfect_sec_P2_def funct_OT_12_def)
qed
end
locale np_asymp =
fixes 𝒢 :: "security ⇒ 'grp cyclic_group"
assumes np: "⋀η. np (𝒢 η)"
begin
sublocale np "𝒢 η" for η by(simp add: np)
theorem correctness_asymp:
assumes "m0 ∈ carrier (𝒢 η)" "m1 ∈ carrier (𝒢 η)"
shows "sim_def.correctness η (m0, m1) σ"
by(simp add: correctness assms)
theorem security_P1_asymp:
assumes "negligible (λ η. ddh.advantage η (inter_S1_adversary η D msgs))"
and "negligible (λ η. ddh.advantage η (R1_inter_adversary η D msgs))"
shows "negligible (λ η. sim_def.adv_P1 η msgs σ D)"
proof-
have "sim_def.adv_P1 η msgs σ D ≤ ddh.advantage η (R1_inter_adversary η D msgs) + ddh.advantage η (inter_S1_adversary η D msgs)"
for η
using security_P1 by simp
moreover have "negligible (λ η. ddh.advantage η (R1_inter_adversary η D msgs) + ddh.advantage η (inter_S1_adversary η D msgs))"
using assms
by (simp add: negligible_plus)
ultimately show ?thesis
using negligible_le sim_def.adv_P1_def by auto
qed
theorem security_P2_asymp:
assumes "m0 ∈ carrier (𝒢 η)" "m1 ∈ carrier (𝒢 η)"
shows "sim_def.perfect_sec_P2 η (m0,m1) σ"
by(simp add: security_P2 assms)
end
end