Skip to content

Commit

Permalink
Correctness bound
Browse files Browse the repository at this point in the history
  • Loading branch information
@mbbarbosa-lectures
mbbarbosa-lectures committed Nov 3, 2023
1 parent 86998c3 commit c0e3672
Show file tree
Hide file tree
Showing 3 changed files with 205 additions and 5 deletions.
153 changes: 153 additions & 0 deletions proof/security/FO_Kyber.ec
View file
Original file line number Diff line number Diff line change
Expand Up @@ -96,6 +96,8 @@ module (FO_K : KEMROM.Scheme) (H : POracle) = {
}
}.

(* A modular version of the UU construction for moving samples *)

module UU_L(H1 : RO1.RO, H2 : RO2.RO) = {
include UU(RO_x2(H1,H2)) [kg, enc]
proc dec(sk : skey, c : ciphertext) : key option = {
Expand Down Expand Up @@ -123,6 +125,157 @@ module UU_L(H1 : RO1.RO, H2 : RO2.RO) = {
}
}.

(* CORRECTNESS PROOF *)

module Correctness_L(H1 : RO1.RO, H2 : RO2.RO) = {
proc main() : bool = {
var pk : pkey;
var sk : KEMROMx2.skey;
var c : ciphertext;
var k : key;
var k' : key option;
H1.init();
H2.init();
(pk, sk) <@ UU_L(H1,H2).kg();
(c, k) <@ UU_L(H1,H2).enc(pk);
k' <@ UU_L(H1,H2).dec(sk, c);

return k' <> Some k;
}
}.
lemma go_parametric_corr_lro &m :
Pr[KEMROMx2.Correctness(RO_x2(RO1.RO, RO2.RO), UU).main() @ &m : res] =
Pr[Correctness_L(RO1.LRO, RO2.LRO).main() @ &m : res].
proof.
byequiv => //.
proc.
conseq (: ={k,k'}); 1: by smt().
seq 1 2 : (={RO1.RO.m,RO2.RO.m}); 1: by inline *;sim.
seq 1 1 : (#pre /\ ={pk,sk}); 1: by sim.
seq 1 1 : (#pre /\ ={c,k}); 1: by sim.
inline {1} 1; inline {2} 1; inline {2} 5; inline {2} 6.
inline {1} 4;sp;if;1:by auto.
+ seq 1 1 : (#pre /\ ={r}); 1: by inline *;auto => />.
by sp;if;[by auto | |];inline *;auto => /> /#.
by sp;if;[by auto | |];inline *;auto => /> /#.
qed.


module (DC1 : KEMROMx2.RO1.RO_Distinguisher) (G1 : RO1.RO) = {
proc distinguish = Correctness_L(G1, RO2.LRO).main
}.

module (DC2 : KEMROMx2.RO2.RO_Distinguisher) (G2 : RO2.RO) = {
proc distinguish = Correctness_L(RO1.RO, G2).main
}.

lemma go_parametric_corr &m :
Pr[KEMROMx2.Correctness(RO_x2(RO1.RO, RO2.RO), UU).main() @ &m : res] =
Pr[Correctness_L(RO1.RO, RO2.RO).main() @ &m : res].
proof.
rewrite go_parametric_corr_lro.
have -> : Pr[Correctness_L(RO1.LRO, RO2.LRO).main() @ &m : res] =
Pr[KEMROMx2.RO1.MainD(DC1,RO1.LRO).distinguish() @ &m : res]
by byequiv => //;proc; inline {2} 2;wp;conseq />;inline *;sim.

have -> : Pr[Correctness_L(RO1.RO, RO2.RO).main() @ &m : res] =
Pr[KEMROMx2.RO2.MainD(DC2,RO2.RO).distinguish() @ &m : res]
by byequiv => //;proc; inline {2} 2;wp;conseq />;inline *;sim.

have -> : Pr[KEMROMx2.RO2.MainD(DC2,RO2.RO).distinguish() @ &m : res] =
Pr[KEMROMx2.RO2.MainD(DC2,RO2.LRO).distinguish() @ &m : res].
byequiv (: ={RO1.RO.m, arg} ==> ={res, RO1.RO.m}) => //.
apply(RO2.FullEager.RO_LRO (DC2) _).
by move => *;rewrite dkey_ll.

have <- : Pr[KEMROMx2.RO1.MainD(DC1,RO1.RO).distinguish() @ &m : res] =
Pr[KEMROMx2.RO1.MainD(DC1,RO1.LRO).distinguish() @ &m : res].
+ byequiv (: ={RO2.RO.m, arg} ==> ={res, RO2.RO.m}) => //.
apply(RO1.FullEager.RO_LRO (DC1) _).
by move => *;rewrite randd_ll.

byequiv => //;proc;inline {1} 2; inline {2} 2.
by sim.
qed.

(* FIXME: THIS FACTOR OF 2 IS TO AVOID A LOSSLESS GOAL IN THE TOP LEVEL
INSTANTIATION DUE TO THE RANGE SAMPLING OF THE TT REDUCTION.
THIS ALSO IMPACTS CARD BY 1 *)
lemma correctness_fo_k &m :
qHC = 1 =>
2<FinT.card =>
Pr[ KEMROM.Correctness(RO.RO,FO_K).main() @ &m : res ] <=
2%r * Pr[ Correctness_Adv(BasePKE, B(B_UC, PKEROM.RO.RO)).main() @ &m : res].
move => qHC_0 card2.
have := Top.UU.correctness &m qHC_0 card2.
have -> : Pr[KEMROMx2.Correctness(RO_x2(RO1.RO, RO2.RO), UU).main() @ &m : res] =
Pr[Correctness(RO.RO, FO_K).main() @ &m : res]; last by smt().
rewrite go_parametric_corr.
byequiv => //.
proc.
inline {1} 4; inline {2} 3.
swap {1} [3..5] -2; swap {2} [2..4] -1.
seq 3 3 : (={pk,sk,m,pk0} /\ pk0{1} = pk{2}
/\ sk{1}.`1.`1 = pk{2}); 1 : by inline *;auto.
inline {1} 3; inline {2} 2.
swap {1} 8 -2.
seq 6 5 : (#pre /\ m0{1} = m{2} /\ pk1{1} = pk0{2} /\
m{1} \in RO1.RO.m{1} /\ ={r,k0} /\
m{1} \in RO2.RO.m{1} /\
(pkh pk{2},m{2}) \in RO.RO.m{2} /\
oget RO.RO.m{2}.[(pkh pk{2},m{2})] =
(oget RO1.RO.m{1}.[m{1}],oget RO2.RO.m{1}.[m{1}]) /\
r{1} = oget RO1.RO.m{1}.[m{1}] /\
k0{1} = oget RO2.RO.m{1}.[m{1}] /\
(r{2},k0{2}) = oget RO.RO.m{2}.[(pkh pk{2},m{2})] /\
fdom RO1.RO.m{1} = fset1 m{1} /\
fdom RO2.RO.m{1} = fset1 m{1} /\
fdom RO.RO.m{2} = fset1 (pkh pk{2}, m{2})).
+ inline *; swap {1} 6 -5; swap {1} 10 -8; swap {2} 3 -2.
seq 2 1 : (#pre /\ r0{1} = r0{2}.`1 /\ r1{1} = r0{2}.`2).
+ conseq />;rndsem{1} 0;rnd;auto => />.
have -> : (dlet randd (fun (r1_0 : randomness) => dmap dkey
(fun (r0_0 : key) => (r1_0, r0_0)))) = randd `*` dkey; last by smt().
rewrite dprod_dlet; congr;apply fun_ext => r.
by rewrite dlet_dunit.
by auto => />;smt(get_setE mem_set mem_empty @SmtMap @FSet).

seq 1 1 : (#pre /\ c1{1} = c0{2}); 1: by auto => /#.

sp;inline {1} 1; inline {2} 1;sp.
inline {1} 2; inline {1} 1;inline {1} 4; inline {1} 2;inline {2} 1.
swap {1} 3 -2; swap {1} 7 -5; swap {2} 2 -1.
seq 2 1 : (#pre /\ r2{1} = r2{2}.`1 /\ r1{1} = r2{2}.`2).
+ conseq />;rndsem{1} 0;rnd;auto => />.
have -> : (dlet randd (fun (r1_0 : randomness) => dmap dkey
(fun (r0_0 : key) => (r1_0, r0_0)))) = randd `*` dkey; last by smt().
rewrite dprod_dlet; congr;apply fun_ext => r.
by rewrite dlet_dunit.

case (m'{1} = None).
+ rcondf{1} 7; 1: by auto.
rcondt{1} 7; 1: by auto.
by auto => /> /#.
rcondt{1} 7; 1: by auto.
inline {1} 7.
rcondf{1} 9; 1: by auto => />;smt(mem_set).
swap {1} 8 -7; seq 1 0 : #pre; 1: by auto.
swap {2} 4 1.
seq 9 4 : (={c',sk0,m',k} /\ c2{1} = c1{2} /\ m'{1} <> None /\
RO2.RO.m{1}.[oget m'{1}] = Some ks{2}); last
by inline *;sp;if{1};auto => /> /#.
by auto => />;smt(mem_fdom in_fset1 get_setE).
qed.
(* SECURITY PROOF *)
module CCAL(H1 : RO1.RO, H2 : RO2.RO, A : KEMROMx2.CCA_ADV) = {
module O = {
proc dec(c : ciphertext) : key option = {
Expand Down
17 changes: 16 additions & 1 deletion proof/security/FO_UU.ec
View file
Original file line number Diff line number Diff line change
Expand Up @@ -119,7 +119,7 @@ module (B_UC : PKEROM.CORR_ADV) (HT : PKEROM.POracle)= {
}
}.

lemma correctness &m :
lemma correctness_rel &m :
Pr [ KEMROMx2.Correctness(RO_x2(RO1.RO,RO2.RO),UU).main() @ &m : res ] <=
Pr [ PKEROM.Correctness_Adv(PKEROM.RO.RO,TT,B_UC).main() @ &m : res ].
proof.
Expand All @@ -143,6 +143,21 @@ seq 1 1 : (#pre /\ m'{1} = m'{2});
by inline *;if{1};inline *;auto => />;smt(get_setE).
qed.

(* FIXME: THIS FACTOR OF 2 IS TO AVOID A LOSSLESS GOAL IN THE TOP LEVEL
INSTANTIATION DUE TO THE RANGE SAMPLING OF THE TT REDUCTION.
THIS ALSO IMPACTS CARD BY 1 *)
lemma correctness &m :
qHC = 1 =>
2<FinT.card =>
Pr[ KEMROMx2.Correctness(RO_x2(RO1.RO,RO2.RO),UU).main() @ &m : res ] <=
2%r * Pr[ Correctness_Adv(BasePKE, B(B_UC, PKEROM.RO.RO)).main() @ &m : res].
move => qHC_0 card2.
have := correctness B_UC &m _ _ _; 1: by smt().
+ by move => *; proc; auto => /#.
by move => *;islossless.
by smt(correctness_rel).
qed.

(* Security proof *)

module CountHx2(H : KEMROMx2.POracle_x2) = {
Expand Down
40 changes: 36 additions & 4 deletions proof/security/MLWE_PKE_Hash.ec
View file
Original file line number Diff line number Diff line change
Expand Up @@ -557,19 +557,51 @@ lemma correctness_theorem &m fail_prob :

end section.

section.

(* INSTANTIATION OF THE FO_K TRANSFORM *)

import UU.TT.PKEROM.
import UU.
declare module A <:
KEMROM.CCA_ADV{ -KEMROM.RO.RO.m, -OW_CPA, -BOWp, -OWL_CPA, -OWvsIND.Bowl, -RO.RO, -RO.FRO, -OW_PCVA, -TT.BasePKE, -TT.B, -TT.Correctness_Adv1, -TT.CountO, -TT.O_AdvOW, -TT.Gm, -RF.RF, -PseudoRF.PRF, -KEMROMx2.RO1.RO, -KEMROMx2.RO1.FRO, -KEMROMx2.RO2.RO, -KEMROMx2.RO2.FRO, -KEMROMx2.CCA, -CountHx2, -RO1E.FunRO, -UU2, -H2, -H2BOWMod, -Gm2, -Gm3, -KEMROM.CCA, -B1x2}.

local equiv kg_same :
equiv kg_same :
TT.BasePKE.kg ~ MLWE_PKE_HASH.kg : true ==> ={res}.
proc;rndsem {2} 0.
admit. (* FIXME: This should not be needed, as post does not mention r *)
qed.

(* correctness *)

(* FIXME: THIS FACTOR OF 2 IS TO AVOID A LOSSLESS GOAL IN THE TOP LEVEL
INSTANTIATION DUE TO THE RANGE SAMPLING OF THE TT REDUCTION.
THIS ALSO IMPACTS CARD BY 1 *)
lemma correctness &m fail_prob :
Pr[ CorrectnessBound.main() @ &m : res] <= fail_prob =>
TT.qHC = 1 =>
2 < TT.FinT.card =>

Pr[KEMROM.Correctness(KEMROM.RO.RO, FO_K).main() @ &m : res] <= 2%r * fail_prob.
proof.
move => cb qHC0 msp2.
have := (correctness_fo_k &m qHC0 msp2).
have -> : Pr[TT.PKE.Correctness_Adv(TT.BasePKE, TT.B(B_UC, RO.RO)).main() @ &m : res] =
Pr[TT.PKE.Correctness_Adv(MLWE_PKE_HASH, TT.B(B_UC, RO.RO)).main() @ &m : res].
+ byequiv => //;proc;seq 1 1 : (#pre /\ ={pk,sk});
1: by conseq />;call kg_same;auto => />.
by inline *;sim.

have := correctness_theorem (TT.B(B_UC, RO.RO)) &m fail_prob _ cb.
+ by islossless;smt(drange_ll).
by smt().
qed.

(* security *)

section.

declare module A <:
KEMROM.CCA_ADV{ -KEMROM.RO.RO.m, -OW_CPA, -BOWp, -OWL_CPA, -OWvsIND.Bowl, -RO.RO, -RO.FRO, -OW_PCVA, -TT.BasePKE, -TT.B, -TT.Correctness_Adv1, -TT.CountO, -TT.O_AdvOW, -TT.Gm, -RF.RF, -PseudoRF.PRF, -KEMROMx2.RO1.RO, -KEMROMx2.RO1.FRO, -KEMROMx2.RO2.RO, -KEMROMx2.RO2.FRO, -KEMROMx2.CCA, -CountHx2, -RO1E.FunRO, -UU2, -H2, -H2BOWMod, -Gm2, -Gm3, -KEMROM.CCA, -B1x2}.


module BUOOOWMod_Hx2 = CountH(B1x2(A, CountHx2(BUUOWMod(B1x2(A), TT.CountH(TT.H(TT.CO1(RO.RO))), TT.CountO(TT.G2_O(TT.CO1(RO.RO)))).H2B), KEMROMx2.CCA(CountHx2(BUUOWMod(B1x2(A), TT.CountH(TT.H(TT.CO1(RO.RO))), TT.CountO(TT.G2_O(TT.CO1(RO.RO)))).H2B), UU2, B1x2(A)).O).BH).
module BUOOOWMod_dec = KEMROMx2.CCA(CountHx2(BUUOWMod(B1x2(A), TT.CountH(TT.H(TT.CO1(RO.RO))), TT.CountO(TT.G2_O(TT.CO1(RO.RO)))).H2B), UU2, B1x2(A)).O.

Expand Down

0 comments on commit c0e3672

Please sign in to comment.