Commit f4a25444 authored by Stephane Glondu's avatar Stephane Glondu

Functorized interface to crypto functions

 * new module StdExtra, for things that are like they could be in
   stdlib
 * new module ElGamal, for "abstract" crypto stuff
 * check group parameters (p, q, g) in make_ff_msubgroup
 * check that q is prime
parent e5296260
<**/*.{ml,mli}>: package(zarith), package(calendar), package(uuidm)
<**/*_{t,j}.{ml,mli}>: package(atdgen), package(yojson)
<**/*.{ml,mli}>: package(zarith), package(calendar), package(uuidm), package(cryptokit), package(atdgen)
<**/*_{t,j}.{ml,mli}>: package(yojson)
open StdExtra
open Helios_datatypes_t
module type GROUP = sig
type t
val one : t
val g : t
val q : Z.t
val p : Z.t
val ( *~ ) : t -> t -> t
val ( **~ ) : t -> Z.t -> t
val ( =~ ) : t -> t -> bool
val inv : t -> t
val check_exponent : Z.t -> bool
val check_element : t -> bool
val hash : t list -> Z.t
end
let hashZ x = Cryptokit.(x |>
hash_string (Hash.sha1 ()) |>
transform_string (Hexa.encode ()) |>
Z.of_string_base 16
)
let check_modulo p x = Z.(geq x zero && lt x p)
let make_ff_msubgroup p q g =
if
Z.probab_prime p 10 > 0 &&
Z.probab_prime q 10 > 0 &&
check_modulo p g &&
check_modulo p q &&
Z.(powm g q p =% one)
then
let module G = struct
open Z
type t = Z.t
let one = Z.one
let p = p
let q = q
let g = g
let ( *~ ) a b = a * b mod p
let ( **~ ) a b = powm a b p
let inv x = invert x p
let ( =~ ) = equal
let check_element x = check_modulo p x && x **~ q =~ one
let check_exponent x = check_modulo q x
let hash x = hashZ (String.concat "," (List.map to_string x)) mod q
end in (module G : GROUP with type t = Z.t)
else
invalid_arg "Invalid parameters for a multiplicative subgroup of finite field"
module type ELGAMAL_CRYPTO = sig
type t
val verify_public_key : t public_key -> bool
val verify_private_key : t private_key -> bool
val verify_pok : t -> t pok -> bool
val verify_election_key : t -> t trustee_public_key array -> bool
val verify_disjunction : t -> t -> t array -> t proof array -> bool
val verify_range : t -> int -> int -> t -> t -> t proof array -> bool
val verify_answer : t -> question -> t answer -> bool
val verify_vote : t election -> string -> t vote -> bool
val verify_equality : t -> t -> t -> t proof -> bool
val verify_partial_decryption :
t election -> t tally -> t trustee_public_key -> t partial_decryption -> bool
val verify_partial_decryptions : t election -> t election_public_data -> bool
val verify_result : t election -> t election_public_data -> bool
val compute_encrypted_tally : t election -> t vote array -> t encrypted_tally
end
module Make (G : GROUP) = struct
open G
(* FIXME: redundancy of group parameters that are embedded in the
abstract group *)
let verify_public_key k =
let {g = g'; p = p'; q = q'; y} = k in
g =~ g' && p =% p' && q =% q' && check_element y
let verify_private_key k =
let {x; public_key = {y; _}} = k in
check_exponent x && y =~ g **~ x
let verify_pok y pok =
let {pok_commitment; pok_challenge; pok_response} = pok in
(* NB: we don't check commitment and challenge thanks to hash *)
check_exponent pok_response &&
g **~ pok_response =~ pok_commitment *~ y **~ pok_challenge &&
pok_challenge =% hash [pok_commitment]
let verify_election_key y tpks =
let n = Array.length tpks in
assert (n > 0);
let rec loop i accu =
if i >= 0 then
let tpk = tpks.(i) in
let {g = g'; p = p'; q = q'; y = y'} = tpk.trustee_public_key in
g =~ g' && p =% p' && q =% q' && verify_pok y' tpk.trustee_pok &&
loop (pred i) (accu *~ y')
else accu =~ y
in loop (pred n) one
let verify_disjunction h big_g big_hs proof =
let n = Array.length big_hs in
assert (n > 0);
n = Array.length proof &&
(let rec check i commitments challenges =
if i >= 0 then
let {dp_commitment = {a; b}; dp_challenge; dp_response} = proof.(i) in
(* NB: we don't check commitment and challenge thanks to hash *)
check_exponent dp_response &&
g **~ dp_response =~ big_g **~ dp_challenge *~ a &&
h **~ dp_response =~ big_hs.(i) **~ dp_challenge *~ b &&
check (pred i) (a :: b :: commitments) Z.(challenges + dp_challenge)
else
hash commitments =% Z.(challenges mod q)
in check (pred n) [] Z.zero)
let verify_range h min max alpha beta proof =
Array.length proof = 2 &&
let big_hs = Array.init (max-min+1) (fun i -> beta *~ inv (g **~ Z.of_int (i-min))) in
verify_disjunction h alpha big_hs proof
let verify_answer y question answer =
let {q_max; q_min; q_answers; _} = question in
let nb = Array.length q_answers in
Array.length answer.choices = nb &&
Array.length answer.individual_proofs = nb &&
(let rec check i alphas betas =
if i >= 0 then
let {alpha; beta} = answer.choices.(i) in
check_element alpha &&
check_element beta &&
verify_range y 0 1 alpha beta answer.individual_proofs.(i) &&
check (pred i) (alphas *~ alpha) (betas *~ beta)
else
verify_range y q_min q_max alphas betas answer.overall_proof
in check (pred nb) one one)
let verify_vote e fingerprint v =
v.election_hash = fingerprint &&
e.e_uuid = v.election_uuid &&
array_forall2 (verify_answer e.e_public_key.y) e.e_questions v.answers
let verify_equality h g' h' proof =
(* NB: similar to disjunctive, but with different challenge
checking... hardly factorizable *)
let {dp_commitment = {a; b}; dp_challenge; dp_response} = proof in
(* NB: we don't check commitment and challenge thanks to hash *)
check_exponent dp_response &&
g **~ dp_response =~ g' **~ dp_challenge *~ a &&
h **~ dp_response =~ h' **~ dp_challenge *~ b &&
dp_challenge =% hash [a; b]
let verify_partial_decryption election tally tpk pds =
let y = tpk.trustee_public_key.y in
let {decryption_factors = dfs; decryption_proofs = dps} = pds in
array_foralli (fun i question ->
let dfs_i = dfs.(i) and dps_i = dps.(i) and tally_i = tally.(i) in
array_foralli (fun j answer ->
verify_equality tally_i.(j).alpha y dfs_i.(j) dps_i.(j)
) question.q_answers
) election.e_questions
let verify_partial_decryptions election public_data =
array_forall2 (verify_partial_decryption election public_data.encrypted_tally.tally)
public_data.public_keys
public_data.partial_decryptions
let verify_result election public_data =
let pds = public_data.partial_decryptions in
let tally = public_data.encrypted_tally.tally in
let result = public_data.result in
array_foralli (fun i question ->
array_foralli (fun j answer ->
let combined_factor = Array.fold_left (fun accu f ->
accu *~ f.decryption_factors.(i).(j)
) one pds in
inv combined_factor *~ tally.(i).(j).beta =~ g **~ Z.of_int result.(i).(j)
) question.q_answers
) election.e_questions
let compute_encrypted_tally e vs =
let ( * ) a b = Z.({ alpha = a.alpha *~ b.alpha; beta = a.beta *~ b.beta}) in
let num_tallied = Array.length vs in
let tally = Array.mapi (fun i question ->
Array.mapi (fun j answer ->
Array.fold_left (fun accu v ->
accu * v.answers.(i).choices.(j)
) { alpha = one; beta = one} vs
) question.q_answers
) e.e_questions in
{ num_tallied; tally }
end
(** Module [ElGamal] *)
open Helios_datatypes_t
module type GROUP = sig
type t
val one : t
val g : t
val q : Z.t
val p : Z.t
val ( *~ ) : t -> t -> t
val ( **~ ) : t -> Z.t -> t
val ( =~ ) : t -> t -> bool
val inv : t -> t
val check_exponent : Z.t -> bool
val check_element : t -> bool
val hash : t list -> Z.t
end
(** Signature of an abstract group suitable for ElGamal *)
val make_ff_msubgroup : Z.t -> Z.t -> Z.t -> (module GROUP with type t = Z.t)
(** [make_ff_msubgroup p q g] builds the multiplicative subgroup of
F[p], generated by [g], of order [q]. *)
module type ELGAMAL_CRYPTO = sig
type t
val verify_public_key : t public_key -> bool
val verify_private_key : t private_key -> bool
val verify_pok : t -> t pok -> bool
val verify_election_key : t -> t trustee_public_key array -> bool
val verify_disjunction : t -> t -> t array -> t proof array -> bool
val verify_range : t -> int -> int -> t -> t -> t proof array -> bool
val verify_answer : t -> question -> t answer -> bool
val verify_vote : t election -> string -> t vote -> bool
val verify_equality : t -> t -> t -> t proof -> bool
val verify_partial_decryption :
t election -> t tally -> t trustee_public_key -> t partial_decryption -> bool
val verify_partial_decryptions : t election -> t election_public_data -> bool
val verify_result : t election -> t election_public_data -> bool
val compute_encrypted_tally : t election -> t vote array -> t encrypted_tally
end
module Make (G : GROUP) : ELGAMAL_CRYPTO with type t := G.t
StdExtra
Core_datatypes_j
Helios_datatypes_t
Helios_datatypes_j
ElGamal
let ( |> ) x f = f x
let ( =% ) = Z.equal
let array_forall2 f a b =
let n = Array.length a in
n = Array.length b &&
(let rec check i =
if i >= 0 then f a.(i) b.(i) && check (pred i)
else true
in check (pred n))
let array_foralli f x =
let rec loop i =
if i >= 0 then f i x.(i) && loop (pred i)
else true
in loop (pred (Array.length x))
val ( |> ) : 'a -> ('a -> 'b) -> 'b
val ( =% ) : Z.t -> Z.t -> bool
val array_forall2 : ('a -> 'b -> bool) -> 'a array -> 'b array -> bool
val array_foralli : (int -> 'a -> bool) -> 'a array -> bool
open StdExtra
open Helios_datatypes_t
let ( |> ) x f = f x
let ( =~ ) = Z.equal
let hashZ x = Cryptokit.(x |>
hash_string (Hash.sha1 ()) |>
transform_string (Hexa.encode ()) |>
Z.of_string_base 16
)
let hashB x = Cryptokit.(x |>
hash_string (Hash.sha256 ()) |>
transform_string (Base64.encode_compact ())
)
let array_forall2 f a b =
let n = Array.length a in
n = Array.length b &&
(let rec check i =
if i >= 0 then f a.(i) b.(i) && check (pred i)
else true
in check (pred n))
let array_foralli f x =
let rec loop i =
if i >= 0 then f i x.(i) && loop (pred i)
else true
in loop (pred (Array.length x))
let check_modulo p x = Z.(geq x zero && lt x p)
let check_subgroup p q x = Z.(powm x q p =~ one)
module type TYPES = sig
type elt
type 'a t
......@@ -134,159 +109,6 @@ let load_election_test_data ?(verbose=false) dirname =
let private_data = load_and_check ~verbose Types.election_private_data (data "private_data.json") in
{ fingerprint; election; public_data; private_data }
let verify_public_key {g; p; q; y} =
Z.probab_prime p 10 > 0 &&
check_modulo p g &&
check_modulo p y &&
check_modulo p q &&
check_subgroup p q g &&
check_subgroup p q y
let verify_pok pk =
let {g; p; q; y} = pk.trustee_public_key in
let {pok_commitment; pok_challenge; pok_response} = pk.trustee_pok in
let ( ** ) a b = Z.powm a b p in
let ( * ) a b = Z.(a * b mod p) in
check_modulo p pok_commitment &&
check_modulo q pok_response &&
g ** pok_response =~ pok_commitment * y ** pok_challenge &&
pok_challenge =~ Z.(hashZ (Z.to_string pok_commitment) mod q)
let verify_disjunctive_proof pk big_g big_hs proof =
let n = Array.length big_hs in
n = Array.length proof &&
let {g; p; q; y = h} = pk in
let ( ** ) a b = Z.powm a b p in
let ( * ) a b = Z.(a * b mod p) in
assert (n > 0);
(let rec check i commitments challenges =
if i >= 0 then
let {dp_commitment = {a; b}; dp_challenge; dp_response} = proof.(i) in
(* FIXME: is it needed to do check_subgroup on a and b? *)
check_modulo p a &&
check_modulo p b &&
check_modulo q dp_challenge &&
check_modulo q dp_response &&
g ** dp_response =~ big_g ** dp_challenge * a &&
h ** dp_response =~ big_hs.(i) ** dp_challenge * b &&
check (pred i) (Z.to_string a :: Z.to_string b :: commitments) Z.(challenges + dp_challenge)
else
let commitments = String.concat "," commitments in
Z.(hashZ commitments mod q =~ challenges mod q)
in check (pred n) [] Z.zero)
let verify_range pk min max alpha beta proof =
let {g; p; q; y} = pk in
Array.length proof = 2 &&
let ( ** ) a b = Z.(powm a (of_int b) p) in
let ( / ) a b = Z.(a * invert b p mod p) in
let big_hs = Array.init (max-min+1) (fun i -> beta / (g ** (i-min))) in
verify_disjunctive_proof pk alpha big_hs proof
let verify_answer pk question answer =
let {q_max; q_min; q_answers; _} = question in
(* FIXME: handle q_max = infinity *)
let nb = Array.length q_answers in
let {g; p; q; y} = pk in
Array.length answer.choices = nb &&
Array.length answer.individual_proofs = nb &&
let ( * ) a b = Z.(a * b mod p) in
(let rec check i alphas betas =
if i >= 0 then
let {alpha; beta} = answer.choices.(i) in
check_subgroup p q alpha &&
check_subgroup p q beta &&
verify_range pk 0 1 alpha beta answer.individual_proofs.(i) &&
check (pred i) (alphas * alpha) (betas * beta)
else
verify_range pk q_min q_max alphas betas answer.overall_proof
in check (pred nb) Z.one Z.one)
let verify_vote e fingerprint v =
v.election_hash = fingerprint &&
e.e_uuid = v.election_uuid &&
array_forall2 (verify_answer e.e_public_key) e.e_questions v.answers
let compute_encrypted_tally e vs =
let {g; p; q; y} = e.e_public_key in
let ( * ) a b = Z.(a * b mod p) in
let ( *~ ) a b = Z.({ alpha = a.alpha * b.alpha mod p; beta = a.beta * b.beta mod p}) in
let num_tallied = Array.length vs in
let tally = Array.mapi (fun i question ->
Array.mapi (fun j answer ->
Array.fold_left (fun accu v ->
accu *~ v.answers.(i).choices.(j)
) Z.({ alpha = one; beta = one}) vs
) question.q_answers
) e.e_questions in
{ num_tallied; tally }
let verify_proof_item challenge_generator g h g' h' p q proof =
(* FIXME: factorize with verify_disjunctive_proof *)
let ( ** ) a b = Z.(powm a b p) and ( * ) a b = Z.(a * b mod p) in
let {dp_commitment = {a; b}; dp_challenge; dp_response} = proof in
(* FIXME: is it needed to do check_subgroup on a and b? *)
check_modulo p a &&
check_modulo p b &&
check_modulo q dp_challenge &&
check_modulo q dp_response &&
g ** dp_response =~ g' ** dp_challenge * a &&
h ** dp_response =~ h' ** dp_challenge * b &&
dp_challenge =~ challenge_generator a b
let verify_partial_decryption e tpk pds =
let {g; p; q; y} = tpk.trustee_public_key in
let {decryption_factors = dfs; decryption_proofs = dps} = pds in
let challenge_generator a b =
Z.(hashZ (to_string a ^ "," ^ to_string b) mod q)
in
let tally = e.public_data.encrypted_tally.tally in
array_foralli (fun i question ->
let dfs_i = dfs.(i) and dps_i = dps.(i) and tally_i = tally.(i) in
array_foralli (fun j answer ->
verify_proof_item challenge_generator g tally_i.(j).alpha y dfs_i.(j) p q dps_i.(j)
) question.q_answers
) e.election.e_questions
let verify_partial_decryptions e =
array_forall2 (verify_partial_decryption e)
e.public_data.public_keys
e.public_data.partial_decryptions
let verify_election_public_key pk tpks =
let n = Array.length tpks in
assert (n > 0);
let {g; p; q; y} = pk in
let rec loop i accu =
if i >= 0 then
let tpk = tpks.(i) in
let {g = g'; p = p'; q = q'; y = y'} = tpk.trustee_public_key in
g =~ g' && p =~ p' && q =~ q' &&
verify_pok tpk &&
loop (pred i) Z.(accu * y' mod p)
else accu =~ y
in loop (pred n) Z.one
let verify_result e =
let {g; p; q; y} = e.election.e_public_key in
let pds = e.public_data.partial_decryptions in
let tally = e.public_data.encrypted_tally.tally in
let result = e.public_data.result in
let ( * ) a b = Z.(a * b mod p) and ( ** ) a b = Z.(powm a (of_int b) p) in
array_foralli (fun i question ->
array_foralli (fun j answer ->
let combined_factor = Array.fold_left (fun accu f ->
accu * f.decryption_factors.(i).(j)
) Z.one pds in
Z.invert combined_factor p * tally.(i).(j).beta =~ g ** result.(i).(j)
) question.q_answers
) e.election.e_questions
let verify_private_key k =
let {x; public_key = {g; p; q; y}} = k in
check_modulo q x && y =~ Z.powm g x p
let verbose_assert msg it =
Printf.eprintf "Verifying %s...%!" msg;
let r = Lazy.force it in
......@@ -294,24 +116,27 @@ let verbose_assert msg it =
let load_election_and_verify_it_all dirname =
let e = load_election_test_data ~verbose:true dirname in
verbose_assert "public key"
(lazy (verify_election_public_key
e.election.e_public_key
let {g; p; q; y} = e.election.e_public_key in
let module G = (val ElGamal.make_ff_msubgroup p q g : ElGamal.GROUP with type t = Z.t) in
let module Crypto = ElGamal.Make (G) in
verbose_assert "election key"
(lazy (Crypto.verify_election_key
e.election.e_public_key.y
e.public_data.public_keys));
verbose_assert "votes"
(lazy (array_foralli
(fun _ x -> verify_vote e.election e.fingerprint x)
(fun _ x -> Crypto.verify_vote e.election e.fingerprint x)
e.public_data.votes));
verbose_assert "encrypted tally"
(lazy (e.public_data.encrypted_tally =
compute_encrypted_tally e.election e.public_data.votes));
Crypto.compute_encrypted_tally e.election e.public_data.votes));
verbose_assert "partial decryptions"
(lazy (verify_partial_decryptions e));
(lazy (Crypto.verify_partial_decryptions e.election e.public_data));
verbose_assert "result"
(lazy (verify_result e));
(lazy (Crypto.verify_result e.election e.public_data));
verbose_assert "private keys"
(lazy (array_foralli
(fun _ k -> verify_private_key k)
(fun _ k -> Crypto.verify_private_key k)
e.private_data.private_keys));;
let () = load_election_and_verify_it_all "tests/data/favorite-editor"
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment