[en] Security properties are often focused on the technological side of the system. One implicitly assumes that the users will behave in the right way to preserve the property at hand. In real life, this cannot be taken for granted. In particular, security mechanisms that are difficult and costly to use are often ignored by the users, and do not really defend the system against possible attacks.Here, we propose a graded notion of security based on the complexity of the user’s strategic behavior. More precisely, we suggest that the level to which a security property φ is satisfied can be defined in terms of (a)the complexity of the strategy that the voter needs to execute to make φ true, and (b) the resources that the user must employ on the way. The simpler and cheaper to obtain φ, the higher the degree of security. We demonstrate how the idea works in a case study based on an electronicv oting scenario. To this end, we model the vVote implementation of thePrˆet `a Voter voting protocol for coercion-resistant and voter-verifiable elections. Then, we identify “natural” strategies for the voter to obtain receipt-freeness, and measure the voter’s effort that they require. We also look at how hard it is for the coercer to compromise the election through a randomization attack.
Disciplines :
Sciences informatiques
Auteur, co-auteur :
JAMROGA, Wojciech ; University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > APSIA
Kurpiewski, Damian
Malvone, Vadim
Co-auteurs externes :
yes
Langue du document :
Anglais
Titre :
Natural Strategic Abilities in Voting Protocols
Date de publication/diffusion :
2020
Nom de la manifestation :
10th International Workshop on Socio-Technical Aspects in Security STAST 2020
Date de la manifestation :
17/18 Sept 2020
Manifestation à portée :
International
Titre de l'ouvrage principal :
Proceedings of the 10th International Workshop on Socio-Technical Aspects in Security STAST 2020
Ågotnes, T., Goranko, V., Jamroga, W., Wooldridge, M.: Knowledge and ability. In: Handbook of Epistemic Logic, pp. 543–589 (2015)
Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM 49, 672–713 (2002)
Basin, D., Gersbach, H., Mamageishvili, A., Schmid, L., Tejada, O.: Election security and economics: it’s all about eve. In: Krimmer, R., Volkamer, M., Braun Binder, N., Kersting, N., Pereira, O., Schürmann, C. (eds.) E-Vote-ID 2017. LNCS, vol. 10615, pp. 1–20. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-68687-5 1
Basin, D.A., Radomirovic, S., Schmid, L.: Modeling human errors in security protocols. In: CSF, pp. 325–340 (2016)
Behrmann, G., David, A., Larsen, K.G.: A tutorial on Uppaal. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30080-9 7
Bella, G., Curzon, P., Giustolisi, R., Lenzini, G.: A socio-technical methodology for the security and privacy analysis of services. In: COMPSAC, pp. 401–406 (2014)
Bella, G., Curzon, P., Lenzini, G.: Service security and privacy as a socio-technical problem. J. Comput. Secur. 23(5), 563–585 (2015)
Benaloh, J., Tuinstra, D.: Receipt-free secret-ballot elections. In: ACM symposium on Theory of Computing, pp. 544–553 (1994)
Bourne, L.E.: Knowing and using concepts. Psychol. Rev. 77, 546–556 (1970)
Buldas, A., Mägi, T.: Practical security analysis of E-voting systems. In: Miyaji, A., Kikuchi, H., Rannenberg, K. (eds.) IWSEC 2007. LNCS, vol. 4752, pp. 320–335. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-75651-4 22
Carlos, M.C., Martina, J.E., Price, G., Custódio, R.F.: A proposed framework for analysing security ceremonies. In: SECRYPT, pp. 440–445 (2012)
Cortier, V., Galindo, D., Küsters, R., Müller, J., Truderung, T.: SoK: verifiability notions for e-voting protocols. In: IEEE Symposium on Security and Privacy, pp. 779–798 (2016)
Delaune, S., Kremer, S., Ryan, M.: Coercion-resistance and receipt-freeness in electronic voting. In: CSF, 12-pp (2006)
Dreier, J., Lafourcade, P., Lakhnech, Y.: A formal taxonomy of privacy in voting protocols. In: ICC, pp. 6710–6715 (2012)
Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning about Knowledge. MIT Press, Cambridge (1995)
Feldman, J.: Minimization of Boolean complexity in human concept learning. Nature 407, 630–633 (2000)
Ghallab, M., Nau, D., Traverso, P.: Automated Planning: Theory and Practice. Morgan Kaufmann, San Francisco (2004)
Hunker, J., Probst, C.W.: Insiders and insider threats-an overview of definitions and mitigation techniques. J. Wirel. Mob. Networks Ubiquitous Comput. Dependable Appl. 2(1), 4–27 (2011)
Jamroga, W., Knapik, M., Kurpiewski, D.: Model checking the SELENE E-voting protocol in multi-agent logics. In: Krimmer, R., Volkamer, M., Cortier, V., Goré, R., Hapsara, M., Serdült, U., Duenas-Cid, D. (eds.) E-Vote-ID 2018. LNCS, vol. 11143, pp. 100–116. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-00419-4 7
Jamroga, W., Malvone, V., Murano, A.: Reasoning about natural strategic ability. In: AAMAS, pp. 714–722 (2017)
Jamroga, W., Malvone, V., Murano, A.: A.: Natural strategic ability under imperfect information. In: AAMAS, pp. 962–970 (2019)
Jamroga, W., Tabatabaei, M.: Preventing coercion in E-voting: be open and commit. In: Krimmer, R., Volkamer, M., Barrat, J., Benaloh, J., Goodman, N., Ryan, P.Y.A., Teague, V. (eds.) E-Vote-ID 2016. LNCS, vol. 10141, pp. 1–17. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-52240-1 1
Jamroga, W., van der Hoek, W.: Agents that know how to play. Fund. Inform. 63(2–3), 185–219 (2004)
Juels, A., Catalano, D., Jakobsson, M.: Coercion-resistant electronic elections. In: ACM Workshop on Privacy in the Electronic Society, pp. 61–70 (2005)
Küsters, R., Truderung, T., Vogt, A.: A game-based definition of coercion-resistance and its applications. In: IEEE Computer Security Foundations Symposium, pp. 122–136 (2010)
Martimiano, T., Dos Santos, E., Olembo, M., Martina, J.E.: Ceremony analysis meets verifiable voting: individual verifiability in Helios. In: SECURWARE, pp. 169–183 (2015)
Martimiano, T., Martina, J.E.: Threat modelling service security as a security ceremony. In: ARES, pp. 195–204 (2016)
Mogavero, F., Murano, A., Perelli, G., Vardi, M.Y.: Reasoning about strategies: on the model-checking problem. ACM Trans. Comput. Log. 15(4), 1–42 (2014)
Okamoto, T.: Receipt-free electronic voting schemes for large scale elections. In: Christianson, B., Crispo, B., Lomas, M., Roe, M. (eds.) Security Protocols 1997. LNCS, vol. 1361, pp. 25–35. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0028157
P. Y. A. Ryan. The computer ate my vote. In: Boca, P., Bowen, J., Siddiqi, J. (eds.) Formal Methods: State of the Art and New Directions, pp. 147–184. Springer, London (2010). https://doi.org/10.1007/978-1-84882-736-3 5
Ryan, P.Y.A., Schneider, S.A., Teague, V.: End-to-end verifiability in voting systems, from theory to practice. IEEE Secur. Privacy 13(3), 59–62 (2015)
Santos, F.P.: Dynamics of reputation and the self-organization of cooperation. Ph.D. thesis, University of Lisbon (2018)
Santos, F.P., Santos, F.C., Pacheco, J.M.: Social norm complexity and past reputations in the evolution of cooperation. Nature 555, 242–245 (2018)
Shoham, Y., Leyton-Brown, K.: Multiagent Systems-Algorithmic, Game-Theoretic, and Logical Foundations. Cambridge University Press, New York (2009)
Tabatabaei, M., Jamroga, W., Peter, Ryan, Y.A.: Expressing receipt-freeness and coercion-resistance in logics of strategic ability: preliminary attempt. In: PrAISe@ECAI 2016, pp. 1:1–1:8 (2016)
Verified Voting. Policy on direct recording electronic voting machines and ballot marking devices (2019)
