signatures.mli 8.54 KB
Newer Older
Stephane Glondu's avatar
Stephane Glondu committed
1
2
3
(**************************************************************************)
(*                                BELENIOS                                *)
(*                                                                        *)
Stephane Glondu's avatar
Stephane Glondu committed
4
(*  Copyright © 2012-2016 Inria                                           *)
Stephane Glondu's avatar
Stephane Glondu committed
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
(*                                                                        *)
(*  This program is free software: you can redistribute it and/or modify  *)
(*  it under the terms of the GNU Affero General Public License as        *)
(*  published by the Free Software Foundation, either version 3 of the    *)
(*  License, or (at your option) any later version, with the additional   *)
(*  exemption that compiling, linking, and/or using OpenSSL is allowed.   *)
(*                                                                        *)
(*  This program is distributed in the hope that it will be useful, but   *)
(*  WITHOUT ANY WARRANTY; without even the implied warranty of            *)
(*  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU     *)
(*  Affero General Public License for more details.                       *)
(*                                                                        *)
(*  You should have received a copy of the GNU Affero General Public      *)
(*  License along with this program.  If not, see                         *)
(*  <http://www.gnu.org/licenses/>.                                       *)
(**************************************************************************)

Stephane Glondu's avatar
Doc    
Stephane Glondu committed
22
(** Signatures *)
Stephane Glondu's avatar
Stephane Glondu committed
23

24
open Platform
25
26
open Serializable_t

27
28
29
30
31
(** Helpers for interacting with atd stuff *)

type 'a reader = Yojson.Safe.lexer_state -> Lexing.lexbuf -> 'a
type 'a writer = Bi_outbuf.t -> 'a -> unit

Stephane Glondu's avatar
Stephane Glondu committed
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
(** A group suitable for discrete logarithm-based cryptography. *)
module type GROUP = sig
  (** The following interface is redundant: it is assumed, but not
      checked, that usual mathematical relations hold. *)

  type t
  (** The type of elements. Note that it may be larger than the group
      itself, hence the [check] function below. *)

  val check : t -> bool
  (** Check group membership. *)

  val one : t
  (** The neutral element of the group. *)

  val g : t
  (** A generator of the group. *)

  val q : Z.t
  (** The order of [g]. *)

  val ( *~ ) : t -> t -> t
  (** Multiplication. *)

  val ( **~ ) : t -> Z.t -> t
  (** Exponentiation. *)

  val ( =~ ) : t -> t -> bool
  (** Equality test. *)

  val invert : t -> t
  (** Inversion. *)

65
66
67
  val to_string : t -> string
  (** Conversion to string. *)

68
69
70
  val of_string : string -> t
  (** Conversion from string. *)

71
72
73
74
75
76
  val read : t reader
  (** Reading from a stream. *)

  val write : t writer
  (** Writing to a stream. *)

77
78
79
  val hash : string -> t array -> Z.t
  (** Hash an array of elements into an integer mod [q]. The string
      argument is a string that is prepended before computing the hash. *)
Stephane Glondu's avatar
Stephane Glondu committed
80
81
82

  val compare : t -> t -> int
  (** A total ordering over the elements of the group. *)
83
84
85
86
87

  type group
  (** Serializable description of the group. *)

  val group : group
88
  val write_group : group writer
89
90
91

end

92
93
(** Monad signature. *)
module type MONAD = sig
Stephane Glondu's avatar
Stephane Glondu committed
94
95
96
  type 'a t
  val return : 'a -> 'a t
  val bind : 'a t -> ('a -> 'b t) -> 'b t
97
  val fail : exn -> 'a t
98
end
Stephane Glondu's avatar
Stephane Glondu committed
99

100
101
102
(** Random number generation. *)
module type RANDOM = sig
  include MONAD
Stephane Glondu's avatar
Stephane Glondu committed
103
104
105

  val random : Z.t -> Z.t t
  (** [random q] returns a random number modulo [q]. *)
106
end
Stephane Glondu's avatar
Stephane Glondu committed
107

Stephane Glondu's avatar
Stephane Glondu committed
108
(** Election data needed for cryptographic operations. *)
Stephane Glondu's avatar
Stephane Glondu committed
109
type 'a election = {
110
  e_params : 'a params;
111
112
  (** Parameters of the election. *)

Stephane Glondu's avatar
Stephane Glondu committed
113
114
115
  e_fingerprint : string;
  (** Fingerprint of the election. *)
}
Stephane Glondu's avatar
Stephane Glondu committed
116

