Article

Knowledge-based modelling of voting protocols

Authors:

S. P. SureshAuthors Info & Claims

TARK '07: Proceedings of the 11th conference on Theoretical aspects of rationality and knowledge

Pages 62 - 71

https://doi.org/10.1145/1324249.1324261

Published: 25 June 2007 Publication History

Abstract

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

References

[1]

{AN05} S. Artemov and E. Nogina. On epistemic logic with justification. In Proceedings of TARK X, pages 279--294, Singapore, July 2005.

Digital Library

[2]

{AR00} Martin Abadi and Phillip Rogaway. Reconciling two views of cryptography (the computational soundness of formal encryption). In Proceedings of the IFIP International Conference on TCS (IFIP TCS2000), volume 1872 of Lecture Notes in Computer Science, pages 3--22, 2000.

Digital Library

[3]

{BT94} Josh Cohen Benaloh and Dwight Tuinstra. Receiptfree secret-ballot elections(extended abstract). In Proceedings of 26th Symposium on Theory of Computing, pages 544--553, 1994.

Digital Library

[4]

{CDL⁺99} Iliano Cervesato, Nancy A. Durgin, Patrick D. Lincoln, John C. Mitchell, and Andre Scedrov. A Metanotation for Protocol Analysis. In P. Syverson, editor, Proceedings of the 12th IEEE Computer Security Foundations Workshop, pages 35--51. IEEE Computer Society Press, 1999.

Digital Library

[5]

{Cha83} D. Chaum. Blind signatures for untraceable payments. In Advances in Cryptology -- Crypto '82, pages 199--203. Springer--Verlag, 1983.

[6]

{Cha85} D. Chaum. Security without identification: transaction systems to make big brother obsolete. Communications of the ACM, 28(10):1030--1044, 1985.

Digital Library

[7]

{CMFP⁺06} Benoit Chevallier-Mames, Pierre-Alain Fouque, David Pointcheval, Julien Stern, and Jacques Traore. On Some Incompatible properties of Voting Schemes. In Proceedings of the IAVoSS Workshop on Trustworthy Elections, 2006.

[8]

{CMS00} Iliano Cervesato, Catherine A. Meadows, and Paul F. Syverson. Dolev-Yao is no better than Machiavelli. In P. Degano, editor, Proceedings of WITS'00, pages 87--92, July 2000.

[9]

{DKR06} Stephanie Delaune, Steve Kremer, and Mark Ryan. Coercion-Resistance and Receipt-Freeness in Electronic Voting. In 19th Computer Security Foundations Workshop, pages 28--42. IEEE Computer Society, 2006.

Digital Library

[10]

{DY83} Danny Dolev and Andrew Yao. On the Security of public-key protocols. IEEE Transactions on Information Theory, 29:198--208, 1983.

Digital Library

[11]

{FHMV95} Ronald Fagin, Joseph Y. Halpern, Yoram Moses, and Moshe Y. Vardi. Reasoning about Knowledge. M.I.T. Press, 1995.

[12]

{FOO92} Atsushi Fujioka, Tatsuaki Okamoto, and Kaazuo Ohta. A practical secret voting scheme for large scale elections. In ASIACRYPT, pages 244--251, 1992.

Digital Library

[13]

{HO05} Joseph Y. Halpern and Kevin R. O'Neil. Anonymity and Information Hiding in Multiagent Systems. Journal of Computer Security, 13(3):483--512, 2005.

Digital Library

[14]

{HP03} Joseph Y. Halpern and Riccardo Pucella. Modeling adversaries in a logic for security protocol analysis. In Formal Aspects of Security, First International Conference, FASec 2002, volume 2629 of Lecture Notes in Computer Science, pages 115--132, 2003.

[15]

{JdV06} Hugo Jonker and E. P. de Vink. Formalising Receipt-Freeness. In Information Security Conference, volume 4176 of Lecture Notes in Computer Science, pages 476--488. Springer, 2006.

Digital Library

[16]

{JP06} Hugo Jonker and Wolter Pieters. Receipt-freeness as a special case of anonymity in epistemic logic. In Proceedings of the IAVoSS Workshop on Trustworthy Elections, 2006.

[17]

{KR05} Steve Kremer and Mark Ryan. Analysis of an Electronic Voting Protocol in the Applied Pi Calculus. In Proceedings of the European Symposium on Programming, volume 3444 of Lecture Notes in Computer Science, pages 186--200. Springer, 2005.

Digital Library

[18]

{PR85} Rohit Parikh and R. Ramanujam. Distributed Processes and the Logic of Knowledge. In Logic of Programs, pages 256--268, 1985.

Digital Library

[19]

{Rja02} Zuzana Rjaskova. Electronic voting schemes. Master's thesis, Comenius University, 2002.

[20]

{RS05} R. Ramanujam and S. P. Suresh. Decidability of context-explicit security protocols. Journal of Computer Security, 13(1):135--165, 2005.

Digital Library

[21]

{RS06} R. Ramanujam and S. P. Suresh. A (restricted) quantifier elimination for security protocols. Theoretical Computer Science, 367:228--256, 2006.

Digital Library

Cited By

