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.



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

Security goal Number of selections Result Output file
expanded.OBS.k=1.pv : Observational Equivalence 1 true result.OBS.k=1.true
expanded.OBS.k=2.pv : Observational Equivalence 2 true result.OBS.k=2.true
expanded.OBS.k=2.ab-ba.pv : Observational Equivalence 2 true result.OBS.k=2.ab-ba.true
expanded.OBS.k=2.ab-bc.pv : Observational Equivalence 2 true result.OBS.k=2.ab-bc.true
expanded.OBS.k=2.ab-cb.pv : Observational Equivalence 2 true result.OBS.k=2.ab-cb.true
expanded.REA.k=1.pv : Reachability 1 true result.REA.k=1.true.true
expanded.REA.k=2.pv : Reachability 2 true result.REA.k=2.true.true
expanded.REA.k=3.pv : Reachability 3 true result.REA.k=3.true.true
expanded.REA.k=4.pv : Reachability 4 true result.REA.k=4.true.true

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.