research-article

Expressing Receipt-Freeness and Coercion-Resistance in Logics of Strategic Ability: Preliminary Attempt

Authors:

Masoud Tabatabaei,

Wojciech Jamroga,

Peter Y. A. RyanAuthors Info & Claims

PrAISe '16: Proceedings of the 1st International Workshop on AI for Privacy and Security

Article No.: 1, Pages 1 - 8

https://doi.org/10.1145/2970030.2970039

Published: 29 August 2016 Publication History

Abstract

Voting is a mechanism of utmost importance to social processes. In this paper, we focus on the strategic aspect of information security in voting procedures. We argue that the notions of receipt-freeness and coercion resistance are underpinned by existence (or nonexistence) of a suitable strategy for some participants of the voting process. In order to back the argument formally, we provide logical "transcriptions" of the informal intuitions behind coercion-related properties that can be found in the existing literature. The transcriptions are formulated in the modal game logic ATL*, well known in the area of multi-agent systems.

References

[1]

R. Aditya, B. Lee, C. Boyd, and E. Dawson. An efficient mixnet-based voting scheme providing receipt-freeness. In Trust and Privacy in Digital Business, pages 152--161. Springer, 2004.

[2]

T. Ågotnes. Action and knowledge in alternating-time temporal logic. Synthese, 149(2):377--409, 2006. Section on Knowledge, Rationality and Action.

[3]

R. Alur, T. A. Henzinger, and O. Kupferman. Alternating-time Temporal Logic. In Proceedings of the 38th Annual Symposium on Foundations of Computer Science (FOCS), pages 100--109. IEEE Computer Society Press, 1997.

Digital Library

[4]

R. Alur, T. A. Henzinger, and O. Kupferman. Alternating-time Temporal Logic. Journal of the ACM, 49:672--713, 2002.

Digital Library

[5]

R. Araújo, N. B. Rajeb, R. Robbana, J. Traoré, and S. Youssfi. Towards practical and secure coercion-resistant electronic elections. In Cryptology and Network Security, pages 278--297. Springer, 2010.

[6]

M. Backes, C. Hritcu, and M. Maffei. Automated verification of remote electronic voting protocols in the applied pi-calculus. In Computer Security Foundations Symposium, 2008. CSF'08. IEEE 21st, pages 195--209. IEEE, 2008.

Digital Library

[7]

A. Baskar, R. Ramanujam, and S. Suresh. Knowledge-based modelling of voting protocols. In Proceedings of the 11th conference on Theoretical aspects of rationality and knowledge, pages 62--71. ACM, 2007.

Digital Library

[8]

N. Belnap and M. Perloff. Seeing to it that: a canonical form for agentives. Theoria, 54:175--199, 1988.

[9]

J. Benaloh and D. Tuinstra. Receipt-free secret-ballot elections. In Proceedings of the twenty-sixth annual ACM symposium on Theory of computing, pages 544--553. ACM, 1994.

Digital Library

[10]

I. Boureanu, M. Cohen, and A. Lomuscio. Automatic verification of temporal-epistemic properties of cryptographic protocols. Journal of Applied Non-Classical Logics, 19(4):463--487, 2009.

[11]

I. Boureanu, M. Cohen, and A. Lomuscio. Model checking detectability of attacks in multiagent systems. In Proceedings of AAMAS, pages 691--698, 2010.

Digital Library

[12]

I. Boureanu, A. V. Jones, and A. Lomuscio. Automatic verification of epistemic specifications under convergent equational theories. In Proceedings of AAMAS, pages 1141--1148, 2012.

Digital Library

[13]

I. Boureanu, P. Kouvaros, and A. Lomuscio. Verifying security properties in unbounded multiagent systems. In Proceedings of AAMAS, pages 1209--1217, 2016.

Digital Library

[14]

J. W. Bryans, M. Koutny, L. Mazaré, and P. Y. Ryan. Opacity generalised to transition systems. In Formal Aspects in Security and Trust, pages 81--95. Springer, 2005.

Digital Library

[15]

J. W. Bryans, M. Koutny, and P. Y. Ryan. Modelling opacity using petri nets. Electronic Notes in Theoretical Computer Science, 121:101--115, 2005.

Digital Library

[16]

R. Chadha, S. Kremer, and A. Scedrov. Formal analysis of multiparty contract signing. Journal of Automated Reasoning, 36(1-2):39--83, 2006.

Digital Library

[17]

K. Chatterjee, T. A. Henzinger, and N. Piterman. Strategy logic. In Proceedings of CONCUR, pages 59--73, 2007.

