Knowledge-based modelling of voting protocols

We contend that reasoning about knowledge is both natural and pragmatic for verification of electronic voting protocols. We present a model in which desirable properties of elections are naturally expressed using standard knowledge operators, and show that the associated logic is decidable (under reasonable assumptions of bounded agents and nonces). 1 Summary Consider the following scenario: an election is announced and is to take place on a given date. Voters are given a choice of candidates, and this is a standard political election, with each voter allowed to vote for exactly one candidate. On election day, during a specified period, voters can exercise their franchise in designated voting stations, or (here is the difference), vote online. What are the risks and vulnerabilities associated with such an electronic election? Electronic voting protocols address such issues and pose solutions. See [Rja02] for a discussion of cryptographic schemes intended as solutions to these proble...

• Type: Conference
• Year: 2007
• Where: TARK
• Authors: A. Baskar, Ramaswamy Ramanujam, S. P. Suresh
• Keywords: Electronic Elections, Electronic Voting Protocols, Political Elections, TARK 2007