BeleniosVS: Secrecy and Verifiability against a Corrupted Voting Device

REQUIREMENTS TO VERIFY THE MODELS

  • The ProVerif protocol verifier. ProVerif can be installed using the Opam package manager by running
    opam install proverif
    It is also available directly from the ProVerif website. Versions 1.98pl1 and 2.00 are known to work.
    Note that the scripts assume ProVerif is already installed and is in the shell’s PATH.
  • The bash shell and the perl interpreter are required by the scripts used to generate and verify the models for all corruption scenarios.
    These scripts are optional, as we provide all generated files, and ProVerif can be run manually on them.

MODEL FILES

[Download]

We provide all the ProVerif model files for the analysis of the BeleniosVS protocol, as well as the scripts we used to generate them.
The files are organised in three folders named after the security property they model.

  • Privacy
    These files formalise the privacy property for the BeleniosVS protocol, under different corruption scenarios.
    The scenario considered is described precisely in the beginning of each file. In a nutshell:

  • Receipt-freeness
    These files formalise the receipt-freeness property for the BeleniosVS protocol, under different corruption scenarios.
    The scenario considered is described precisely in the beginning of each file. In a nutshell:

    • rf-all-honest.pv: all entities are honest.
    • rf-audit.pv: the audit devices are dishonest (and thus the voting sheets are leaked, whether the voters lose them or not).
    • rf-registrar.pv: the registrar is dishonest (and thus the voting sheets are leaked, whether the voters lose them or not).
  • Verifiability
    This folder contains the scripts and files needed to generate the ProVerif files to analyse verifiability for the BeleniosVS protocol.
    We verify the necessary conditions established in the paper, under different corruption scenarios.

    • Source files
      The *.pv files in the verifiability folder contain pieces of ProVerif processes modelling the different entities of the protocol.
      These are not valid ProVerif files, but instead contain some macros that allow the scripts to make the entities honest or dishonest.
      The scripts then combine these files to generate the complete file for each scenario.
    • Scripts
      The README file contains a description of what each script does, and how to use them. In short:

      • gen.pl: a script that uses the source files to generate a proverif file modelling a corruption scenario that is described by the options passed to it.
        For instance, for a dishonest registrar and dishonest voting device:
        perl ./gen.pl --registrar dishonest --votingdevice dishonest
      • gen-both.pl: a script used to generate the file for the special case where some of the voters lose their voting sheet, while others lose their password.
        Run with:
        perl ./gen-both.pl
      • scan.pl: a script that reads the output of ProVerif on one of the generated files, parses it, and applies the theorems stated in the article to determine whether verifiability is proved or not. The relevant theorem is applied, depending on options indicating whether the server and registrar are honest or not.
        For instance:
        proverif <file.pv> | perl ./scan.pl --registrar honest --votingserver dishonest
      • all.sh: uses the previous three scripts to generate the ProVerif files for each scenario, run ProVerif on them, and print the results of the analysis.
        The generated files are stored in the generated-files folder.
        Run with:
        bash ./all.sh
    • Model files
      The ProVerif files for each scenario have been pre-generated, and are provided in the generated-files folder.Each file contains a description of the scenario it models. The files are also named accordingly, following the format « rx ax dx sx vsx pwdx.pv« , which indicates the honesty or dishonesty status of each entity:

      • r for the registrar, a for the audit device, d for the voting device, s for the voting server, vs for the voting sheet, pwd for the password.
      • 0 indicates a honest entity/secret data, while 1 indicates a dishonest entity/leaked data. In the case of the audit device only, 2 indicates that no audit is performed.
        For instance, « r0 a2 d0 s1 vs1 pwd1.pv » models the scenario where the registrar is honest, no audit is performed, the voting device is honest, the voting server is dishonest, and the voters leak both their voting sheet and their password.