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