Masoud Tabatabaei
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.
- 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.Google Scholar
Cross Ref
- T. Ågotnes. Action and knowledge in alternating-time temporal logic. Synthese, 149(2):377--409, 2006. Section on Knowledge, Rationality and Action.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- R. Alur, T. A. Henzinger, and O. Kupferman. Alternating-time Temporal Logic. Journal of the ACM, 49:672--713, 2002. Google ScholarDigital Library
- 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.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- N. Belnap and M. Perloff. Seeing to it that: a canonical form for agentives. Theoria, 54:175--199, 1988.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- 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.Google ScholarCross Ref
- I. Boureanu, M. Cohen, and A. Lomuscio. Model checking detectability of attacks in multiagent systems. In Proceedings of AAMAS, pages 691--698, 2010. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- I. Boureanu, P. Kouvaros, and A. Lomuscio. Verifying security properties in unbounded multiagent systems. In Proceedings of AAMAS, pages 1209--1217, 2016. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- J. W. Bryans, M. Koutny, and P. Y. Ryan. Modelling opacity using petri nets. Electronic Notes in Theoretical Computer Science, 121:101--115, 2005.Google ScholarDigital Library
- R. Chadha, S. Kremer, and A. Scedrov. Formal analysis of multiparty contract signing. Journal of Automated Reasoning, 36(1-2):39--83, 2006. Google ScholarDigital Library
- K. Chatterjee, T. A. Henzinger, and N. Piterman. Strategy logic. In Proceedings of CONCUR, pages 59--73, 2007. Google ScholarDigital Library
- D. Chaum, P. Y. A. Ryan, and S. A. Schneider. A practical voter-verifiable election scheme. In Proceedings of ESORICS, pages 118--139, 2005. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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.Google Scholar
- 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.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- A. Herzig and N. Troquard. Knowing how to play: Uniform choices in logics of agency. In Proceedings of AAMAS'06, pages 209--216, 2006. Google ScholarDigital Library
- 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.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- W. Jamroga and W. van der Hoek. Agents that know how to play. Fundamenta Informaticae, 63(2-3):185--219, 2004. Google ScholarDigital Library
- H. L. Jonker and W. Pieters. Receipt-freeness as a special case of anonymity in epistemic logic. 2006.Google Scholar
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- S. Kremer and J.-F. Raskin. A game-based verification of non-repudiation and fair exchange protocols. Journal of Computer Security, 11(3), 2003. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- A. Lomuscio and W. Penczek. LDYIS: a framework for model checking security protocols. Fundamenta Informaticae, 85(1-4):359--375, 2008. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- B. Meng. A critical review of receipt-freeness and coercion-resistance. Information Technology Journal, 8(7):934--964, 2009.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- 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. Google ScholarDigital Library
- F. Mogavero, A. Murano, and M. Vardi. Reasoning about strategies. In Proceedings of FSTTCS, pages 133--144, 2010.Google Scholar
- T. Moran and M. Naor. Receipt-free universally-verifiable voting with everlasting privacy. In Advances in Cryptology-CRYPTO 2006, pages 373--392. Springer, 2006. Google ScholarDigital Library
- T. Okamoto. Receipt-free electronic voting schemes for large scale elections. In Security Protocols, pages 25--35. Springer, 1998. Google ScholarDigital Library
- T. Peacock and P. Ryan. Coercion-resistance as opacity in voting systems. Technical Report Series-University Of Newcatle Upon Tyne Computing Science, 959, 2006.Google Scholar
- P. Y. A. Ryan. The computer ate my vote. In Formal Methods: State of the Art and New Directions, pages 147--184. Springer, 2010.Google Scholar
- 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. Google ScholarDigital Library
- H. Schnoor. Strategic planning for probabilistic games with incomplete information. In Proceedings of AAMAS'10, pages 1057--1064, 2010. Google ScholarDigital Library
- P. Y. Schobbens. Alternating-time logic with imperfect recall. Electronic Notes in Theoretical Computer Science, 85(2):82--93, 2004.Google ScholarCross Ref
- 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. Google ScholarDigital Library
- Expressing Receipt-Freeness and Coercion-Resistance in Logics of Strategic Ability: Preliminary Attempt
Recommendations
Coercion-Resistance and Receipt-Freeness in Electronic Voting
CSFW '06: Proceedings of the 19th IEEE workshop on Computer Security FoundationsIn 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 TechnologyMany 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