Formal analysis of the Belenios VS protocol – Verifiability

All proof files can be downloaded here.

Source files for ProVerif files generation:

ProVerif models for each entity and corruption case can be found in the folder « 00_Entities_Models« :

  • 00_SETUP: the election setup phase model. Considered to always be honest.
  • 01_ (…): registrar and voting sheet models;
    • HONEST: honest registrar model. Generates a set of signature keys along the associated voting sheet. Sends the voting sheet through a private secure channel to the voter. Public credentials (the signature verification key and the certification value that proves the verfication key was generated by the registrar and is part of the set of valid public credentials for the election) are made public.
    • ROGUE: rogue registrar model. Generates the signature keyset and outputs it on the public channel controlled by the attacker along with the associated certification value that proves the signature verification key was generated by the registra and is part of the set of valid public credentials for the electionr. It also gives control of the voting sheet transmission channel to the attacker.
    • VISIBLE: models the voting sheet leak. Acts as a honest registrar but outputs the voting sheet on the public channel.
  • 02_ (…): honest voter models:
    • AUDIT: honest voter who audits the voting sheet models: one voting for candidate « A », the other for candidate « B« . Once the voter « n » receives the voting sheet associated to the verification key « spk_n », the event VOTER(n, spk_n, H) is triggered. After auditing all of the voting sheet entries, when the voter « n » scans the voting sheet entry matching their choice « v » with the voting device, the event VOTE(n, v, vote_id) is triggered, with « vote_id » a fresh nonce used to model the Tallied-as-Cast properties. After the voter « n » checks the value « spk_n » appears on the Public Bulletin Board, the event VERIFIED(n, v) is triggered.
    • NO_AUDIT: honest voter who does not audit the voting sheet models: one voting for candidate « A« , the other for candidate « B« . Once the voter « n » receives the voting sheet associated to the verification key « spk_n« , the event VOTER(n, spk_n, H) is triggered. When the voter « n » scans the voting sheet entry matching their choice « v » with the voting device, the event VOTE(n, v, vote_id) is triggered, with « vote_id » a fresh nonce used to model the Tallied-as-Cast properties. After the voter « n » checks the value « spk_n » appears on the Public Bulletin Board, the event VERIFIED(n, v) is triggered.
  • 03_ROGUE_VOTER: rogue voter model. Always part of the main process. Once the voter « n » receives the voting sheet associated to the verification key « spk_n« , the event VOTER(n, spk_n, C) is triggered. Outputs the voting sheet and their authentication credentials to the attacker.
  • 04_ (…): auditing device model. Does not appear on the main process if honest voters do not audit the voting sheet.
    • HONEST: honest auditing device model. Receives audit material through a private channel and proceeds to all required verification. Outputs « true » if the audit is successfull.
    • ROGUE: rogue auditing device model. Outputs all information it receives to the attacker and answer « true » without auditing the material.
  • 05_ (…): voting device models:
    • HONEST: honest voting device model. Receives the encrypted ballot scanned by the voter, verifies the signature and randomizes it with freshly generated nonces. Casts the ballot to the voting server through a authenticated channel.
    • ROGUE: rogue voting device model. Gives it all to the attacker.
  • 06_ (…): voting server models:
    • HONEST: honest voting server model. Checks the eligibility of the voter with function « is_registered« , checks the authentication credentials used by the voter to connect to the voting server are correct and that the signature verification key is part of the ones generated by the registrar with function « is_valid« . Finally, verifies the signature of the ballot. Then randomizes the ballot and publish it on the Public Bulletin Board, triggering the event GOING_TO_TALLY(n, spk_n, v), with « n » the voter identifier under which the server registers the ballot, « spk_n » the signature verification key used to sign the ballot and « v » the decryption of the ballot.
    • ROGUE: rogue voting server model. Since the Public Bulletin Board audit is considered as honest in our analysis, verifies the signature of ballots it receives. Publishes the ballot on the Public Bulletin Board with no further verification, triggering the event GOING_TO_TALLY(n, spk_n, v), with « n » the voter identifier under which the server registers the ballot, « spk_n » the signature verification key used to sign the ballot and « v » the decryption of the ballot.
    • ROGUE_NO_ROGUE_REGISTRAR: rogue voting server model when the registrar is part of honest entities. Since the Bulletin Board audit is considered as honest and since the registrar is honest, verifies the signature of ballots it receives but also that the signature verification key is part of the ones generated by the registrar with function « is_valid« . Publishes the ballot on the Public Bulletin Board with no further verification, triggering the event GOING_TO_TALLY(n, spk_n, v), with « n » the voter identifier under which the server registers the ballot, « spk_n » the signature verification key used to sign the ballot and « v » the decryption of the ballot.
  • 07_SECURITY_PROPERTIES: security properties that imply the verifiability of our protocol when satisfied.
  • 08_MAIN: main process modeling the execution of Belenios VS with an unbounded number of honest and rogue voters. Note that in all our proof files the election secret key is leaked.

ProVerif files generation for each corruption scenario that was considered:

All proof files were generated using the bash scripts that can be found in the folder « 01_Protocol_Models« :

  • GENERATOR: generates all combination of corruption cases we considered for our analysis.
  • SCRIPT: generates a ProVerif file corresponding to a specific combination of corruption case.

Note that due to specific modeling issues, two proof files could not be automatically generated with those scripts from our models:

Understanding our ProVerif files name:

The ProVerif files are named after the corruption scenarii they model. « 0 » means HONEST, « 1 » means ROGUE. « a » is used when there is no need to include the auditing device process, when honest voters do not audit the voting sheet.

  • Bit 1: authentication credentials stolen or not.
  • Bit 2: auditing device.
  • Bit 3: voting server.
  • Bit 4: voting device.
  • Bit 5: voting sheet leaked or not.
  • Bit 6: registrar.
  • Bit 7: honest voters audits or not the voting sheet.

For instance, if we consider the corruption scenario where the registrar and the voting server are honest, the voter does not audit the voting sheet and the authentication credentials are stolen, the ProVerif file is named: « 1a01001.pv« .

ProVerif proof results:

All ProVerif proof results for all files can be found in the folder « 02_Proofs_Results ».