Static Validation of a Voting Protocol

Christoffer Rosenkilde Nielsen; Esben Heltoft Andersen; Hanne Riis Nielson

Static Validation of a Voting Protocol

Christoffer Rosenkilde Nielsen, Esben Heltoft Andersen, Hanne Riis Nielson

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

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.

Original language	English
Title of host publication	Automated Reasoning for Security Protocol Analysis (ARSPA 2005)
Publisher	Elsevier
Publication date	2005
Pages	115-134
Publication status	Published - 2005

Access to Document

http://dx.doi.org/10.1016/j.entcs.2005.06.001

OpenUrl availability

Full text

Cite this

@inproceedings{2c87ed2162ca4c7abbcd2c1790fe4627,

title = "Static Validation of a Voting Protocol",

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",

author = "Nielsen, {Christoffer Rosenkilde} and Andersen, {Esben Heltoft} and Nielson, {Hanne Riis}",

year = "2005",

language = "English",

pages = "115--134",

booktitle = "Automated Reasoning for Security Protocol Analysis (ARSPA 2005)",

publisher = "Elsevier",

address = "United Kingdom",

}

TY - GEN

T1 - Static Validation of a Voting Protocol

AU - Nielsen, Christoffer Rosenkilde

AU - Andersen, Esben Heltoft

AU - Nielson, Hanne Riis

PY - 2005

Y1 - 2005

N2 - 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.

AB - 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.

KW - Static Program Analysis Voting Protocols LySa

M3 - Article in proceedings

SP - 115

EP - 134

BT - Automated Reasoning for Security Protocol Analysis (ARSPA 2005)

PB - Elsevier

ER -