117
118
119
120
121
122
(** Election data bundled with a group. *)
module type ELECTION_DATA = sig
  module G : GROUP
  val election : G.t election
end

Stephane Glondu's avatar
Typo    
Stephane Glondu committed
123
(** Cryptographic primitives for an election with homomorphic tally. *)
Stephane Glondu's avatar
Stephane Glondu committed
124
module type ELECTION = sig
Stephane Glondu's avatar
Stephane Glondu committed
125

Stephane Glondu's avatar
Stephane Glondu committed
126
127
128
  type 'a m
  (** The type of monadic values. *)

Stephane Glondu's avatar
Stephane Glondu committed
129
130
131
132
133
134
135
  (** {2 Election parameters} *)

  (** Ballots are encrypted using public-key cryptography secured by
      the discrete logarithm problem. Here, we suppose private keys
      are integers modulo a large prime number. Public keys are
      members of a suitably chosen group. *)

Stephane Glondu's avatar
Stephane Glondu committed
136
  type elt
Stephane Glondu's avatar
Stephane Glondu committed
137
138

  type t = elt election
Stephane Glondu's avatar
Stephane Glondu committed
139
  type private_key = Z.t
Stephane Glondu's avatar
Stephane Glondu committed
140
  type public_key = elt
Stephane Glondu's avatar
Stephane Glondu committed
141
142
143

  (** {2 Ciphertexts} *)

Stephane Glondu's avatar
Stephane Glondu committed
144
  type ciphertext = elt Serializable_t.ciphertext array array
Stephane Glondu's avatar
Stephane Glondu committed
145
146
  (** A ciphertext that can be homomorphically combined. *)

Stephane Glondu's avatar
Stephane Glondu committed
147
  val neutral_ciphertext : t -> ciphertext
148
149
  (** The neutral element for [combine_ciphertext] below. *)

Stephane Glondu's avatar
Stephane Glondu committed
150
151
152
153
154
155
  val combine_ciphertexts : ciphertext -> ciphertext -> ciphertext
  (** Combine two ciphertexts. The encrypted tally of an election is
      the combination of all ciphertexts of valid cast ballots. *)

  (** {2 Ballots} *)

Stephane Glondu's avatar
Stephane Glondu committed
156
  type plaintext = Serializable_t.plaintext
Stephane Glondu's avatar
Stephane Glondu committed
157
158
159
160
  (** The plaintext equivalent of [ciphertext], i.e. the contents of a
      ballot. When [x] is such a value, [x.(i).(j)] is the weight (0
      or 1) given to answer [j] in question [i]. *)

Stephane Glondu's avatar
Stephane Glondu committed
161
  type ballot = elt Serializable_t.ballot
Stephane Glondu's avatar
Stephane Glondu committed
162
163
164
165
  (** A ballot ready to be transmitted, containing the encrypted
      answers and cryptographic proofs that they satisfy the election
      constraints. *)

166
  type randomness
Stephane Glondu's avatar
Stephane Glondu committed
167
168
  (** Randomness needed to create a ballot. *)

Stephane Glondu's avatar
Stephane Glondu committed
169
  val make_randomness : t -> randomness m
170
171
172
  (** Creates randomness for [create_ballot] below. The result can be
      kept for Benaloh-style auditing. *)

173
174
  val create_ballot : t -> ?sk:private_key ->
    randomness -> plaintext -> ballot m
175
  (** [create_ballot r answers] creates a ballot, or raises
Stephane Glondu's avatar
Stephane Glondu committed
176
      [Invalid_argument] if [answers] doesn't satisfy the election
177
178
      constraints. The private key, if given, will be used to sign
      the ballot. *)