Digital Library

[18]

D. Chaum, P. Y. A. Ryan, and S. A. Schneider. A practical voter-verifiable election scheme. In Proceedings of ESORICS, pages 118--139, 2005.

Digital Library

[19]

S. Delaune, S. Kremer, and M. Ryan. Coercion-resistance and receipt-freeness in electronic voting. In Computer Security Foundations Workshop, 2006. 19th IEEE, pages 12--pp. IEEE, 2006.

Digital Library

[20]

S. Delaune, S. Kremer, and M. Ryan. Verifying privacy-type properties of electronic voting protocols: A taster. In Towards Trustworthy Elections, pages 289--309. Springer, 2010.

Digital Library

[21]

S. Delaune, S. Kremer, and M. D. Ryan. Receipt-freeness: Formal definition and fault attacks. In Proceedings of the Workshop Frontiers in Electronic Elections (FEE 2005), Milan, Italy. Citeseer, 2005.

[22]

J. Dreier, P. Lafourcade, and Y. Lakhnech. A formal taxonomy of privacy in voting protocols. In Communications (ICC), 2012 IEEE International Conference on, pages 6710--6715. IEEE, 2012.

[23]

E. Emerson. Temporal and modal logic. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 995--1072. Elsevier Science Publishers, 1990.

Digital Library

[24]

A. Herzig and N. Troquard. Knowing how to play: Uniform choices in logics of agency. In Proceedings of AAMAS'06, pages 209--216, 2006.

Digital Library

[25]

W. Jamroga and T. Ågotnes. Constructive knowledge: What agents can achieve under incomplete information. Journal of Applied Non-Classical Logics, 17(4):423--475, 2007.

[26]

W. Jamroga, S. Mauw, and M. Melissen. Fairness in non-repudiation protocols. In Proceedings of STM'11, volume 7170 of Lecture Notes in Computer Science, pages 122--139, 2012.

Digital Library

[27]

W. Jamroga and W. van der Hoek. Agents that know how to play. Fundamenta Informaticae, 63(2-3):185--219, 2004.

Digital Library

[28]

H. L. Jonker and W. Pieters. Receipt-freeness as a special case of anonymity in epistemic logic. 2006.

[29]

A. Juels, D. Catalano, and M. Jakobsson. Coercion-resistant electronic elections. In Proceedings of the 2005 ACM workshop on Privacy in the electronic society, pages 61--70. ACM, 2005.

Digital Library

[30]

