diff --git a/examples/global-hybrid/GlobalHybridExamp1.ec b/examples/global-hybrid/GlobalHybridExamp1.ec index a19cb5228..b091b24ba 100644 --- a/examples/global-hybrid/GlobalHybridExamp1.ec +++ b/examples/global-hybrid/GlobalHybridExamp1.ec @@ -13,6 +13,10 @@ require import AllCore Real Distr StdOrder StdBigop GlobalHybrid. import RealOrder Bigreal BRA. +clone include GlobalHybrid with + type input <- unit (* no additional input *) +proof *. + op n : {int | 1 <= n} as ge1_n. type t. (* we want t to have 2 ^ n elements, including def *) @@ -24,13 +28,13 @@ op [lossless] dt : t distr. axiom mu1_dt (x : t) : mu1 dt x = 1%r / (2 ^ n)%r. lemma dt_uni : is_uniform dt. -proof. move => x y _ _; by rewrite !mu1_dt. qed. +proof. by move => x y _ _; by rewrite !mu1_dt. qed. lemma dt_fu : is_full dt. proof. rewrite funi_ll_full. -move => x y; by rewrite !mu1_dt. -rewrite dt_ll. ++ by move => x y; by rewrite !mu1_dt. +by rewrite dt_ll. qed. op m : {int | 1 <= m} as ge1_m. @@ -65,7 +69,7 @@ lemma GReal_GIdeal &m : *) module Hybrid : HYBRID = { - proc main(i : int) : bool = { + proc main(y : unit, i : int) : bool = { var b <- true; var x : t; (* start from i: *) @@ -81,18 +85,18 @@ module Hybrid : HYBRID = { }. lemma GReal_Hybrid_1 &m : - Pr[GReal.main() @ &m : res] = Pr[Hybrid.main(1) @ &m : res]. + Pr[GReal.main() @ &m : res] = Pr[Hybrid.main((), 1) @ &m : res]. proof. byequiv => //; proc. seq 2 1 : (={b, i} /\ i{1} = 1); first auto. -sim. +by sim. qed. lemma Hybrid_m &m : - Pr[Hybrid.main(m) @ &m : res] = Pr[GIdeal.main() @ &m : res]. + Pr[Hybrid.main((), m) @ &m : res] = Pr[GIdeal.main() @ &m : res]. proof. byequiv => //; proc; sp 1 0. -rcondf{1} 1; auto. +by rcondf{1} 1; auto. qed. (* we use upto bad reasoning *) @@ -147,31 +151,35 @@ module GBad2 = { lemma Hybrid_step (i' : int) &m : 1 <= i' < m => - `|Pr[Hybrid.main(i') @ &m : res] - Pr[Hybrid.main(i' + 1) @ &m : res]| <= + `|Pr[Hybrid.main((), i') @ &m : res] - + Pr[Hybrid.main((), i' + 1) @ &m : res]| <= 1%r / (2 ^ n)%r. proof. -move => [ge1_i' lt_i'_m]. -have -> : Pr[Hybrid.main(i') @ &m : res] = Pr[GBad1.main(i') @ &m : res]. - byequiv => //; proc; sp 1 2. +move => [ge1_i' lt_i'_m]. +have -> : + Pr[Hybrid.main((), i') @ &m : res] = Pr[GBad1.main(i') @ &m : res]. ++ byequiv => //; proc; sp 1 2. rcondt{1} 1; first auto. - sim. -have -> : Pr[Hybrid.main(i' + 1) @ &m : res] = Pr[GBad2.main(i') @ &m : res]. - byequiv => //; proc; sp 1 2. + by sim. +have -> : + Pr[Hybrid.main((), i' + 1) @ &m : res] = + Pr[GBad2.main(i') @ &m : res]. ++ byequiv => //; proc; sp 1 2. seq 0 3 : (={i, b}); first auto. - sim. + by sim. rewrite (ler_trans Pr[GBad2.main(i') @ &m : GBad2.bad]). -byequiv - (_ : - ={i} ==> GBad1.bad{1} = GBad2.bad{2} /\ (! GBad2.bad{2} => ={res})) : - GBad1.bad => //. -proc. -seq 5 5 : - (GBad1.bad{1} = GBad2.bad{2} /\ ={i} /\ - (!GBad2.bad{2} => ={b})); first auto. -case (GBad1.bad{1}). -while (={i}); auto. -while (={i, b}); auto; smt(). -smt(). ++ byequiv + (_ : + ={i} ==> GBad1.bad{1} = GBad2.bad{2} /\ (! GBad2.bad{2} => ={res})) : + GBad1.bad => //. + + proc. + seq 5 5 : + (GBad1.bad{1} = GBad2.bad{2} /\ ={i} /\ + (!GBad2.bad{2} => ={b})); first auto. + case (GBad1.bad{1}). + + by while (={i}); auto. + by while (={i, b}); auto; smt(). + by smt(). byphoare => //; proc; sp. seq 3 : GBad2.bad @@ -179,14 +187,14 @@ seq 3 : 1%r (1%r - (1%r / (2 ^ n)%r)) 0%r. -auto. -wp; rnd (pred1 def); auto; smt(mu1_dt). -conseq (_ : _ ==> _ : = 1%r). -while (true) (m - i) => [z |]. -auto; smt(dt_ll). -auto; smt(). -hoare; while (true); auto. -trivial. ++ by auto. ++ by wp; rnd (pred1 def); auto; smt(mu1_dt). ++ conseq (_ : _ ==> _ : = 1%r). + while (true) (m - i) => [z |]. + + by auto; smt(dt_ll). + by auto; smt(). ++ by hoare; while (true); auto. +done. qed. lemma GReal_GIdeal &m : @@ -194,6 +202,6 @@ lemma GReal_GIdeal &m : (m - 1)%r * (1%r / (2 ^ n)%r). proof. rewrite (GReal_Hybrid_1 &m) -(Hybrid_m &m). -rewrite (hybrid_simp _ _ Hybrid) 1:ge1_m => i ge1_i_lt_m. +rewrite (hybrid_simp _ _ _ Hybrid) 1:ge1_m => i ge1_i_lt_m. by rewrite Hybrid_step. qed. diff --git a/examples/global-hybrid/GlobalHybridExamp2.ec b/examples/global-hybrid/GlobalHybridExamp2.ec index 89a74d337..7ff2426e6 100644 --- a/examples/global-hybrid/GlobalHybridExamp2.ec +++ b/examples/global-hybrid/GlobalHybridExamp2.ec @@ -1,49 +1,45 @@ (* GlobalHybridExamp2.ec *) -(* We use theories/crypto/GlobalHybrid.ec for an example where the - cost of each hybrid step is an instance of the Decisional - Diffie-Hellman (DDH) assumption. *) +(* We use theories/crypto/GlobalHybrid.ec for an example involving the + Decisional Diffie-Hellman (DDH) assumption, expressing security + as an equality. *) -require import AllCore Real Distr DBool StdOrder StdBigop GlobalHybrid. +require import AllCore Real Distr DBool StdOrder StdBigop. require import FMap PROM. import RealOrder Bigreal BRA. +require GlobalHybrid. + +theory DDH. + +type input. (* additional input *) (* group of keys *) type key. op (^^) : key -> key -> key. (* binary operation *) - -op kid : key. (* identity *) - -op kinv : key -> key. (* inverse *) +op kid : key. (* identity *) +op kinv : key -> key. (* inverse *) axiom kmulA (x y z : key) : x ^^ y ^^ z = x ^^ (y ^^ z). - -axiom kid_l (x : key) : kid ^^ x = x. - -axiom kid_r (x : key) : x ^^ kid = x. - -axiom kinv_l (x : key) : kinv x ^^ x = kid. - -axiom kinv_r (x : key) : x ^^ kinv x = kid. +axiom kid_l (x : key) : kid ^^ x = x. +axiom kid_r (x : key) : x ^^ kid = x. +axiom kinv_l (x : key) : kinv x ^^ x = kid. +axiom kinv_r (x : key) : x ^^ kinv x = kid. (* commutative semigroup of exponents *) type exp. -op e : exp. (* some exponent *) - +op e : exp. (* some exponent *) op ( * ) : exp -> exp -> exp. (* multiplication *) -axiom mulC (q r : exp) : q * r = r * q. - +axiom mulC (q r : exp) : q * r = r * q. axiom mulA (q r s : exp) : q * r * s = q * (r * s). op [full uniform lossless] dexp : exp distr. -op g : key. (* generator *) - +op g : key. (* generator *) op (^) : key -> exp -> key. (* exponentiation *) axiom double_exp_gen (q1 q2 : exp) : (g ^ q1) ^ q2 = g ^ (q1 * q2). @@ -51,31 +47,89 @@ axiom double_exp_gen (q1 q2 : exp) : (g ^ q1) ^ q2 = g ^ (q1 * q2). (* DDH Adversary *) module type DDH_ADV = { - proc main(k1 k2 k3 : key) : bool + proc main(i : input, k1 k2 k3 : key) : bool }. (* the real DDH game *) module DDH1 (Adv : DDH_ADV) = { - proc main() : bool = { + proc main(i : input) : bool = { var b : bool; var q1, q2 : exp; q1 <$ dexp; q2 <$ dexp; - b <@ Adv.main(g ^ q1, g ^ q2, g ^ (q1 * q2)); + b <@ Adv.main(i, g ^ q1, g ^ q2, g ^ (q1 * q2)); return b; } }. - + (* the ideal DDH game *) module DDH2 (Adv : DDH_ADV) = { - proc main() : bool = { + proc main(i : input) : bool = { var b : bool; var q1, q2, q3 : exp; q1 <$ dexp; q2 <$ dexp; q3 <$ dexp; - b <@ Adv.main(g ^ q1, g ^ q2 , g ^ q3); + b <@ Adv.main(i, g ^ q1, g ^ q2 , g ^ q3); return b; } }. +end DDH. + +(* group of keys *) + +type key. + +op (^^) : key -> key -> key. (* binary operation *) +op kid : key. (* identity *) +op kinv : key -> key. (* inverse *) + +axiom kmulA (x y z : key) : x ^^ y ^^ z = x ^^ (y ^^ z). +axiom kid_l (x : key) : kid ^^ x = x. +axiom kid_r (x : key) : x ^^ kid = x. +axiom kinv_l (x : key) : kinv x ^^ x = kid. +axiom kinv_r (x : key) : x ^^ kinv x = kid. + +(* commutative semigroup of exponents *) + +type exp. + +op e : exp. (* some exponent *) +op ( * ) : exp -> exp -> exp. (* multiplication *) + +axiom mulC (q r : exp) : q * r = r * q. +axiom mulA (q r s : exp) : q * r * s = q * (r * s). + +op [full uniform lossless] dexp : exp distr. + +op g : key. (* generator *) +op (^) : key -> exp -> key. (* exponentiation *) + +axiom double_exp_gen (q1 q2 : exp) : (g ^ q1) ^ q2 = g ^ (q1 * q2). + +clone import DDH as DDH' with + type input <- int, (* note *) + type key <- key, + type exp <- exp, + op (^^) <- (^^), + op kid <- kid, + op kinv <- kinv, + op e <- e, + op ( * ) <- ( * ), + op dexp <- dexp, + op g <- g, + op (^) <- (^) +proof *. +realize kmulA. apply kmulA. qed. +realize kid_l. apply kid_l. qed. +realize kid_r. apply kid_r. qed. +realize kinv_l. apply kinv_l. qed. +realize kinv_r. apply kinv_r. qed. +realize mulC. apply mulC. qed. +realize mulA. apply mulA. qed. +realize dexp_ll. apply dexp_ll. qed. +realize dexp_uni. apply dexp_uni. qed. +realize dexp_fu. apply dexp_fu. qed. +realize double_exp_gen. apply double_exp_gen. qed. + (* the real and ideal games let an adversary call an oracle m times before the returned results return a default value *) @@ -92,20 +146,16 @@ module OrReal : OR = { var ctr : int var x, y : exp - proc init() : unit = { - ctr <- 0; - } + proc init() : unit = { ctr <- 1; } proc get() : key * key * key = { var r : key * key * key; - if (ctr < m) { + if (ctr <= m) { x <$ dexp; y <$ dexp; r <- (g ^ x, g ^ y, g ^ (x * y)); ctr <- ctr + 1; } - else { - r <- witness; - } + else { r <- witness; } return r; } }. @@ -115,21 +165,17 @@ module OrReal : OR = { module OrIdeal : OR = { var ctr : int - proc init() : unit = { - ctr <- 0; - } + proc init() : unit = { ctr <- 1; } proc get() : key * key * key = { var r : key * key * key; var x, y, z : exp; - if (ctr < m) { + if (ctr <= m) { x <$ dexp; y <$ dexp; z <$ dexp; r <- (g ^ x, g ^ y, g ^ z); ctr <- ctr + 1; } - else { - r <- witness; - } + else { r <- witness; } return r; } }. @@ -165,7 +211,7 @@ module GIdeal(Adv : ADV) = { (* our reduction to DDH *) module Reduct(Adv : ADV) : DDH_ADV = { - var i : int (* needs to be a global to support game hoping *) + var i : int var u, v, w : key module Or = { @@ -176,75 +222,82 @@ module Reduct(Adv : ADV) : DDH_ADV = { proc get() : key * key * key = { var r : key * key * key; var x, y, z : exp; - if (ctr < m) { - if (ctr + 1 < i) { + if (ctr <= m) { + if (ctr < i) { x <$ dexp; y <$ dexp; z <$ dexp; r <- (g ^ x, g ^ y, g ^ z); } - elif (ctr + 1 = i) { - r <- (u, v, w); - } + elif (ctr = i) { r <- (u, v, w); } else { x <$ dexp; y <$ dexp; r <- (g ^ x, g ^ y, g ^ (x * y)); } ctr <- ctr + 1; } - else { - r <- witness; - } + else { r <- witness; } return r; } } - proc main(u' : key, v' : key, w' : key) : bool = { - var b : bool; - Or.ctr <- 0; - u <- u'; v <- v'; w <- w'; + proc main(i' : int, u' : key, v' : key, w' : key) : bool = { + var b : bool; var x : unit; + Or.ctr <- 1; + i <- i'; u <- u'; v <- v'; w <- w'; b <@ Adv(Or).disting(); return b; } }. -(* the reduction composed with DDH1 *) - -module DDH1Reduct(Adv : ADV) = { - proc main(i : int) : bool = { - var b : bool; - Reduct.i <- i; (* so value of Reduct.i in memory irrelevant *) - b <@ DDH1(Reduct(Adv)).main(); - return b; - } -}. - -(* the reduction composed with DDH2 *) - -module DDH2Reduct(Adv : ADV) = { - proc main(i : int) : bool = { - var b : bool; - Reduct.i <- i; (* so value of Reduct.i in memory irrelevant *) - b <@ DDH2(Reduct(Adv)).main(); - return b; - } -}. - -(* our goal is to prove: +(* We will prove security with an exact upper bound: lemma GReal_GIdeal (Adv <: ADV{-OrReal, -OrIdeal, -Reduct}) &m : `|Pr[GReal(Adv).main() @ &m : res] - - Pr[GIdeal(Adv).main() @ &m : res]| <= - bigi predT - (fun i => - `|Pr[DDH1Reduct(Adv).main(i) @ &m : res] - - Pr[DDH2Reduct(Adv).main(i) @ &m : res]|) - 1 (m + 1). + Pr[GIdeal(Adv).main() @ &m : res]| = + m%r * + `|bigi predT + (fun (i : int) => + Pr[DDH1(Reduct(Adv)).main(i) @ &m : res] / m%r) + 1 (m + 1) - + bigi predT + (fun (i : int) => + Pr[DDH2(Reduct(Adv)).main(i) @ &m : res] / m%r) + 1 (m + 1)|. *) section. +local clone GlobalHybrid as GH with + type input <- unit +proof *. + +local clone GH.Param as GHP with + type or_input <- unit, + type or_output <- key * key * key +proof *. + declare module Adv <: ADV{-OrReal, -OrIdeal, -Reduct}. -local module Hybrid : HYBRID = { +local module DDHOr1 : GHP.OR = { (* real *) + proc init() : unit = { } + + proc f() : key * key * key = { + var x, y : exp; + x <$ dexp; y <$ dexp; + return (g ^ x, g ^ y, g ^ (x * y)); + } +}. + +local module DDHOr2 : GHP.OR = { (* ideal *) + proc init() : unit = { } + + proc f() : key * key * key = { + var x, y, z : exp; + x <$ dexp; y <$ dexp; z <$ dexp; + return (g ^ x, g ^ y, g ^ z); + } +}. + +local module (Hybrid : GHP.HYBRID_PARAM) (GHOr : GHP.OR) = { var i : int module Or = { @@ -257,68 +310,94 @@ local module Hybrid : HYBRID = { proc get() : key * key * key = { var r : key * key * key; var x, y, z : exp; - if (ctr < m) { - if (ctr + 1 < i) { + if (ctr <= m) { + if (ctr < i) { x <$ dexp; y <$ dexp; z <$ dexp; (* ideal *) r <- (g ^ x, g ^ y, g ^ z); } + elif (ctr = i) { r <@ GHOr.f(); } else { x <$ dexp; y <$ dexp; (* real *) r <- (g ^ x, g ^ y, g ^ (x * y)); } ctr <- ctr + 1; } - else { - r <- witness; - } + else { r <- witness; } return r; } } (* i' should be between 1 and m + 1 *) - proc main(i' : int) : bool = { + proc main(x : unit, i' : int) : bool = { var b : bool; - i <- i'; Or.ctr <- 0; + i <- i'; Or.ctr <- 1; b <@ Adv(Or).disting(); return b; } }. local lemma GReal_Hybrid &m : - Pr[GReal(Adv).main() @ &m : res] = Pr[Hybrid.main(1) @ &m : res]. + Pr[GReal(Adv).main() @ &m : res] = + Pr[GHP.Exper(Hybrid, DDHOr1).main((), 1) @ &m : res]. proof. -byequiv => //; proc; inline. -seq 1 2 : +byequiv => //; proc; inline; wp. +seq 1 4 : (={glob Adv} /\ OrReal.ctr{1} = Hybrid.Or.ctr{2} /\ - OrReal.ctr{1} = 0 /\ Hybrid.i{2} = 1); first auto. + OrReal.ctr{1} = 1 /\ Hybrid.i{2} = 1); first auto. call - (_ : + (: OrReal.ctr{1} = Hybrid.Or.ctr{2} /\ - 0 <= OrReal.ctr{1} <= m /\ Hybrid.i{2} = 1). -proc; if => //. + 1 <= OrReal.ctr{1} <= m + 1 /\ Hybrid.i{2} = 1); + last auto; smt(ge1_m). +proc; if => //; last auto; smt(ge1_m). rcondf{2} 1; first auto; smt(). -auto; smt(). -auto. -auto; smt(ge1_m). +by if{2}; [inline{2} 1; auto; smt() | auto; smt()]. qed. local lemma Hybrid_GIdeal &m : - Pr[Hybrid.main(m + 1) @ &m : res] = Pr[GIdeal(Adv).main() @ &m : res]. + Pr[GHP.Exper(Hybrid, DDHOr1).main((), m + 1) @ &m : res] = + Pr[GIdeal(Adv).main() @ &m : res]. proof. -byequiv => //; proc; inline. -seq 2 1 : +byequiv => //; proc; inline; wp. +seq 4 1 : (={glob Adv} /\ Hybrid.Or.ctr{1} = OrIdeal.ctr{2} /\ - OrIdeal.ctr{2} = 0 /\ Hybrid.i{1} = m + 1); first auto. + OrIdeal.ctr{2} = 1 /\ Hybrid.i{1} = m + 1); first auto. call - (_ : + (: Hybrid.Or.ctr{1} = OrIdeal.ctr{2} /\ - 0 <= OrIdeal.ctr{2} <= m /\ Hybrid.i{1} = m + 1). -proc; if => //. + 0 <= OrIdeal.ctr{2} <= m + 1 /\ Hybrid.i{1} = m + 1); + last auto; smt(ge1_m). +proc; if => //; last auto. rcondt{1} 1; first auto; smt(). -auto; smt(). -auto. -auto; smt(ge1_m). +by auto; smt(). +qed. + +local lemma Hybrid_step (j : int) &m : + 1 <= j <= m => + Pr[GHP.Exper(Hybrid, DDHOr2).main((), j) @ &m : res] = + Pr[GHP.Exper(Hybrid, DDHOr1).main((), j + 1) @ &m : res]. +proof. +move => j_rng; byequiv => //; proc; inline; wp. +seq 4 4 : + (Hybrid.i{1} = j /\ Hybrid.i{2} = j + 1 /\ + Hybrid.Or.ctr{1} = 1 /\ ={glob Adv, Hybrid.Or.ctr}); + first auto. +call + (: + ={Hybrid.Or.ctr} /\ Hybrid.i{1} = j /\ + Hybrid.i{2} = j + 1 /\ 1 <= Hybrid.Or.ctr{1} <= m + 1); + last auto; smt(). +proc. +if => //; last auto. +if{1}. ++ rcondt{2} 1; first auto; smt(). + by auto; smt(). +if{1}. ++ rcondt{2} 1; first auto; smt(). + by inline{1} 1; auto; smt(). +rcondf{2} 1; first auto; smt(). +by if{2}; [inline{2} 1; auto; smt() | auto; smt()]. qed. (* in our sequences of games, we need to shift from lazy to eager @@ -330,19 +409,18 @@ local clone FullRO with type in_t <- ro_in_t, type out_t <- exp, op dout <- fun _ => dexp, - type d_in_t <- unit, + type d_in_t <- int, type d_out_t <- bool proof *. (* first, the sequence of games proving: - 1 <= i < m + 1 => Reduct.i{m} = i => - Pr[Hybrid.main(i) @ &m : res] = - Pr[DDH1(Reduct(Adv)).main() @ &m : res] *) + 1 <= i < m + 1 => + Pr[GHP.Exper(Hybrid, DDHOr1).main((), i) @ &m : res] = + Pr[DDH1(Reduct(Adv)).main((), i) @ &m : res]. *) local module (RO_Disting1 : FullRO.RO_Distinguisher) (RO : FullRO.RO) = { var i : int - var u, v, w : key module Or = { var ctr : int @@ -352,12 +430,12 @@ local module (RO_Disting1 : FullRO.RO_Distinguisher) (RO : FullRO.RO) = { proc get() : key * key * key = { var r : key * key * key; var x, y, z : exp; - if (ctr < m) { - if (ctr + 1 < i) { + if (ctr <= m) { + if (ctr < i) { x <$ dexp; y <$ dexp; z <$ dexp; r <- (g ^ x, g ^ y, g ^ z); } - elif (ctr + 1 = i) { + elif (ctr = i) { x <@ RO.get(A); y <@ RO.get(B); r <- (g ^ x, g ^ y, g ^ (x * y)); } @@ -367,136 +445,130 @@ local module (RO_Disting1 : FullRO.RO_Distinguisher) (RO : FullRO.RO) = { } ctr <- ctr + 1; } - else { - r <- witness; - } + else { r <- witness; } return r; } } - proc distinguish() : bool = { + proc distinguish(i' : int) : bool = { var b : bool; - Or.ctr <- 0; - RO.sample(A); RO.sample(B); RO.sample(C); + i <- i'; Or.ctr <- 1; + RO.sample(A); RO.sample(B); b <@ Adv(Or).disting(); return b; } }. -local lemma Hybrid_MainD_RO_Disting1_RO (i : int) : - 1 <= i < m + 1 => +local lemma Hybrid_DDHOr1_MainD_RO_Disting1_RO (i' : int) : + 1 <= i' < m + 1 => equiv - [Hybrid.main ~ + [GHP.Exper(Hybrid, DDHOr1).main ~ FullRO.MainD(RO_Disting1, FullRO.RO).distinguish : - ={glob Adv} /\ i'{1} = i /\ RO_Disting1.i{2} = i ==> + ={glob Adv} /\ i{1} = i' /\ x{2} = i' ==> ={res}]. proof. -move => [ge1_i le_i_m]; rewrite ltzS in le_i_m. +move => [ge1_i' le_i'_m]; rewrite ltzS in le_i'_m. transitivity - FullRO.MainD(RO_Disting1, FullRO.LRO).distinguish - (={glob Adv} /\ i'{1} = i /\ RO_Disting1.i{2} = i ==> ={res}) - (={glob Adv} /\ ={glob RO_Disting1} ==> ={res}) => //. -progress. -by exists (glob Adv){2} arg{1} RO_Disting1.u{2} RO_Disting1.v{2} - RO_Disting1.w{2} RO_Disting1.Or.ctr{2}. -proc; inline*; wp. -seq 2 6 : - (={glob Adv} /\ Hybrid.i{1} = i /\ RO_Disting1.i{2} = i /\ - Hybrid.Or.ctr{1} = 0 /\ RO_Disting1.Or.ctr{2} = 0 /\ - FullRO.RO.m{2} = empty); first auto. -call - (_ : - Hybrid.Or.ctr{1} = RO_Disting1.Or.ctr{2} /\ - 0 <= Hybrid.Or.ctr{1} <= m /\ - Hybrid.i{1} = i /\ RO_Disting1.i{2} = i /\ - (Hybrid.Or.ctr{1} + 1 <= i => FullRO.RO.m{2} = empty)). -proc; if => //. -case (Hybrid.Or.ctr{1} + 1 = Hybrid.i{1}). -rcondf{1} 1; first auto. -rcondf{2} 1; first auto; smt(). -rcondt{2} 1; first auto. -wp; inline*. -swap{2} 2 -1; swap{2} 6 -4. -seq 2 3 : - (#pre /\ x{1} = r0{2} /\ y{1} = r1{2} /\ - x0{2} = A); first auto. -rcondt{2} 1; first auto; smt(mem_empty). -sp 0 3. -rcondt{2} 1; first auto; smt(mem_set mem_empty). -auto; smt(get_set_sameE). -if => //; first auto; smt(). -rcondf{2} 1; first auto. -auto; smt(). -auto. -auto. -smt(ge1_m). + FullRO.MainD(RO_Disting1, FullRO.LRO).distinguish + (={glob Adv} /\ i{1} = i' /\ x{2} = i' ==> ={res}) + (={glob RO_Disting1, x} ==> ={res}) => //; first smt(). ++ proc; inline*; wp. + seq 4 6 : + (={glob Adv} /\ Hybrid.i{1} = i' /\ RO_Disting1.i{2} = i' /\ + Hybrid.Or.ctr{1} = 1 /\ RO_Disting1.Or.ctr{2} = 1 /\ + FullRO.RO.m{2} = empty); first auto. + call + (: + Hybrid.Or.ctr{1} = RO_Disting1.Or.ctr{2} /\ + 1 <= Hybrid.Or.ctr{1} <= m + 1 /\ + Hybrid.i{1} = i' /\ RO_Disting1.i{2} = i' /\ + (Hybrid.Or.ctr{1} <= i' => FullRO.RO.m{2} = empty)); + last auto; smt(). + proc. + if => //; last auto. + if => //; first auto; smt(). + if => //; last auto; smt(). + inline*; swap{2} 2 -1; swap{2} 6 -4. + seq 2 3 : + (#pre /\ x0{1} = r0{2} /\ y0{1} = r1{2} /\ + x0{2} = A); first auto. + rcondt{2} 1; first auto; smt(mem_empty). + sp 0 3. + rcondt{2} 1; first auto; smt(mem_set mem_empty). + by auto; smt(get_set_sameE). symmetry. conseq (FullRO.FullEager.RO_LRO RO_Disting1 _) => //. -move => _; apply dexp_ll. +by move => _; apply dexp_ll. qed. -local lemma MainD_RO_Disting1_RO_DDH1_Reduct : +local lemma MainD_RO_Disting1_RO_DDH1_Reduct (i' : int) : + 1 <= i' < m + 1 => equiv [FullRO.MainD(RO_Disting1, FullRO.RO).distinguish ~ DDH1(Reduct(Adv)).main : - ={glob Adv} /\ RO_Disting1.i{1} = Reduct.i{2} ==> + ={glob Adv} /\ x{1} = i' /\ i{2} = i' ==> ={res}]. proof. -proc; inline*; wp. -swap{1} 6 -5; swap{1} 10 -8; swap{1} 14 -11. -seq 15 9 : - (={glob Adv} /\ RO_Disting1.i{1} = Reduct.i{2} /\ +move => [ge1_i' le_i'_m]; rewrite ltzS in le_i'_m. +proc; inline*; wp; swap{1} 7 -6; swap{1} 11 -9. +seq 2 2 : (#pre /\ r0{1} = q1{2} /\ r1{1} = q2{2}); + first auto. +seq 10 9 : + (={glob Adv} /\ + RO_Disting1.i{1} = i' /\ Reduct.i{2} = i' /\ RO_Disting1.Or.ctr{1} = Reduct.Or.ctr{2} /\ FullRO.RO.m{1}.[A] = Some q1{2} /\ FullRO.RO.m{1}.[B] = Some q2{2} /\ Reduct.u{2} = g ^ q1{2} /\ Reduct.v{2} = g ^ q2{2} /\ Reduct.w{2} = g ^ (q1{2} * q2{2})). -wp => /=; rnd{1}; rnd; rnd. -auto; smt(get_setE mem_set mem_empty). ++ by auto; smt(get_setE mem_set mem_empty). exlim q1{2}, q2{2} => q1_R q2_R. call - (_ : - RO_Disting1.i{1} = Reduct.i{2} /\ + (: + RO_Disting1.i{1} = i' /\ + Reduct.i{2} = i' /\ RO_Disting1.Or.ctr{1} = Reduct.Or.ctr{2} /\ FullRO.RO.m{1}.[A] = Some q1_R /\ FullRO.RO.m{1}.[B] = Some q2_R /\ Reduct.u{2} = g ^ q1_R /\ Reduct.v{2} = g ^ q2_R /\ - Reduct.w{2} = g ^ (q1_R * q2_R)). -proc; if => //. -if => //; first auto. -if => //. -wp; inline*; auto; smt(get_setE). -auto. -auto. -auto. + Reduct.w{2} = g ^ (q1_R * q2_R)); last auto. +proc. +if => //; last auto. +if => //; first auto; smt(). +if => //; last auto. +inline*. +rcondf{1} 3; first auto; smt(). +rcondf{1} 6; first auto; smt(). +by auto; smt(). qed. -local lemma Hybrid_DDH1_Reduct (i : int) &m : - 1 <= i < m + 1 => Reduct.i{m} = i => - Pr[Hybrid.main(i) @ &m : res] = - Pr[DDH1(Reduct(Adv)).main() @ &m : res]. +local lemma reduct1 (i' : int) &m : + 1 <= i' < m + 1 => + Pr[GHP.Exper(Hybrid, DDHOr1).main((), i') @ &m : res] = + Pr[DDH1(Reduct(Adv)).main(i') @ &m : res]. proof. -move => i_bnd Reduct_i_eq_i. -byequiv (_ : ={glob Adv} /\ i'{1} = i /\ Reduct.i{2} = i ==> _) => //. +move => i'_rng. +byequiv + (: ={glob Adv} /\ i{1} = i' /\ i{2} = i' ==> _) => //. transitivity FullRO.MainD(RO_Disting1, FullRO.RO).distinguish - (={glob Adv} /\ i'{1} = i /\ RO_Disting1.i{2} = i ==> ={res}) - (={glob Adv} /\ RO_Disting1.i{1} = Reduct.i{2} ==> ={res}) => //. -progress; by exists (glob Adv){2} arg{1}. -by apply Hybrid_MainD_RO_Disting1_RO. + (={glob Adv} /\ i{1} = i' /\ x{2} = i' ==> ={res}) + (={glob Adv} /\ x{1} = i' /\ i{2} = i' ==> ={res}) => //. +by smt(). +by apply Hybrid_DDHOr1_MainD_RO_Disting1_RO. by apply MainD_RO_Disting1_RO_DDH1_Reduct. qed. -(* next the sequence of games proving: - 1 <= i < m + 1 => Reduct.i{m} = i => - Pr[Hybrid.main(i + 1) @ &m : res] = - Pr[DDH2(Reduct(Adv)).main() @ &m : res] *) +(* second, the sequence of games proving: + + 1 <= i < m + 1 => + Pr[GHP.Exper(Hybrid, DDHOr2).main((), i) @ &m : res] = + Pr[DDH2(Reduct(Adv)).main((), i) @ &m : res]. *) local module (RO_Disting2 : FullRO.RO_Distinguisher) (RO : FullRO.RO) = { var i : int - var u, v, w : key module Or = { var ctr : int @@ -506,12 +578,12 @@ local module (RO_Disting2 : FullRO.RO_Distinguisher) (RO : FullRO.RO) = { proc get() : key * key * key = { var r : key * key * key; var x, y, z : exp; - if (ctr < m) { - if (ctr + 1 < i) { + if (ctr <= m) { + if (ctr < i) { x <$ dexp; y <$ dexp; z <$ dexp; r <- (g ^ x, g ^ y, g ^ z); } - elif (ctr + 1 = i) { + elif (ctr = i) { x <@ RO.get(A); y <@ RO.get(B); z <@ RO.get(C); r <- (g ^ x, g ^ y, g ^ z); } @@ -521,84 +593,80 @@ local module (RO_Disting2 : FullRO.RO_Distinguisher) (RO : FullRO.RO) = { } ctr <- ctr + 1; } - else { - r <- witness; - } + else { r <- witness; } return r; } } - proc distinguish() : bool = { + proc distinguish(i' : int) : bool = { var b : bool; - Or.ctr <- 0; + i <- i'; Or.ctr <- 1; RO.sample(A); RO.sample(B); RO.sample(C); b <@ Adv(Or).disting(); return b; } }. -local lemma Hybrid_MainD_RO_Disting2_RO (i : int) : - 1 <= i < m + 1 => +local lemma Hybrid_DDHOr2_MainD_RO_Disting2_RO (i' : int) : + 1 <= i' < m + 1 => equiv - [Hybrid.main ~ + [GHP.Exper(Hybrid, DDHOr2).main ~ FullRO.MainD(RO_Disting2, FullRO.RO).distinguish : - ={glob Adv} /\ i'{1} = i + 1 /\ RO_Disting2.i{2} = i ==> + ={glob Adv} /\ i{1} = i' /\ x{2} = i' ==> ={res}]. proof. -move => [ge1_i le_i_m]; rewrite ltzS in le_i_m. +move => [ge1_i' le_i'_m]; rewrite ltzS in le_i'_m. transitivity - FullRO.MainD(RO_Disting2, FullRO.LRO).distinguish - (={glob Adv} /\ i'{1} = i + 1 /\ RO_Disting2.i{2} = i ==> ={res}) - (={glob Adv} /\ ={glob RO_Disting2} ==> ={res}) => //. -progress. -by exists (glob Adv){2} RO_Disting2.i{2} RO_Disting2.u{2} RO_Disting2.v{2} - RO_Disting2.w{2} RO_Disting2.Or.ctr{2}. -proc; inline*; wp. -seq 2 6 : - (={glob Adv} /\ Hybrid.i{1} = i + 1 /\ RO_Disting2.i{2} = i /\ - Hybrid.Or.ctr{1} = 0 /\ RO_Disting2.Or.ctr{2} = 0 /\ - FullRO.RO.m{2} = empty); first auto. -call - (_ : - Hybrid.Or.ctr{1} = RO_Disting2.Or.ctr{2} /\ - 0 <= Hybrid.Or.ctr{1} <= m /\ - Hybrid.i{1} = i + 1 /\ RO_Disting2.i{2} = i /\ - (Hybrid.Or.ctr{1} + 1 <= i => FullRO.RO.m{2} = empty)). -proc; if => //. -if{1}. -if{2}; first auto; smt(). -rcondt{2} 1; first auto; smt(). -wp; inline*; swap{2} 2 -1; swap{2} 6 -4; swap{2} 10 -7. -seq 3 4 : - (#pre /\ x{1} = r0{2} /\ y{1} = r1{2} /\ z{1} = r2{2} /\ - x0{2} = A); first auto. -rcondt{2} 1; first auto; smt(mem_empty). -sp 0 3. -rcondt{2} 1; first auto; smt(mem_set mem_empty). -sp 0 3. -rcondt{2} 1; first auto; smt(mem_set mem_empty). -auto; smt(get_set_sameE). -rcondf{2} 1; first auto; smt(). -rcondf{2} 1; first auto; smt(). -auto; smt(). -auto. -auto; smt(ge1_m). + FullRO.MainD(RO_Disting2, FullRO.LRO).distinguish + (={glob Adv} /\ i{1} = i' /\ x{2} = i' ==> ={res}) + (={glob RO_Disting2, x} ==> ={res}) => //; first smt(). ++ proc; inline*; wp. + seq 4 7 : + (={glob Adv} /\ Hybrid.i{1} = i' /\ RO_Disting2.i{2} = i' /\ + Hybrid.Or.ctr{1} = 1 /\ RO_Disting2.Or.ctr{2} = 1 /\ + FullRO.RO.m{2} = empty); first auto. + call + (: + Hybrid.Or.ctr{1} = RO_Disting2.Or.ctr{2} /\ + 1 <= Hybrid.Or.ctr{1} <= m + 1 /\ + Hybrid.i{1} = i' /\ RO_Disting2.i{2} = i' /\ + (Hybrid.Or.ctr{1} <= i' => FullRO.RO.m{2} = empty)); + last auto; smt(). + proc. + if => //; last auto. + if => //; first auto; smt(). + if => //; last auto; smt(). + inline*; swap{2} 2 -1; swap{2} 6 -4; swap{2} 10 -7. + seq 3 4 : + (#pre /\ x0{1} = r0{2} /\ y0{1} = r1{2} /\ + z0{1} = r2{2} /\ x0{2} = A); first auto. + rcondt{2} 1; first auto; smt(mem_empty). + sp 0 3. + rcondt{2} 1; first auto; smt(mem_set mem_empty). + sp 0 3. + rcondt{2} 1; first auto; smt(mem_set mem_empty). + auto; smt(get_set_sameE). symmetry. conseq (FullRO.FullEager.RO_LRO RO_Disting2 _) => //. -move => _; apply dexp_ll. +by move => _; apply dexp_ll. qed. -local lemma MainD_RO_Disting2_RO_DDH2_Reduct : +local lemma MainD_RO_Disting2_RO_DDH2_Reduct (i' : int) : + 1 <= i' < m + 1 => equiv [FullRO.MainD(RO_Disting2, FullRO.RO).distinguish ~ DDH2(Reduct(Adv)).main : - ={glob Adv} /\ RO_Disting2.i{1} = Reduct.i{2} ==> + ={glob Adv} /\ x{1} = i' /\ i{2} = i' ==> ={res}]. proof. -proc; inline*; wp. -swap{1} 6 -5; swap{1} 10 -8; swap{1} 14 -11. -seq 15 10 : - (={glob Adv} /\ RO_Disting2.i{1} = Reduct.i{2} /\ +move => [ge1_i' le_i'_m]; rewrite ltzS in le_i'_m. +proc; inline*; wp; swap{1} 7 -6; swap{1} 11 -9; swap{1} 15 -12. +seq 3 3 : + (#pre /\ r0{1} = q1{2} /\ r1{1} = q2{2} /\ + r2{1} = q3{2}); first auto. +seq 13 9 : + (={glob Adv} /\ + RO_Disting2.i{1} = i' /\ Reduct.i{2} = i' /\ RO_Disting2.Or.ctr{1} = Reduct.Or.ctr{2} /\ FullRO.RO.m{1}.[A] = Some q1{2} /\ FullRO.RO.m{1}.[B] = Some q2{2} /\ @@ -606,100 +674,93 @@ seq 15 10 : Reduct.u{2} = g ^ q1{2} /\ Reduct.v{2} = g ^ q2{2} /\ Reduct.w{2} = g ^ q3{2}). -wp => /=; rnd; rnd; rnd. -auto; smt(get_setE mem_set mem_empty). ++ auto; smt(get_setE mem_set mem_empty). exlim q1{2}, q2{2}, q3{2} => q1_R q2_R q3_R. call - (_ : - RO_Disting2.i{1} = Reduct.i{2} /\ + (: + RO_Disting2.i{1} = i' /\ + Reduct.i{2} = i' /\ RO_Disting2.Or.ctr{1} = Reduct.Or.ctr{2} /\ FullRO.RO.m{1}.[A] = Some q1_R /\ FullRO.RO.m{1}.[B] = Some q2_R /\ FullRO.RO.m{1}.[C] = Some q3_R /\ Reduct.u{2} = g ^ q1_R /\ Reduct.v{2} = g ^ q2_R /\ - Reduct.w{2} = g ^ q3_R). -proc; if => //. -if => //; first auto. -if => //; first wp; inline*; auto; smt(get_setE). -auto. -auto. -auto. + Reduct.w{2} = g ^ q3_R); last auto. +proc. +if => //; last auto. +if => //; first auto; smt(). +if => //; last auto. +inline*. +rcondf{1} 3; first auto; smt(). +rcondf{1} 6; first auto; smt(). +rcondf{1} 9; first auto; smt(). +by auto; smt(). qed. -local lemma Hybrid_DDH2_Reduct (i : int) &m : - 1 <= i < m + 1 => Reduct.i{m} = i => - Pr[Hybrid.main(i + 1) @ &m : res] = - Pr[DDH2(Reduct(Adv)).main() @ &m : res]. +local lemma reduct2 (i' : int) &m : + 1 <= i' < m + 1 => + Pr[GHP.Exper(Hybrid, DDHOr2).main((), i') @ &m : res] = + Pr[DDH2(Reduct(Adv)).main(i') @ &m : res]. proof. -move => i_bnd H. -byequiv (_ : ={glob Adv} /\ i'{1} = i + 1 /\ Reduct.i{2} = i ==> _) => //. +move => i'_rng. +byequiv + (: ={glob Adv} /\ i{1} = i' /\ i{2} = i' ==> _) => //. transitivity FullRO.MainD(RO_Disting2, FullRO.RO).distinguish - (={glob Adv} /\ i'{1} = i + 1 /\ RO_Disting2.i{2} = i ==> ={res}) - (={glob Adv} /\ RO_Disting2.i{1} = Reduct.i{2} ==> ={res}) => //. -progress; by exists (glob Adv){2} Reduct.i{2}. -by apply (Hybrid_MainD_RO_Disting2_RO i). + (={glob Adv} /\ i{1} = i' /\ x{2} = i' ==> ={res}) + (={glob Adv} /\ x{1} = i' /\ i{2} = i' ==> ={res}) => //. +by smt(). +by apply Hybrid_DDHOr2_MainD_RO_Disting2_RO. by apply MainD_RO_Disting2_RO_DDH2_Reduct. qed. -local lemma Hybrid_DDH1Reduct (i' : int) &m : - 1 <= i' < m + 1 => - Pr[Hybrid.main(i') @ &m : res] = - Pr[DDH1Reduct(Adv).main(i') @ &m : res]. -proof. -move => ge1_i'_lt_m_plus1. -rewrite eq_sym. -byphoare (_ : i = i' /\ glob Adv = (glob Adv){m} ==> _) => //. -proc; sp. -call (_ : Reduct.i = i' /\ (glob Adv) = (glob Adv){m} ==> res). -bypr => &n [] Reduct_i_n_eq_i' eq_glob_n_m. -rewrite -(Hybrid_DDH1_Reduct i' &n) => //. -byequiv => //; sim. -auto. -qed. - -local lemma Hybrid_DDH2Reduct (i' : int) &m : - 1 <= i' < m + 1 => - Pr[Hybrid.main(i' + 1) @ &m : res] = - Pr[DDH2Reduct(Adv).main(i') @ &m : res]. -proof. -move => ge1_i'_lt_m_plus1. -rewrite eq_sym. -byphoare (_ : i = i' /\ glob Adv = (glob Adv){m} ==> _) => //. -proc; sp. -call (_ : Reduct.i = i' /\ (glob Adv) = (glob Adv){m} ==> res). -bypr => &n [] Reduct_i_n_eq_i' eq_glob_n_m. -rewrite -(Hybrid_DDH2_Reduct i' &n) => //. -byequiv => //; sim. -auto. -qed. - lemma GReal_GIdeal_sect &m : `|Pr[GReal(Adv).main() @ &m : res] - - Pr[GIdeal(Adv).main() @ &m : res]| <= - bigi predT - (fun i => - `|Pr[DDH1Reduct(Adv).main(i) @ &m : res] - - Pr[DDH2Reduct(Adv).main(i) @ &m : res]|) - 1 (m + 1). + Pr[GIdeal(Adv).main() @ &m : res]| = + m%r * + `|bigi predT + (fun (i : int) => + Pr[DDH1(Reduct(Adv)).main(i) @ &m : res] / m%r) + 1 (m + 1) - + bigi predT + (fun (i : int) => + Pr[DDH2(Reduct(Adv)).main(i) @ &m : res] / m%r) + 1 (m + 1)|. proof. -rewrite GReal_Hybrid -Hybrid_GIdeal (hybrid_gen _ _ Hybrid _ _ _). -smt(ge1_m). -move => i bnd_i /=. -by rewrite Hybrid_DDH1Reduct // Hybrid_DDH2Reduct. +rewrite GReal_Hybrid -Hybrid_GIdeal. +rewrite (GHP.hybrid_param () (m + 1) DDHOr1 DDHOr2 Hybrid) /=. ++ by smt(ge1_m). ++ move => i i_rng; rewrite Hybrid_step /#. +rewrite + (eq_big_int _ _ + (fun (j : int) => + Pr[GHP.Exper(Hybrid, DDHOr1).main(tt, j) @ &m : res] / m%r) + (fun (i : int) => + Pr[DDH1(Reduct(Adv)).main(i) @ &m : res] / m%r)). ++ by move => i i_rng /=; rewrite reduct1. +rewrite + (eq_big_int _ _ + (fun (j : int) => + Pr[GHP.Exper(Hybrid, DDHOr2).main(tt, j) @ &m : res] / m%r) + (fun (i : int) => + Pr[DDH2(Reduct(Adv)).main(i) @ &m : res] / m%r)). ++ by move => i i_rng /=; rewrite reduct2. +done. qed. end section. lemma GReal_GIdeal (Adv <: ADV{-OrReal, -OrIdeal, -Reduct}) &m : `|Pr[GReal(Adv).main() @ &m : res] - - Pr[GIdeal(Adv).main() @ &m : res]| <= - bigi predT - (fun i => - `|Pr[DDH1Reduct(Adv).main(i) @ &m : res] - - Pr[DDH2Reduct(Adv).main(i) @ &m : res]|) - 1 (m + 1). -proof. -apply (GReal_GIdeal_sect Adv). -qed. + Pr[GIdeal(Adv).main() @ &m : res]| = + m%r * + `|bigi predT + (fun (i : int) => + Pr[DDH1(Reduct(Adv)).main(i) @ &m : res] / m%r) + 1 (m + 1) - + bigi predT + (fun (i : int) => + Pr[DDH2(Reduct(Adv)).main(i) @ &m : res] / m%r) + 1 (m + 1)|. +proof. by apply (GReal_GIdeal_sect Adv). qed. diff --git a/theories/crypto/GlobalHybrid.ec b/theories/crypto/GlobalHybrid.ec index ee33aa395..9ce5c05c0 100644 --- a/theories/crypto/GlobalHybrid.ec +++ b/theories/crypto/GlobalHybrid.ec @@ -1,68 +1,163 @@ (* GlobalHybrid.ec *) -(*^ Consider a module `M` with a `bool`-returning procedure `main` - taking an integer `i` as its argument. We consider the result of - calling `M` with argument `i`, where `i` is in the range `1 .. n` - inclusive, for `n >= 1`, to be the `i`th __global hybrid__, - global because its entire behavior, and not just that of an oracle - it may use, can be a function of `i`. - - This theory provides lemmas for upper bounding the absolute value - of the difference of the probabilities of the first and last - hybrids returning true, given upper bounds on the absolute values - of the probability differences for each of the steps, as a function - of `i`. -^*) - -require import AllCore Real StdOrder StdBigop. +(*^ This theory proves several lemmas about __global__ hybrids, + hybrids whose entire behavior, not just that of any oracles they + may use, can be a function of the hybrid index `i`. + + We have a lemma based on the triangular inequality, where the + overall upper bound is the sum of the bounds of the individual + steps, as well as the specialization of this to the case where + each step's bound is the same. + + And we have a lemma for hybrids parameterized by an oracle + that gives an equality, not just an upper bound, assuming + a natural precondition holds. This lemma is adapted + from the Nominal-SSProve paper "Mechanizing Nested Hybrid Arguments", + https://eprint.iacr.org/2025/1122 ^*) + +require import AllCore Real StdOrder StdBigop Distr. import RealOrder Bigreal BRA. +(*& Type of additional input. &*) + +type input. + (*& Module type of global hybrids. &*) module type HYBRID = { - (* i is the index of the hybrid, starting from 1 *) - proc main(i : int) : bool + (* i is the index of the hybrid, starting from 1 + x is an additional input *) + proc main(x : input, i : int) : bool }. (*& General global hybrid lemma; the bound for each step is a function of the index. &*) -lemma hybrid_gen (n : int) (p : int -> real) (M <: HYBRID) &m : +lemma hybrid_gen (x : input) (n : int) (p : int -> real) (M <: HYBRID) &m : 1 <= n => (forall (i : int), - 1 <= i < n => - `|Pr[M.main(i) @ &m : res] - Pr[M.main(i + 1) @ &m : res]| <= p i) => - `|Pr[M.main(1) @ &m : res] - Pr[M.main(n) @ &m : res]| <= + 1 <= i < n => + `|Pr[M.main(x, i) @ &m : res] - Pr[M.main(x, i + 1) @ &m : res]| <= p i) => + `|Pr[M.main(x, 1) @ &m : res] - Pr[M.main(x, n) @ &m : res]| <= bigi predT p 1 n. proof. move => ge1_n step. have ind : forall (i : int), 0 <= i => 1 <= i <= n => - `|Pr[M.main(1) @ &m : res] - Pr[M.main(i) @ &m : res]| <= bigi predT p 1 i. - elim => [// | i ge0_i IH [_ i_plus1_le_n]]. + `|Pr[M.main(x, 1) @ &m : res] - + Pr[M.main(x, i) @ &m : res]| <= bigi predT p 1 i. ++ elim => [// | i ge0_i IH [_ i_plus1_le_n]]. case (i = 0) => [-> /= |]. - by rewrite ger0_norm // big_geq. + + by rewrite ger0_norm // big_geq. rewrite -lt0n // ltzE /= => ge1_i. rewrite big_int_recr //. rewrite (ler_trans - (`|Pr[M.main(1) @ &m : res] - Pr[M.main(i) @ &m : res]| + - `|Pr[M.main(i) @ &m : res] - Pr[M.main(i + 1) @ &m : res]|)). - rewrite RealOrder.ler_dist_add. - rewrite ler_add 1:IH 1:/# step /#. + (`|Pr[M.main(x, 1) @ &m : res] - + Pr[M.main(x, i) @ &m : res]| + + `|Pr[M.main(x, i) @ &m : res] - + Pr[M.main(x, i + 1) @ &m : res]|)). + + by rewrite RealOrder.ler_dist_add. + by rewrite ler_add 1:IH 1:/# step /#. by rewrite ind // (IntOrder.ler_trans 1). qed. (*& Simple global hybrid lemma; the bound for each step is a constant. &*) -lemma hybrid_simp (n : int) (p : real) (M <: HYBRID) &m : +lemma hybrid_simp (x : input) (n : int) (p : real) (M <: HYBRID) &m : 1 <= n => (forall (i : int), - 1 <= i < n => - `|Pr[M.main(i) @ &m : res] - Pr[M.main(i + 1) @ &m : res]| <= p) => - `|Pr[M.main(1) @ &m : res] - Pr[M.main(n) @ &m : res]| <= (n - 1)%r * p. + 1 <= i < n => + `|Pr[M.main(x, i) @ &m : res] - + Pr[M.main(x, i + 1) @ &m : res]| <= p) => + `|Pr[M.main(x, 1) @ &m : res] - + Pr[M.main(x, n) @ &m : res]| <= (n - 1)%r * p. proof. move => ge1_n step. -have HG := hybrid_gen n (fun _ => p) M &m _ _ => //. +have HG := hybrid_gen x n (fun _ => p) M &m _ _ => //. by rewrite Bigreal.sumri_const in HG. qed. + +(*& Hybrids parameterized by an oracle. &*) + +theory Param. + +(*& Types of oracle inputs. &*) + +type or_input. + +(*& Types of oracle outputs. &*) + +type or_output. + +(*& Oracle module type. &*) + +module type OR = { + proc init() : unit + proc f(x : or_input) : or_output +}. + +(*& Parameterized hybrid module type. &*) + +module type HYBRID_PARAM (Or : OR) = { + (* i is the index of the hybrid, starting from 1 + x is an additional input *) + proc main(x : input, i : int) : bool {Or.f} +}. + +(*& Parameterized hybrid experiment. &*) + +module Exper(M : HYBRID_PARAM, Or : OR) = { + proc main(x : input, i : int) : bool = { + var b : bool; + Or.init(); + b <@ M(Or).main(x, i); + return b; + } +}. + +(*& Parameterized hybrid lemma. &*) + +lemma hybrid_param (x : input) (n : int) (Or1 <: OR) (Or2 <: OR) + (M <: HYBRID_PARAM) &m : + 1 < n => + (forall (i : int), + 1 <= i < n => + Pr[Exper(M, Or2).main(x, i) @ &m : res] = + Pr[Exper(M, Or1).main(x, i + 1) @ &m : res]) => + `|Pr[Exper(M, Or1).main(x, 1) @ &m : res] - + Pr[Exper(M, Or1).main(x, n) @ &m : res]| = (* also Or1 *) + (n - 1)%r * + `|bigi predT + (fun (j : int) => Pr[Exper(M, Or1).main(x, j) @ &m : res] / (n - 1)%r) + 1 n - + bigi predT + (fun (j : int) => Pr[Exper(M, Or2).main(x, j) @ &m : res] / (n - 1)%r) + 1 n|. +proof. +move => gt1_n steps. +rewrite + (telescoping_sum + (fun i => Pr[Exper(M, Or1).main(x, i) @ &m : res])) 1:/# /=. +rewrite + (eq_big_int _ _ _ + (fun (i : int) => + Pr[Exper(M, Or1).main(x, i) @ &m : res] - + Pr[Exper(M, Or2).main(x, i) @ &m : res]) _). ++ by move => i i_rng /=; rewrite -steps. +rewrite big_split -sumrN. +rewrite -normrZ 1:/# RField.mulrC RField.mulrBl 2!mulr_suml /=. +have -> : + (fun (i : int) => + Pr[Exper(M, Or1).main(x, i) @ &m : res] * (n - 1)%r / (n - 1)%r) = + (fun (i : int) => Pr[Exper(M, Or1).main(x, i) @ &m : res]). ++ by apply fun_ext => i; rewrite -RField.mulrA Num.Domain.divrr /#. +have -> : + (fun (i : int) => + Pr[Exper(M, Or2).main(x, i) @ &m : res] * (n - 1)%r / (n - 1)%r) = + (fun (i : int) => Pr[Exper(M, Or2).main(x, i) @ &m : res]). ++ by apply fun_ext => i; rewrite -RField.mulrA Num.Domain.divrr /#. +done. +qed. + +end Param.