Stephane Glondu's avatar
Stephane Glondu committed
179

Stephane Glondu's avatar
Stephane Glondu committed
180
  val check_ballot : t -> ballot -> bool
Stephane Glondu's avatar
Stephane Glondu committed
181
182
183
184
185
186
187
188
  (** [check_ballot b] checks all the cryptographic proofs in [b]. All
      ballots produced by [create_ballot] should pass this check. *)

  val extract_ciphertext : ballot -> ciphertext
  (** Extract the ciphertext from a ballot. *)

  (** {2 Partial decryptions} *)

189
  type factor = elt partial_decryption
Stephane Glondu's avatar
Stephane Glondu committed
190
191
192
193
  (** A decryption share. It is computed by a trustee from his or her
      private key share and the encrypted tally, and contains a
      cryptographic proof that he or she didn't cheat. *)

Stephane Glondu's avatar
Stephane Glondu committed
194
  val compute_factor : ciphertext -> private_key -> factor m
Stephane Glondu's avatar
Stephane Glondu committed
195
196
197
198
199
200
201
202

  val check_factor : ciphertext -> public_key -> factor -> bool
  (** [check_factor c pk f] checks that [f], supposedly submitted by a
      trustee whose public_key is [pk], is valid with respect to the
      encrypted tally [c]. *)

  (** {2 Result} *)

Stephane Glondu's avatar
Stephane Glondu committed
203
  type result = elt Serializable_t.result
Stephane Glondu's avatar
Stephane Glondu committed
204
205
206
  (** The election result. It contains the needed data to validate the
      result from the encrypted tally. *)

207
  type combinator = factor list -> elt array array
208

209
  val compute_result : int -> ciphertext -> factor list -> combinator -> result
Stephane Glondu's avatar
Stephane Glondu committed
210
  (** Combine the encrypted tally and the factors from all trustees to
Stephane Glondu's avatar
Stephane Glondu committed
211
212
      produce the election result. The first argument is the number of
      tallied ballots. May raise [Invalid_argument]. *)
Stephane Glondu's avatar
Stephane Glondu committed
213

214
  val check_result : combinator -> result -> bool
Stephane Glondu's avatar
Stephane Glondu committed
215
216
217
218

  val extract_tally : result -> plaintext
  (** Extract the plaintext result of the election. *)
end
219
220
221
222
223
224
225
226

module type PKI = sig
  type 'a m
  type private_key
  type public_key
  val genkey : unit -> string m
  val derive_sk : string -> private_key
  val derive_dk : string -> private_key
227
228
  val sign : private_key -> string -> signed_msg m
  val verify : public_key -> signed_msg -> bool
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
  val encrypt : public_key -> string -> string m
  val decrypt : private_key -> string -> string
  val make_cert : sk:private_key -> dk:private_key -> cert m
  val verify_cert : cert -> bool
end

module type CHANNELS = sig
  type 'a m
  type private_key
  type public_key
  val send : private_key -> public_key -> string -> string m
  val recv : private_key -> public_key -> string -> string
end

module type PEDERSEN = sig
  type 'a m
  type elt

  val step1 : unit -> (string * cert) m
Stephane Glondu's avatar
Stephane Glondu committed
248
  val step1_check : cert -> bool
249
250
  val step2 : certs -> unit
  val step3 : certs -> string -> int -> polynomial m
Stephane Glondu's avatar
Stephane Glondu committed
251
  val step3_check : certs -> int -> polynomial -> bool
252
253
  val step4 : certs -> polynomial array -> vinput array
  val step5 : certs -> string -> vinput -> elt voutput m
Stephane Glondu's avatar
Stephane Glondu committed
254
  val step5_check : certs -> int -> polynomial array -> elt voutput -> bool
255
256
257
258
259
260
  val step6 : certs -> polynomial array -> elt voutput array -> elt threshold_parameters

  val check : elt threshold_parameters -> bool
  val combine : elt threshold_parameters -> elt

  type checker = elt -> elt partial_decryption -> bool
261
  val combine_factors : checker -> elt threshold_parameters -> elt partial_decryption list -> elt array array
262
end