Static Validation of a Voting Protocol |
Christoffer Rosenkilde Nielsen, Esben Heltoft Andersen, Hanne Riis Nielson
|
| Abstract | The desired security properties of electronic voting protocols include verifiability, accuracy, democracy and fairness. In this paper we use a static program analysis tool to validate these properties for one of the classical voting protocols under appropriate assumptions. The protocol is formalised in an extension of the LySa process calculus with blinding signatures. The analysis, which is fully automatic, pinpoints previously undiscovered flaws related to verifiability and accuracy and we suggest modifications of the protocol needed for validating these properties. |
| Keywords | Static Program Analysis Voting Protocols LySa |
| Type | Conference paper [With referee] |
| Conference | Automated Reasoning for Security Protocol Analysis (ARSPA 2005) |
| Year | 2005 Month July Vol. 135 No. 1 pp. 115-134 |
| Publisher | Elsevier |
| Series | Electronic Notes in Theoretical Computer Science |
| Publication link | http://dx.doi.org/10.1016/j.entcs.2005.06.001 |
| BibTeX data | [bibtex] |
| IMM Group(s) | Computer Science & Engineering |