A formal analysis of the Neuchâtel e-voting protocol

This is the ProVerif analysis files for our study of the Neuchâtel e-voting protocol to be published and presented at EuroS&P 2018.
By Véronique Cortier, David Galindo and Mathieu Turuani.

Requirements

• The ProVerif Protocol Analyser. Note that the 'analyse' script used in this study assumes that a link exists in the working directory pointing to the proverif binary.
• The OCaml interpreter is used by the 'expand' script to generate the proverif models for specific values of the parameters. As an extra precaution, we provide already-expanded proverif specifications for the values discussed in the paper.
• The bash shell is used by all scripts except 'expand', and dateutils is used in the script 'analyse'. These scripts are optional and if needed, their function can easily be done by hand.

Scripts

• expand : a script designed to generate plain ProVerif models from the (single) main specification file called study_v14.alpha.pve, for both security targets and any value of k. For example, it can be used this way :
  

  For Observational equivalence, and k=2 :	./expand study_v14.alpha.pve OBS k=2
  For Reachability, and k=4 :	./expand study_v14.alpha.pve REA k=4

• expand_all : a script running 'expand' with all the parameters described in the paper. Expanded files linked bellow.
• analyse : a script to run proverif on some expanded model and output the time used. It writes the proverif's output in a file which extension shows the result (true/false) of the properties shown in the model.
• run_all : a script to running 'analyse' on all the proverif models created by 'expand_all'. Resulting files linked below.

Source model file

File : study_v14.alpha.pve

This is the main specification file. It uses a slightly enhanced ProVerif syntax which purpose is to model and maintain only one source specification model, from which the variants depected in the paper can be generated, for all the properties and values of k. Keywords like 'OBS' (for Observational Equivalence) or 'REA' (for Reachability) are used to activate small parts of the model, like querries for Reachability or chouces for Observational equivalence. Also, the number 'k' of vote selections is kept as a variable here, and the actual content of messages and actions will be adjusted by 'expand' according to the provided value of 'k'.

Expanded Proverif models and results

Note: the expanded.OBS.k=2 file has variants that swaps the voting options of honest voters, as described in the paper. However, they are not built automatically, i.e. the swaps must be done by hand. They are trivial, thu. The swapped files are provided, so that the reader don't need to do it.