Rajaona FBoureanu IRamanujam RWesemeyer S(2024)Epistemic Model Checking for Privacy2024 IEEE 37th Computer Security Foundations Symposium (CSF)10.1109/CSF61375.2024.00020(1-16)Online publication date: 8-Jul-2024
https://doi.org/10.1109/CSF61375.2024.00020
Hagihara SShimakawa MYonezaki N(2019)Verification of Verifiability of Voting Protocols by Strand Space AnalysisProceedings of the 2019 8th International Conference on Software and Computer Applications10.1145/3316615.3316629(363-368)Online publication date: 19-Feb-2019
https://dl.acm.org/doi/10.1145/3316615.3316629
Gardy PDeng Y(2019)Simulations for Multi-Agent Systems with Imperfect InformationFormal Methods and Software Engineering10.1007/978-3-030-32409-4_9(138-153)Online publication date: 28-Oct-2019
https://doi.org/10.1007/978-3-030-32409-4_9
Show More Cited By

Knowledge-based modelling of voting protocols

Recommendations

Three voting protocols: ThreeBallot, VAV, and twin
EVT'07: Proceedings of the USENIX Workshop on Accurate Electronic Voting Technology

We present three new paper-based voting methods with interesting security properties. Our goal is to achieve the same security properties as recently proposed cryptographic voting protocols, but using only paper ballots and no cryptography. From a ...
Verifying privacy-type properties of electronic voting protocols

Electronic voting promises the possibility of a convenient, efficient and secure facility for recording and tallying votes in an election. Recently highlighted inadequacies of implemented systems have demonstrated the importance of formally verifying ...
Sok: vector OLE-based zero-knowledge protocols
Abstract
A zero-knowledge proof is a cryptographic protocol where a prover can convince a verifier that a statement is true, without revealing any further information except for the truth of the statement. This article is a survey of recent developments in ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Other conferences

TARK '07: Proceedings of the 11th conference on Theoretical aspects of rationality and knowledge

June 2007

296 pages

ISBN:9781450378413

DOI:10.1145/1324249

Program Chair:
Dov Samet

Copyright © 2007 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 25 June 2007

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Acceptance Rates

TARK '07 Paper Acceptance Rate 32 of 100 submissions, 32%;

Overall Acceptance Rate 61 of 177 submissions, 34%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

36
Total Citations
View Citations
229
Total Downloads

Downloads (Last 12 months)9
Downloads (Last 6 weeks)0

Reflects downloads up to 28 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Rajaona FBoureanu IRamanujam RWesemeyer S(2024)Epistemic Model Checking for Privacy2024 IEEE 37th Computer Security Foundations Symposium (CSF)10.1109/CSF61375.2024.00020(1-16)Online publication date: 8-Jul-2024
https://doi.org/10.1109/CSF61375.2024.00020
Hagihara SShimakawa MYonezaki N(2019)Verification of Verifiability of Voting Protocols by Strand Space AnalysisProceedings of the 2019 8th International Conference on Software and Computer Applications10.1145/3316615.3316629(363-368)Online publication date: 19-Feb-2019
https://dl.acm.org/doi/10.1145/3316615.3316629
Gardy PDeng Y(2019)Simulations for Multi-Agent Systems with Imperfect InformationFormal Methods and Software Engineering10.1007/978-3-030-32409-4_9(138-153)Online publication date: 28-Oct-2019
https://doi.org/10.1007/978-3-030-32409-4_9
Fraser AQuaglia ESmyth B(2019)A Critique of Game-Based Definitions of Receipt-Freeness for VotingProvable Security10.1007/978-3-030-31919-9_11(189-205)Online publication date: 26-Sep-2019
https://doi.org/10.1007/978-3-030-31919-9_11
Kawamoto Y(2019)Statistical Epistemic LogicThe Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy10.1007/978-3-030-31175-9_20(344-362)Online publication date: 4-Nov-2019
https://doi.org/10.1007/978-3-030-31175-9_20
Baskar ARamanujam RSuresh S(2019)Dolev-Yao Theory with Associative Blindpair OperatorsImplementation and Application of Automata10.1007/978-3-030-23679-3_5(58-69)Online publication date: 26-Jun-2019
https://doi.org/10.1007/978-3-030-23679-3_5
REUß ASEIDL H(2017)Paths, tree homomorphisms and disequalities for -clausesMathematical Structures in Computer Science10.1017/S096012951700024X28:10(1786-1846)Online publication date: 6-Dec-2017
https://doi.org/10.1017/S096012951700024X
Tabatabaei MJamroga WRyan P(2016)Expressing Receipt-Freeness and Coercion-Resistance in Logics of Strategic AbilityProceedings of the 1st International Workshop on AI for Privacy and Security10.1145/2970030.2970039(1-8)Online publication date: 29-Aug-2016
https://dl.acm.org/doi/10.1145/2970030.2970039
Tsukada YSakurada HMano KManabe Y(2016)On compositional reasoning about anonymity and privacy in epistemic logicAnnals of Mathematics and Artificial Intelligence10.1007/s10472-016-9516-878:2(101-129)Online publication date: 1-Oct-2016
https://dl.acm.org/doi/10.1007/s10472-016-9516-8
Mousavi HAhmadi BRahimi S(2016)A new approach to decrease the computational complexity of e‐voting protocolsTransactions on Emerging Telecommunications Technologies10.1002/ett.314028:7Online publication date: 23-Dec-2016
https://doi.org/10.1002/ett.3140
Show More Cited By

View Options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents