Commit 2713e452 authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen

Implement vote zero knowledge proof

This proof is based on the description given in the original open vote
network article. It verifies that the public vote is on the form
g^(x*y)*g^v for either v=0 or v=1, and where x corresponds to the secret
key sent in the first part of the protocol.

This also updates a few things so that the test keeps working.
Specifically, it changes the hash function used to be simple (insecure)
xor, as the encoding used before was causing major computational
isssues.
parent f6dacc26
Pipeline #19367 passed with stage
in 9 minutes and 59 seconds
......@@ -42,6 +42,7 @@ Class BoardroomAxioms {A : Type} :=
mul_proper :> Proper (elmeq ==> elmeq ==> elmeq) mul;
opp_proper :> Proper (elmeq ==> elmeq) opp;
inv_proper :> Proper (elmeq ==> elmeq) inv;
pow_base_proper :> Proper (elmeq ==> eq ==> elmeq) pow;
pow_exp_proper a :
~(elmeq a zero) -> Proper (expeq ==> elmeq) (pow a);
......@@ -76,6 +77,11 @@ Class BoardroomAxioms {A : Type} :=
~(elmeq a zero) ->
elmeq (pow a (e + e')) (mul (pow a e) (pow a e'));
pow_pow a b e :
~(elmeq a zero) ->
elmeq (pow (pow a b) e)
(pow a (b * e)%Z);
pow_nonzero a e :
~(elmeq a zero) ->
~(elmeq (pow a e) zero);
......@@ -564,6 +570,25 @@ Section WithBoardroomAxioms.
now intros ? ? <-.
Qed.
Global Instance elmeqb_elmeq_proper :
Proper (elmeq ==> elmeq ==> eq) elmeqb.
Proof.
intros x x' xeq y y' yeq.
destruct (elmeqb_spec x y), (elmeqb_spec x' y'); auto.
- contradiction n.
now rewrite <- xeq, <- yeq.
- contradiction n.
now rewrite xeq, yeq.
Qed.
Lemma elmeqb_refl a :
a =? a = true.
Proof.
destruct (elmeqb_spec a a); [easy|].
contradiction n.
reflexivity.
Qed.
Lemma bruteforce_tally_aux_correct result max :
Z.of_nat max < order - 1 ->
(result <= max)%nat ->
......@@ -573,13 +598,10 @@ Section WithBoardroomAxioms.
induction max as [|max IH].
- replace result with 0%nat by lia.
cbn.
destruct (elmeqb_spec (generator^0) (generator^0)); auto.
contradiction n; reflexivity.
now rewrite elmeqb_refl.
- destruct (Nat.eq_dec result (S max)) as [->|?].
+ cbn.
destruct (elmeqb_spec (generator ^ Z.pos (Pos.of_succ_nat max))
(generator ^ Z.pos (Pos.of_succ_nat max))); auto.
contradiction n; reflexivity.
now rewrite elmeqb_refl.
+ cbn -[Z.of_nat].
destruct (elmeqb_spec (generator ^ Z.of_nat (S max))
(generator ^ Z.of_nat result)) as [eq|?]; auto.
......@@ -962,6 +984,16 @@ Module Zp.
mod_pow_pos (a mod p) x p = mod_pow_pos a x p.
Proof. apply mod_pow_pos_aux_mod_idemp. Qed.
Lemma mod_pow_mod_idemp a e p :
mod_pow (a mod p) e p = mod_pow a e p.
Proof.
unfold mod_pow.
destruct e.
- now rewrite Z_pow_mod_idemp.
- now rewrite mod_pow_pos_mod_idemp.
- now rewrite mod_pow_pos_mod_idemp.
Qed.
Lemma mod_pow_pos_aux_mod a x p r :
mod_pow_pos_aux a x p r mod p = mod_pow_pos_aux a x p r.
Proof.
......@@ -1487,6 +1519,8 @@ Module Zp.
- intros a a' aeq.
cbn.
now rewrite <- mod_inv_mod_idemp, aeq, mod_inv_mod_idemp by auto.
- intros a a' aeq e ? <-.
now rewrite <- mod_pow_mod_idemp, aeq, mod_pow_mod_idemp.
- intros a anp e e' eeq.
rewrite <- (mod_pow_exp_mod _ e), <- (mod_pow_exp_mod _ e') by auto.
now rewrite eeq.
......@@ -1533,6 +1567,8 @@ Module Zp.
now rewrite mod_inv_mod_idemp.
- intros a e e' ap0.
now rewrite mod_pow_exp_plus by auto.
- intros a b e anz.
now rewrite mod_pow_exp_mul.
- auto.
- auto.
Defined.
......@@ -1708,6 +1744,9 @@ Module BigZp.
- intros a a' aeq.
autorewrite with zsimpl in *.
now rewrite <- Zp.mod_inv_mod_idemp, aeq, Zp.mod_inv_mod_idemp.
- intros a a' aeq e ? <-.
autorewrite with zsimpl in *.
now rewrite <- Zp.mod_pow_mod_idemp, aeq, Zp.mod_pow_mod_idemp.
- intros a anp e e' eeq.
autorewrite with zsimpl in *.
rewrite <- (Zp.mod_pow_exp_mod _ e), <- (Zp.mod_pow_exp_mod _ e') by auto.
......@@ -1770,6 +1809,9 @@ Module BigZp.
- intros a e e' ap0.
autorewrite with zsimpl in *.
now rewrite Zp.mod_pow_exp_plus by auto.
- intros a b e ap0.
autorewrite with zsimpl in *.
now rewrite Zp.mod_pow_exp_mul.
- intros a e ap0.
autorewrite with zsimpl in *.
auto.
......
......@@ -62,10 +62,13 @@ Record State :=
result : option nat;
}.
(* w, a1, b1, a2, b2, d1, d2 *)
Definition VoteProof := (Z * A * A * A * A * Z * Z * Z * Z)%type.
Inductive Msg :=
| signup (pk : A) (proof : A * Z)
| commit_to_vote (hash : positive)
| submit_vote (v : A) (proof : Z)
| submit_vote (v : A) (proof : VoteProof)
| tally_votes.
Global Instance VoterInfo_settable : Settable _ :=
......@@ -86,21 +89,6 @@ Global Instance State_serializable : Serializable State :=
Global Instance Msg_serializable : Serializable Msg :=
Derive Serializable Msg_rect<signup, commit_to_vote, submit_vote, tally_votes>.
Class VoteProofScheme :=
build_vote_proof_scheme {
make_vote_proof (pks : list A) (index : nat)
(secret_key : Z) (secret_vote : bool) : Z;
verify_vote (pks : list A) (index : nat) (public_vote : A) (proof : Z) : bool;
(*
verify_vote_spec pks index pv proof :
verify_vote pks index pv proof = true ->
exists sk sv, proof = make_vote_proof pks index sk sv;
*)
}.
Context `{VoteProofScheme}.
Import ContractMonads.
Local Open Scope broom.
......@@ -122,6 +110,41 @@ Definition verify_secret_key_proof (pk : A) (i : nat) (proof : A * Z) : bool :=
let z := Zpos (hash_sk_data gv pk i) in
elmeqb gv (generator^r * (pk^z)).
Definition hash_sv_data (i : nat) (pk rk a1 b1 a2 b2 : A) : positive :=
H (countable.encode i :: map countable.encode [pk; rk; a1; b1; a2; b2]).
Definition secret_vote_proof (sk : Z) (rk : A) (sv : bool) (i : nat) (w r d : Z) : VoteProof :=
let pk : A := compute_public_key sk in
let pv : A := compute_public_vote rk sk sv in
if sv then
let a1 : A := generator^r * pk^d in
let b1 : A := rk^r * pv^d in
let a2 : A := generator^w in
let b2 : A := rk^w in
let c := Zpos (hash_sv_data i pk rk a1 b1 a2 b2) in
let d2 := c - d in
let r2 := w - sk*d2 in
(w, a1, b1, a2, b2, d, d2, r, r2)
else
let a1 := generator^w in
let b1 := rk^w in
let a2 := generator^r * pk^d in
let b2 := rk^r * (pv * inv generator)^d in
let c := Zpos (hash_sv_data i pk rk a1 b1 a2 b2) in
let d1 := c - d in
let r1 := w - sk*d1 in
(w, a1, b1, a2, b2, d1, d, r1, r).
Local Open Scope bool.
Definition verify_secret_vote_proof (pk rk pv : A) (i : nat) (proof : VoteProof) : bool :=
let '(w, a1, b1, a2, b2, d1, d2, r1, r2) := proof in
let c := hash_sv_data i pk rk a1 b1 a2 b2 in
(Zpos c =? d1 + d2)%Z &&
(a1 =? generator^r1 * pk^d1)%broom &&
(b1 =? rk^r1 * pv^d1)%broom &&
(a2 =? generator^r2 * pk^d2)%broom &&
(b2 =? rk^r2 * (pv * inv generator)^d2)%broom.
Definition make_signup_msg (sk : Z) (v : Z) (i : nat) : Msg :=
signup (compute_public_key sk) (secret_key_proof sk v i).
......@@ -129,9 +152,9 @@ Definition make_commit_msg (pks : list A) (my_index : nat) (sk : Z) (sv : bool)
let pv := compute_public_vote (reconstructed_key pks my_index) sk sv in
commit_to_vote (H [countable.encode pv]).
Definition make_vote_msg (pks : list A) (my_index : nat) (sk : Z) (sv : bool) : Msg :=
submit_vote (compute_public_vote (reconstructed_key pks my_index) sk sv)
(make_vote_proof pks my_index sk sv).
Definition make_vote_msg (sk : Z) (rk : A) (sv : bool) (my_index : nat) (w r d : Z) : Msg :=
submit_vote (compute_public_vote rk sk sv)
(secret_vote_proof sk rk sv my_index w r d).
Definition init : ContractIniter Setup State :=
do owner <- lift caller_addr;
......@@ -180,7 +203,12 @@ Definition receive : ContractReceiver State Msg State :=
if (H [countable.encode v] =? vote_hash inf)%positive then Some tt else None
else
Some tt);
do lift (if verify_vote (public_keys state) (voter_index inf) v proof then Some tt else None);
do lift (if verify_secret_vote_proof
(nth (voter_index inf) (public_keys state) 0)
(reconstructed_key (public_keys state) (voter_index inf))
v
(voter_index inf)
proof then Some tt else None);
let inf := inf<|public_vote := v|> in
accept_call (state<|registered_voters ::= FMap.add caller inf|>)
......@@ -221,7 +249,7 @@ Proof with cbn -[Nat.ltb].
destruct (_ <? _)%nat; auto.
destruct (FMap.find _ _); auto.
destruct (finish_commit_by _); [destruct (_ =? _)%positive; auto|].
all: destruct (verify_vote _ _ _ _); auto.
all: destruct (verify_secret_vote_proof _ _ _ _); auto.
+ rewrite <- ceq.
destruct (_ <? _)%nat; auto.
destruct (result _); auto.
......@@ -231,27 +259,50 @@ Defined.
Section Theories.
Record SecretVoterInfo :=
build_secret_voter_info {
svi_index : nat;
(* Secret key *)
svi_sk : Z;
(* Chosen randomness for knowledge of secret key proof *)
svi_sk_r : Z;
(* Secret vot e*)
svi_sv : bool;
(* Chosen random w for vote proof *)
svi_sv_w : Z;
(* Chosen random r for vote proof *)
svi_sv_r : Z;
(* Chosen random d for vote proof *)
svi_sv_d : Z;
}.
Global Instance SecretVoterInfo_settable : Settable _ :=
settable! build_secret_voter_info <svi_index; svi_sk; svi_sk_r;
svi_sv; svi_sv_w; svi_sv_r; svi_sv_d>.
(* For correctness we assume that all signups and vote messages were
created using the make_signup_msg and make_vote_msg functions from
the contract *)
Fixpoint MsgAssumption
(pks : list A)
(index : Address -> nat)
(sks : Address -> Z)
(chosen_randomness : Address -> Z)
(svs : Address -> bool)
(parties : Address -> SecretVoterInfo)
(calls : list (ContractCallInfo Msg)) : Prop :=
match calls with
| call :: calls =>
let caller := Blockchain.call_from call in
let party := parties (Blockchain.call_from call) in
match Blockchain.call_msg call with
| Some (signup pk prf as m) => m = make_signup_msg (sks caller)
(chosen_randomness caller)
(index caller)
| Some (signup pk prf as m) => m = make_signup_msg (svi_sk party) (svi_sk_r party)
(svi_index party)
| Some (submit_vote _ _ as m) =>
m = make_vote_msg pks (index caller) (sks caller) (svs caller)
m = make_vote_msg (svi_sk party)
(reconstructed_key pks (svi_index party))
(svi_sv party)
(svi_index party)
(svi_sv_w party)
(svi_sv_r party)
(svi_sv_d party)
| _ => True
end /\ MsgAssumption pks index sks chosen_randomness svs calls
end /\ MsgAssumption pks parties calls
| [] => True
end.
......@@ -266,31 +317,11 @@ Definition signups (calls : list (ContractCallInfo Msg)) : list (Address * A) :=
order in which parties signed up in the contract. *)
Definition SignupOrderAssumption
(pks : list A)
(index : Address -> nat)
(parties : Address -> SecretVoterInfo)
(calls : list (ContractCallInfo Msg)) : Prop :=
All (fun '((addr, pk), i) => index addr = i /\ nth_error pks i = Some pk)
All (fun '((addr, pk), i) => svi_index (parties addr) = i /\ nth_error pks i = Some pk)
(zip (signups calls) (seq 0 (length (signups calls)))).
(*
Lemma voter_info_update (voters : FMap Address VoterInfo) index addr vi_before vi_after :
IndexAssumptions (FMap.add addr vi_after voters) index ->
FMap.find addr voters = Some vi_before ->
voter_index vi_before = voter_index vi_after ->
IndexAssumptions voters index.
Proof.
unfold IndexAssumptions in *.
intros index_assum inf index_same addr' inf' find_addr.
destruct (address_eqb_spec addr addr') as [->|].
- specialize (index_assum addr' vi_after).
replace inf' with vi_before in * by congruence.
rewrite index_same.
apply index_assum.
now rewrite FMap.find_add.
- apply index_assum.
rewrite FMap.find_add_ne by auto; congruence.
Qed.
*)
Local Open Scope nat.
Lemma no_outgoing bstate caddr :
......@@ -316,7 +347,7 @@ Proof.
+ destruct (_ <? _); cbn in *; try congruence.
destruct (FMap.find _ _); cbn in *; try congruence.
destruct (if finish_commit_by _ then _ else _); cbn in *; try congruence.
destruct (verify_vote _ _ _ _); cbn in *; try congruence.
destruct (verify_secret_vote_proof _ _ _ _); cbn in *; try congruence.
now inversion_clear receive_some.
+ destruct (_ <? _); cbn in *; try congruence.
destruct (result _); cbn in *; try congruence.
......@@ -355,21 +386,22 @@ Proof.
now rewrite index.
Qed.
Lemma all_signups pks index calls :
SignupOrderAssumption pks index calls ->
Lemma all_signups pks parties calls :
SignupOrderAssumption pks parties calls ->
length (signups calls) = length pks ->
map snd (signups calls) = pks.
Proof.
intros order len_signups.
unfold SignupOrderAssumption in order.
revert index pks len_signups order.
induction (signups calls) as [|[addr pk] xs IH]; intros index pks len_signups order.
revert parties pks len_signups order.
induction (signups calls) as [|[addr pk] xs IH]; intros parties pks len_signups order.
- destruct pks; cbn in *; congruence.
- cbn in *.
destruct pks as [|pk' pks]; cbn in *; try lia.
destruct order as [[index_eq nth_eq] all].
f_equal; try congruence.
apply (IH (fun addr => index addr - 1)); try lia.
apply (IH (fun addr => (parties addr)<|svi_index ::= fun i => i - 1|>));
[lia|].
clear -all.
rewrite <- (map_id xs) in all at 1.
rewrite <- seq_shift in all.
......@@ -393,6 +425,7 @@ Qed.
Hint Resolve
pow_nonzero generator_nonzero int_domain generator_nonzero compute_public_key_unit
reconstructed_key_unit
: broom.
Lemma verify_secret_key_proof_spec sk v i :
verify_secret_key_proof (compute_public_key sk) i (secret_key_proof sk v i) = true.
......@@ -419,6 +452,57 @@ Proof with auto with broom.
lia.
Qed.
Lemma verify_secret_vote_proof_spec sk pks sv i w r d :
All (fun pk => pk !== 0) pks ->
verify_secret_vote_proof
(compute_public_key sk)
(reconstructed_key pks i)
(compute_public_vote (reconstructed_key pks i) sk sv)
i
(secret_vote_proof sk (reconstructed_key pks i) sv i w r d) = true.
Proof.
intros all_units.
set (rk := reconstructed_key pks i).
unfold verify_secret_vote_proof, secret_vote_proof.
cbn.
destruct sv.
- set (h := hash_sv_data _ _ _ _ _ _ _).
rewrite Zplus_minus.
rewrite Pos.eqb_refl, !elmeqb_refl.
cbn.
unfold compute_public_key.
rewrite pow_pow by (auto with broom).
rewrite <- pow_plus by (auto with broom).
rewrite Z.sub_add.
rewrite elmeqb_refl.
cbn.
unfold compute_public_vote.
rewrite <- (mul_assoc (rk^sk)).
rewrite (mul_comm generator).
rewrite inv_inv_l by (auto with broom).
rewrite (mul_comm (rk^sk)), mul_1_l.
rewrite pow_pow by (subst rk; auto with broom).
rewrite <- pow_plus by (subst rk; auto with broom).
rewrite Z.sub_add.
now rewrite elmeqb_refl.
- set (h := hash_sv_data _ _ _ _ _ _ _).
rewrite Z.sub_add.
rewrite Pos.eqb_refl, !elmeqb_refl.
cbn.
unfold compute_public_key.
rewrite pow_pow by (auto with broom).
rewrite <- pow_plus by (auto with broom).
rewrite Z.sub_add.
rewrite elmeqb_refl.
cbn.
unfold compute_public_vote.
rewrite (mul_comm (rk^sk)), mul_1_l.
rewrite pow_pow by (subst rk; auto with broom).
rewrite <- pow_plus by (subst rk; auto with broom).
rewrite Z.sub_add.
now rewrite elmeqb_refl.
Qed.
Definition has_tallied (calls : list (ContractCallInfo Msg)) : bool :=
existsb (fun c => match Blockchain.call_msg c with
| Some tally_votes => true
......@@ -426,8 +510,11 @@ Definition has_tallied (calls : list (ContractCallInfo Msg)) : bool :=
end) calls.
Theorem boardroom_voting_correct_strong
bstate caddr (trace : ChainTrace empty_state bstate)
pks index sks chosen_randomness svs :
(bstate : ChainState)
(caddr : Address)
(trace : ChainTrace empty_state bstate)
(parties : Address -> SecretVoterInfo)
(pks : list A) :
env_contracts bstate caddr = Some (boardroom_voting : WeakContract) ->
exists (cstate : State)
(depinfo : DeploymentInfo Setup)
......@@ -446,8 +533,8 @@ Theorem boardroom_voting_correct_strong
(Z.of_nat (length (public_keys cstate)) < order - 1)%Z /\
(MsgAssumption pks index sks chosen_randomness svs inc_calls ->
SignupOrderAssumption pks index inc_calls ->
(MsgAssumption pks parties inc_calls ->
SignupOrderAssumption pks parties inc_calls ->
(finish_registration_by (setup cstate) < Blockchain.current_slot bstate ->
length pks = length (signups inc_calls)) ->
......@@ -458,18 +545,18 @@ Theorem boardroom_voting_correct_strong
(forall addr inf,
FMap.find addr (registered_voters cstate) = Some inf ->
voter_index inf < length (public_keys cstate) /\
voter_index inf = index addr /\
voter_index inf = svi_index (parties addr) /\
nth_error (public_keys cstate) (voter_index inf) =
Some (compute_public_key (sks addr)) /\
Some (compute_public_key (svi_sk (parties addr))) /\
(public_vote inf == zero \/
public_vote inf = compute_public_vote
(reconstructed_key pks (voter_index inf))
(sks addr)
(svs addr))) /\
(svi_sk (parties addr))
(svi_sv (parties addr)))) /\
((has_tallied inc_calls = false ->
result cstate = None) /\
(has_tallied inc_calls = true ->
result cstate = Some (sumnat (fun party => if svs party then 1 else 0)%nat
result cstate = Some (sumnat (fun party => if svi_sv (parties party) then 1 else 0)%nat
(FMap.keys (registered_voters cstate)))))).
Proof.
contract_induction; intros.
......@@ -606,7 +693,7 @@ Proof.
destruct (_ <? _); cbn -[Nat.ltb] in *; [congruence|].
destruct (FMap.find _ _) eqn:found; cbn in *; [|congruence].
destruct (if finish_commit_by _ then _ else _); cbn in *; [|congruence].
destruct (verify_vote _ _ _ _); cbn in *; [|congruence].
destruct (verify_secret_vote_proof _ _ _ _); cbn in *; [|congruence].
inversion_clear receive_some; cbn.
split; [lia|].
split; [tauto|].
......@@ -636,7 +723,7 @@ Proof.
unfold make_vote_msg in *.
inversion vote_assum.
destruct_hyps.
replace (index (ctx_from ctx)) with (voter_index v0) by congruence.
replace (svi_index (parties (ctx_from ctx))) with (voter_index v0) by congruence.
easy.
* rewrite FMap.find_add_ne in find_add by auto.
auto.
......@@ -668,9 +755,9 @@ Proof.
rewrite (bruteforce_tally_correct
(FMap.elements (registered_voters prev_state))
(fun '(_, v) => voter_index v)
(fun '(addr, _) => sks addr)
(fun '(addr, _) => svi_sk (parties addr))
(public_keys prev_state)
(fun kvp => svs (fst kvp))
(fun kvp => svi_sv (parties (fst kvp)))
(fun '(_, v) => public_vote v)) in bruteforce.
* inversion bruteforce.
unfold FMap.keys.
......@@ -698,10 +785,10 @@ Proof.
specialize (addrs _ _ kvpin).
cbn.
destruct addrs as [_ [_ [_ []]]]; [easy|].
fold (signups prev_inc_calls) (SignupOrderAssumption pks index prev_inc_calls) in *.
fold (signups prev_inc_calls) (SignupOrderAssumption pks parties prev_inc_calls) in *.
rewrite pks_signups.
specialize (num_signups_assum ltac:(lia)).
now rewrite (all_signups pks index) by auto.
now rewrite (all_signups pks parties) by auto.
- [CallFacts]: exact (fun _ ctx _ => ctx_from ctx <> ctx_contract_address ctx).
subst CallFacts; cbn in *; congruence.
- auto.
......@@ -711,27 +798,22 @@ Proof.
+ destruct valid_header; auto.
+ destruct_action_eval; auto.
intros.
pose proof (no_outgoing _ _ from_reachable H1).
unfold outgoing_acts in H3.
rewrite queue_prev in H3.
cbn in H3.
pose proof (no_outgoing _ _ from_reachable H0).
unfold outgoing_acts in H2.
rewrite queue_prev in H2.
cbn in H2.
destruct (address_eqb_spec (act_from act) to_addr); cbn in *; try congruence.
subst act; cbn in *; congruence.
Qed.
Theorem boardroom_voting_correct
bstate caddr (trace : ChainTrace empty_state bstate)
(bstate : ChainState)
(caddr : Address)
(trace : ChainTrace empty_state bstate)
(* list of all public keys, in the order of signups *)
(pks : list A)
(* function mapping a party to his signup index *)
(index : Address -> nat)
(* function mapping a party to his secret key *)
(sks : Address -> Z)
(* function mapping a party to his chosen randomness in the
secret key zero-knowledge proof *)
(chosen_randomness : Address -> Z)
(* function mapping a party to his vote *)
(svs : Address -> bool) :
(* function mapping a party to information about him *)
(parties : Address -> SecretVoterInfo) :
env_contracts bstate caddr = Some (boardroom_voting : WeakContract) ->
exists (cstate : State)
(depinfo : DeploymentInfo Setup)
......@@ -742,11 +824,11 @@ Theorem boardroom_voting_correct
(* assuming that the message sent were created with the
functions provided by this smart contract *)
MsgAssumption pks index sks chosen_randomness svs inc_calls ->
MsgAssumption pks parties inc_calls ->
(* ..and that people signed up in the order given by 'index'
and 'pks' *)
SignupOrderAssumption pks index inc_calls ->
SignupOrderAssumption pks parties inc_calls ->
(* ..and that the correct number of people register *)
(finish_registration_by (setup cstate) < Blockchain.current_slot bstate ->
......@@ -756,12 +838,11 @@ Theorem boardroom_voting_correct
((has_tallied inc_calls = false -> result cstate = None) /\
(* or if we have tallied yet, the result is correct *)
(has_tallied inc_calls = true ->
result cstate = Some (sumnat (fun party => if svs party then 1 else 0)%nat
result cstate = Some (sumnat (fun party => if svi_sv (parties party) then 1 else 0)%nat
(FMap.keys (registered_voters cstate))))).
Proof.
intros deployed.
destruct (boardroom_voting_correct_strong
bstate caddr trace pks index sks chosen_randomness svs deployed)
destruct (boardroom_voting_correct_strong bstate caddr trace parties pks deployed)
as [cstate [depinfo [inc_calls P]]].
exists cstate, depinfo, inc_calls.
tauto.
......
......@@ -39,10 +39,6 @@ Instance generator_instance : Generator axioms :=
BoardroomMath.generator_nonzero := generator_nonzero;
generator_generates := generator_is_generator; |}.
Instance id_scheme : @VoteProofScheme Z :=
{| make_vote_proof l n z b := 0%Z;
verify_vote l n a z := true; |}.
Definition num_parties : nat := 7.
Definition votes_for : nat := 4.
......@@ -64,8 +60,13 @@ Definition svs : list bool :=
Definition pks : list Z :=
Eval native_compute in map compute_public_key sks.
Definition rks : list Z :=
Eval native_compute in map (reconstructed_key pks) (seq 0 (length pks)).
(* In this example we just use xor for the hash function, which is
obviously not cryptographically secure. *)
Definition hash_func (l : list positive) : positive :=
countable.encode l.
N.succ_pos (fold_right (fun p a => N.lxor (Npos p) a) 1%N l).
(* Compute the signup messages that would be sent by each party.
We just use the public key as the chosen randomness here. *)
......@@ -75,10 +76,11 @@ Definition signups : list Msg :=