University of Surrey

Test tubes in the lab Research in the ATI Dance Research

A Peered Bulletin Board for Robust Use in Verifiable Voting Systems

Culnane, C and Schneider, S (2014) A Peered Bulletin Board for Robust Use in Verifiable Voting Systems In: Computer Security Foundations Symposium (CSF), 2014 IEEE 27th, 19-22 July 2014, Vienna.

[img]
Preview
Text
WBB.pdf - ["content_typename_Accepted version (post-print)" not defined]
Available under License : See the attached licence file.

Download (239kB) | Preview
[img]
Preview
PDF (licence)
SRI_deposit_agreement.pdf
Available under License : See the attached licence file.

Download (33kB) | Preview

Abstract

The Web Bulletin Board (WBB) is a key component of verifiable election systems. It is used in the context of election verification to publish evidence of voting and tallying that voters and officials can check, and where challenges can be launched in the event of malfeasance. In practice, the election authority has responsibility for implementing the web bulletin board correctly and reliably, and will wish to ensure that it behaves correctly even in the presence of failures and attacks. To ensure robustness, an implementation will typically use a number of peers to be able to provide a correct service even when some peers go down or behave dishonestly. In this paper we propose a new protocol to implement such a Web Bulletin Board, motivated by the needs of the vVote verifiable voting system. Using a distributed algorithm increases the complexity of the protocol and requires careful reasoning in order to establish correctness. Here we use the Event-B modelling and refinement approach to establish correctness of the peered design against an idealised specification of the bulletin board behaviour. In particular we show that for n peers, a threshold of t > 2n/3 peers behaving correctly is sufficient to ensure correct behaviour of the bulletin board distributed design. The algorithm also behaves correctly even if honest or dishonest peers temporarily drop out of the protocol and then return. The verification approach also establishes that the protocols used within the bulletin board do not interfere with each other. This is the first time a peered web bulletin board suite of protocols has been formally verified.

Item Type: Conference or Workshop Item (Conference Paper)
Divisions : Faculty of Engineering and Physical Sciences > Computing Science
Authors :
AuthorsEmailORCID
Culnane, CUNSPECIFIEDUNSPECIFIED
Schneider, SUNSPECIFIEDUNSPECIFIED
Date : 2014
Identification Number : 10.1109/CSF.2014.20
Uncontrolled Keywords : cs.CR, cs.CR
Related URLs :
Additional Information : © 2014 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.
Depositing User : Symplectic Elements
Date Deposited : 15 Sep 2015 09:18
Last Modified : 15 Sep 2015 09:18
URI: http://epubs.surrey.ac.uk/id/eprint/808435

Actions (login required)

View Item View Item

Downloads

Downloads per month over past year


Information about this web site

© The University of Surrey, Guildford, Surrey, GU2 7XH, United Kingdom.
+44 (0)1483 300800