proposition: Lemma compute_key_bij: ∀ (m : chMap pid (chProd public choiceTranscript1)) (i j: pid), (i != j)%ord → exists (a b : nat), (a != 0)%N /\ (a < q)%N /\ (∀ (x : Secret) zk, compute_key (setm m j (fto (g ^+ x), zk)) i = g ^+ ((a * x + b) %% q)).
proof: Proof. intros m i j ne. simpl. pose low := \prod_(k <- domm m :\ j| (k < i)%ord) get_value m k. pose hi := \prod_(k <- domm m :\ j| (i < k)%ord) get_value m k. have Hlow : exists ilow, low = g ^+ ilow by apply expg_g. have Hhi : exists ihi, hi = g ^+ ihi by apply expg_g. destruct Hlow as [ilow Hlow]. destruct Hhi as [ihi Hhi]. have getv_remm_eq : forall P j m, \prod_(k <- domm m :\ j | P k) get_value (remm m j) k = \prod_(k <- domm m :\ j | P k) get_value m k. { clear low hi ilow ihi Hlow Hhi ne i j m. intros. rewrite big_seq_cond. rewrite [RHS] big_seq_cond. erewrite eq_bigr. 1: done. intros k. move => /andP [k_in _]. simpl. unfold get_value. rewrite remmE. case (k == j) eqn:eq. ++ move: eq => /eqP eq. rewrite eq in_fsetD1 in k_in. move: k_in => /andP [contra]. rewrite eq_refl in contra. discriminate. ++ reflexivity. } case (j < i)%ord eqn:ij_rel. - exists 1%N. exists (ilow + (ihi * #[g ^+ ihi].-1))%N. do 2 split. 1: rewrite q_order_g ; apply (prime_gt1 prime_order). intros x zk. rewrite compute_key'_equiv. 2: assumption. unfold compute_key'. simpl. rewrite ij_rel. rewrite domm_rem. set low' := \prod_(k0 <- _ | _) _. set hi' := \prod_(k0 <- _ | _) _. have -> : low' = low by apply getv_remm_eq. have -> : hi' = hi by apply getv_remm_eq. clear low' hi'. rewrite Hhi Hlow. rewrite invg_expg. rewrite -!expgM. rewrite -!expgD. rewrite !addnA. rewrite -expg_mod_order. f_equal. f_equal. 2: { unfold q. rewrite Fp_cast; [reflexivity | apply prime_order]. } rewrite mul1n. done. - exists #[g].-1. exists (ilow + (ihi * #[g ^+ ihi].-1))%N. repeat split. { unfold negb. rewrite -leqn0. case (#[g].-1 <= 0)%N eqn:e. 2: done. have Hgt1 := (prime_gt1 prime_order). rewrite -ltn_predRL in Hgt1. rewrite -ltnS in Hgt1. rewrite -addn1 in Hgt1. rewrite leq_add2l in Hgt1. eapply leq_trans in e. 2: apply Hgt1. discriminate. } { rewrite q_order_g. rewrite ltn_predL. apply (prime_gt0 prime_order). } intros x zk. rewrite compute_key'_equiv. 2: assumption. unfold compute_key'. simpl. rewrite ij_rel. rewrite domm_rem. set low' := \prod_(k0 <- _ | _) _. set hi' := \prod_(k0 <- _ | _) _. have -> : low' = low by apply getv_remm_eq. have -> : hi' = hi by apply getv_remm_eq. clear low' hi'. rewrite Hhi Hlow. rewrite invMg. rewrite -expgVn. rewrite !invg_expg. rewrite -!expgM. rewrite mulgA. rewrite -!expgD. rewrite !addnA. rewrite -expg_mod_order. f_equal. f_equal. 2: { unfold q. rewrite Fp_cast; [reflexivity | apply prime_order]. } rewrite addnAC. rewrite addnC. rewrite addnA. done. Qed.
imports: Relational(OrderEnrichedCategory GenericRulesSimple) mathcomp(all_ssreflect all_algebra reals distr realsum fingroup.fingroup solvable.cyclic prime ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice seq) Crypt(Axioms ChoiceAsOrd SubDistr Couplings UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb UniformStateProb pkg_composition Package Prelude SigmaProtocol Schnorr DDH) Coq(Utf8 Lia) extructures(ord fset fmap) Equations(Equations)