S. Kremer and J. Raskin. Game analysis of abuse-free contract signing. In Proceedings of the 15th IEEE Computer Security Foundations Workshop (CSFW'02), pages 206--220. IEEE Computer Society Press, 2002.

Digital Library

[31]

S. Kremer and J.-F. Raskin. A game-based verification of non-repudiation and fair exchange protocols. Journal of Computer Security, 11(3), 2003.

Digital Library

[32]

W.-C. Ku and C.-M. Ho. An e-voting scheme against bribe and coercion. In e-Technology, e-Commerce and e-Service, 2004. EEE'04. 2004 IEEE International Conference on, pages 113--116. IEEE, 2004.

Digital Library

[33]

R. Kusters and T. Truderung. An epistemic approach to coercion-resistance for electronic voting protocols. In Security and Privacy, 2009 30th IEEE Symposium on, pages 251--266. IEEE, 2009.

Digital Library

[34]

R. Küsters, T. Truderung, and A. Vogt. A game-based definition of coercion-resistance and its applications. In 2010 23rd IEEE Computer Security Foundations Symposium, pages 122--136. IEEE, 2010.

Digital Library

[35]

B. Lee, C. Boyd, E. Dawson, K. Kim, J. Yang, and S. Yoo. Providing receipt-freeness in mixnet-based voting protocols. In Information Security and Cryptology-ICISC 2003, pages 245--258. Springer, 2004.

[36]

B. Lee and K. Kim. Receipt-free electronic voting scheme with a tamper-resistant randomizer. In Information Security and Cryptology-ICISC 2002, pages 389--406. Springer, 2003.

Digital Library

[37]

A. Lomuscio and W. Penczek. LDYIS: a framework for model checking security protocols. Fundamenta Informaticae, 85(1-4):359--375, 2008.

Digital Library

[38]

E. Magkos, M. Burmester, and V. Chrissikopoulos. Receipt-freeness in large-scale elections without untappable channels. In Towards The E-Society, pages 683--693. Springer, 2001.

Digital Library

[39]

B. Meng. A critical review of receipt-freeness and coercion-resistance. Information Technology Journal, 8(7):934--964, 2009.

[40]

M. Michels and P. Horster. Some remarks on a receipt-free and universally verifiable mix-type voting scheme. In Advances in Cryptology-ASIACRYPT'96, pages 125--132. Springer, 1996.

Digital Library

[41]

F. Mogavero, A. Murano, G. Perelli, and M. Vardi. What makes ATL* decidable? a decidable fragment of strategy logic. In Proceedings of CONCUR, pages 193--208, 2012.

Digital Library

[42]

F. Mogavero, A. Murano, G. Perelli, and M. Vardi. Reasoning about strategies: On the model-checking problem. ACM Transactions on Computational Logic, 15(4):1--42, 2014.

Digital Library

[43]

F. Mogavero, A. Murano, and M. Vardi. Reasoning about strategies. In Proceedings of FSTTCS, pages 133--144, 2010.

[44]

T. Moran and M. Naor. Receipt-free universally-verifiable voting with everlasting privacy. In Advances in Cryptology-CRYPTO 2006, pages 373--392. Springer, 2006.

Digital Library

[45]

T. Okamoto. Receipt-free electronic voting schemes for large scale elections. In Security Protocols, pages 25--35. Springer, 1998.

Digital Library

[46]

T. Peacock and P. Ryan. Coercion-resistance as opacity in voting systems. Technical Report Series-University Of Newcatle Upon Tyne Computing Science, 959, 2006.

[47]

P. Y. A. Ryan. The computer ate my vote. In Formal Methods: State of the Art and New Directions, pages 147--184. Springer, 2010.

[48]

M. Schlapfer, R. Haenni, R. Koenig, and O. Spycher. Efficient vote authorization in coercion-resistant internet voting. In E-Voting and Identity: Third International Conference, VoteID 2011, Tallinn, Estonia, September 28-20, 2011, Revised Selected Papers, volume 7187, page 71. Springer, 2012.

Digital Library

[49]

H. Schnoor. Strategic planning for probabilistic games with incomplete information. In Proceedings of AAMAS'10, pages 1057--1064, 2010.

Digital Library

[50]

P. Y. Schobbens. Alternating-time logic with imperfect recall. Electronic Notes in Theoretical Computer Science, 85(2):82--93, 2004.

[51]

S. G. Weber, R. Araujo, and J. Buchmann. On coercion-resistant electronic elections with linear work. In Availability, Reliability and Security, 2007. ARES 2007. The Second International Conference on, pages 908--916. IEEE, 2007.

Digital Library

Cited By

Niewiadomski ANazarczuk MPrzychodzki MKacprzak MPenczek WZbrzezny ADastani MSichman JAlechina NDignum V(2024)SMT4SMTL: A Tool for SMT-Based Satisfiability Checking of SMTLProceedings of the 23rd International Conference on Autonomous Agents and Multiagent Systems10.5555/3635637.3663297(2815-2817)Online publication date: 6-May-2024
https://dl.acm.org/doi/10.5555/3635637.3663297
Tabatabaei MJamroga WAgmon NAn BRicci AYeoh W(2023)Playing to Learn, or to Keep Secret: Alternating-Time Logic Meets Information TheoryProceedings of the 2023 International Conference on Autonomous Agents and Multiagent Systems10.5555/3545946.3598710(766-774)Online publication date: 30-May-2023
https://dl.acm.org/doi/10.5555/3545946.3598710
Riou SKulyk OMarcos del Blanco D(2022)A Formal Approach to Coercion Resistance and Its Application to E-VotingMathematics10.3390/math1005078110:5(781)Online publication date: 28-Feb-2022
https://doi.org/10.3390/math10050781
Show More Cited By

Expressing Receipt-Freeness and Coercion-Resistance in Logics of Strategic Ability: Preliminary Attempt
1. Computing methodologies
  1. Artificial intelligence
    1. Distributed artificial intelligence
2. Theory of computation
  1. Logic

Recommendations

Coercion-Resistance and Receipt-Freeness in Electronic Voting
CSFW '06: Proceedings of the 19th IEEE workshop on Computer Security Foundations

In this paper we formally study important properties of electronic voting protocols. In particular we are interested in coercion-resistance and receipt-freeness. Intuitively, an election protocol is coercion-resistant if a voter A cannot prove to a ...
Bare-handed electronic voting with pre-processing
EVT'07: Proceedings of the USENIX Workshop on Accurate Electronic Voting Technology

Many electronic voting schemes assume the user votes with some computing device. This raises the question whether a voter can trust the device he is using. Three years ago, Chaum, and independently Neff, proposed what we call bare-handed electronic ...
Receipt-freeness and coercion resistance in remote E-voting systems

Remote electronic voting E-voting is a more convenient and efficient methodology when compared with traditional voting systems. It allows voters to vote for candidates remotely, however, remote E-voting systems have not yet been widely deployed in ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Other conferences

PrAISe '16: Proceedings of the 1st International Workshop on AI for Privacy and Security

August 2016

91 pages

ISBN:9781450343046

DOI:10.1145/2970030

Copyright © 2016 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 the author(s) 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: 29 August 2016

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed limited

Conference

PrAISe '16

PrAISe '16: International Workshop on AI for Privacy and Security

August 29 - 30, 2016

The Hague, Netherlands

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

14
Total Citations
View Citations
95
Total Downloads

Downloads (Last 12 months)7
Downloads (Last 6 weeks)1

Reflects downloads up to 28 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Niewiadomski ANazarczuk MPrzychodzki MKacprzak MPenczek WZbrzezny ADastani MSichman JAlechina NDignum V(2024)SMT4SMTL: A Tool for SMT-Based Satisfiability Checking of SMTLProceedings of the 23rd International Conference on Autonomous Agents and Multiagent Systems10.5555/3635637.3663297(2815-2817)Online publication date: 6-May-2024
https://dl.acm.org/doi/10.5555/3635637.3663297
Tabatabaei MJamroga WAgmon NAn BRicci AYeoh W(2023)Playing to Learn, or to Keep Secret: Alternating-Time Logic Meets Information TheoryProceedings of the 2023 International Conference on Autonomous Agents and Multiagent Systems10.5555/3545946.3598710(766-774)Online publication date: 30-May-2023
https://dl.acm.org/doi/10.5555/3545946.3598710
Riou SKulyk OMarcos del Blanco D(2022)A Formal Approach to Coercion Resistance and Its Application to E-VotingMathematics10.3390/math1005078110:5(781)Online publication date: 28-Feb-2022
https://doi.org/10.3390/math10050781
Jamroga WKurpiewski DMalvone VGroß TViganò L(2022)How to measure usable securityJournal of Computer Security10.3233/JCS-21004930:3(381-409)Online publication date: 1-Jan-2022
https://dl.acm.org/doi/10.3233/JCS-210049
Kurpiewski DMikulski ŁJamroga W(2022)STV+AGR: Towards Verification of Strategic Ability Using Assume-Guarantee ReasoningPRIMA 2022: Principles and Practice of Multi-Agent Systems10.1007/978-3-031-21203-1_47(691-696)Online publication date: 12-Nov-2022
https://doi.org/10.1007/978-3-031-21203-1_47
Kurpiewski DPazderski WJamroga WKim YDignum FLomuscio AEndriss UNowé A(2021)STV+Reductions: Towards Practical Verification of Strategic Ability Using Model ReductionsProceedings of the 20th International Conference on Autonomous Agents and MultiAgent Systems10.5555/3463952.3464232(1770-1772)Online publication date: 3-May-2021
https://dl.acm.org/doi/10.5555/3463952.3464232
Jamroga WKurpiewski DMalvone V(2021)Natural Strategic Abilities in Voting ProtocolsSocio-Technical Aspects in Security and Trust10.1007/978-3-030-79318-0_3(45-62)Online publication date: 22-Jun-2021
https://doi.org/10.1007/978-3-030-79318-0_3
Belardinelli FCondurache RDima CJamroga WKnapik M(2020)Bisimulations for Verifying Strategic Abilities with an Application to the ThreeBallot Voting ProtocolInformation and Computation10.1016/j.ic.2020.104552(104552)Online publication date: Mar-2020
https://doi.org/10.1016/j.ic.2020.104552
Belardinelli FJamroga WKurpiewski DMalvone VMurano A(2019)Strategy logic with simple goalsProceedings of the 28th International Joint Conference on Artificial Intelligence10.5555/3367032.3367046(88-94)Online publication date: 10-Aug-2019
https://dl.acm.org/doi/10.5555/3367032.3367046
Kurpiewski DJamroga WKnapik MElkind EVeloso MAgmon NTaylor M(2019)STVProceedings of the 18th International Conference on Autonomous Agents and MultiAgent Systems10.5555/3306127.3332116(2372-2374)Online publication date: 8-May-2019
https://dl.acm.org/doi/10.5555/3306127.3332116
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