L4 · APPLICATIONMEASURED

Encrypted Tally

encrypted-tally · spec v0.1.0 · 0 implementations · 6 runners

Create implementationSpecification

DESCRIPTION

Aggregates encrypted ballots into an encrypted result — counts per option, the winner, or whatever the tally is defined to produce.

Summing is the part homomorphic encryption gives away for free. Everything difficult is around it: turning the counts into a winner needs comparison, checking that a ballot is well-formed needs a predicate over encrypted data, and the result has to be decryptable by the electorate rather than by whoever ran the count.

The kernel is the tally, not the election. Key distribution, threshold decryption and ballot authentication are separate capabilities that a real election composes with this one.

INTERFACE

encrypted_tally(
  in  ct     : Ciphertext  // the encrypted ballots
  out ct     : Ciphertext  // the encrypted result — counts, ranking, or winner
  ...               // anything else the realization needs — keys, context, encoding — is its own concern
)

PARAMETER SCHEMA

NAMETYPERANGE

votersinteger1 – 2^24

optionsinteger2 – 2^12

result_formenumcounts, winner, ranking

validity_checkedbooleantrue, false

The schema belongs to the kernel. Each implementation declares which part of it it supports.

CORRECTNESS

01Counts are exact: an aggregate off by one is a wrong election.

02Where a winner is reported, ties are resolved by a rule stated in advance.

03Every ballot is counted exactly once.

SECURITY PROPERTIES

No individual ballot may be recoverable from the result or from the process. Intermediate tallies must not be observable either, since a running count reveals how individuals voted.

ASSUMPTIONS

Ballots are encrypted under a key the electorate controls. Authentication of voters and distribution of keys are separate capabilities.

REFERENCES

repoFHERMA participation guide