Verification of the Dutch Rijnland Internet Election System

Organisation:	Free University of Amsterdam (THE NETHERLANDS)
Method:
Tools used:	CADP (Construction and Analysis of Distributed Processes)
Domain:	E-Democracy.
Period:	2007
Size:	11 scenarios 38 μ-calculus formulas up to 488,406 states and 1,264,554 transitions
Description:	Internet voting promises higher election turn-out and lower costs by providing a convenient, efficient and secure facility for managing votes. The Netherlands introduced RIES (the Rijnland Internet Election System) for expatriate voters to the "Second Chambre elections" in 2006. RIES, developed by the TTPI company in collaboration with Rijnland authorities, differs from other election systems in that everyone can tally the votes and voters can verify how their vote was counted, without disclosing their proof of vote. RIES involves five entities (the central controller, the voters, the JavaScript engine, the server administrator, and the vote office) and is divided into three phases: The initial phase, in which cryptographic keys are generated by the central controller and some are sent to voters (e.g., a unique voter key, a unique election identifier, unique candidate identifiers). Also, a reference file containing all the possible votes is generated. The election phase, in which voters can send to the server administrator their vote encrypted with their key by the JavaScript engine on their browser. The tally phase, in which the votes stored by the server administrator are compared to the reference file of the central controller to compute the final results. The vote office publicly announces all the information necessary to validate the results. RIES claims to be safe, in the sense that a fraud can always be detected. This study focuses on internal fraud considered as more perilous than external fraud. Among the verified properties are verifiability (voters are able to check what happened to their vote), validity (authentication and counting of votes), and anonymity (a potential voter cannot be uniquely characterized). RIES is formalized in μCRL and verified with CADP. From the model, nine scenarios have been designed to check with EVALUATOR verifiability and validity properties expressed in μ-calculus. Anonymity cannot be stated in modal logic, therefore the author proposes to compare two runs of the protocol with different voters' choices. The state spaces are minimized with BCG_MIN and showed branching equivalent with ALDEBARAN. Hence anonymity is ensured since an external observer cannot tell the difference between the two runs.
Conclusions:	This study demonstrates the practical use of CADP in the field of Internet voting protocol verification. "The analysis presented here is fully automatic and the verification algorithms do not need human intervention." Several tools offered by the CADP toolbox have been used: EVALUATOR, ALDEBARAN (today replaced by BISIMULATOR), BCG tools, and OCIS simulator. "I used CADP standard simulator which helped to assure that an implication does not result in a positive truth value only because the antecedent is always false. The model checker EVALUATOR 3.0 from the CADP tool-set is used here to verify properties of the protocol. It is used for efficient on-the-fly model checking of regular alternation-free μ-calculus formulas on a given Labeled Transition System (LTS for short)." Note that the study was performed with CADP 2001 and that as stated by the author: "The newer version offers a more convenient notation of modal logic formulas and should operate faster."
Publications:	[Maasbommel-07] Cynthia Maasbommel. "A Formal Analysis of the RIES Internet Voting Protocol". Master Thesis Report, Free University of Amsterdam February 2007 Available on-line from the CADP Web site in PDF or PostScript
Contact:	Wan Fokkink Vrije Universiteit Amsterdam Department of Computer Science Section Theoretical Computer Science De Boelelaan 1081a, 1081 HV Amsterdam, The Netherlands Room: U342 Tel: +31 20 598 7735 Fax: +31 20 598 7653 E-mail: wanf@cs.vu.nl
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page