Free University of Amsterdam (THE NETHERLANDS)
CADP (Construction and Analysis of Distributed Processes)
38 μ-calculus formulas
up to 488,406 states and 1,264,554 transitions
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 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.
This study demonstrates the practical use of CADP in the field
of Internet voting protocol verification.
"A Formal Analysis of the RIES Internet Voting Protocol".
Master Thesis Report,
Free University of Amsterdam
Available on-line from our FTP site in PDF or PostScript
Vrije Universiteit Amsterdam
Department of Computer Science
Section Theoretical Computer Science
De Boelelaan 1081a, 1081 HV Amsterdam, The Netherlands
Tel: +31 20 598 7735
Fax: +31 20 598 7653
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|