Sage Journals: Discover world-class research

Abstract

Formal analysis of security is often focused on the technological side of the system. One implicitly assumes that the users will behave in the right way to preserve the relevant security properties. 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 user 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 electronic voting scenario. To this end, we model the vVote implementation of the Prêt à Voter voting protocol for coercion-resistant and voter-verifiable elections. Then, we identify “natural” strategies for the voter to obtain voter-verifiability, and measure the voter’s effort that they require. We also consider the dual view of graded security, measured by the complexity of the attacker’s strategy to compromise the relevant properties of the election.

Keywords

Electronic voting coercion resistance natural strategies multi-agent models graded security

Get full access to this article

View all access options for this article.

References

Ågotnes,

Goranko,

Jamroga and

Wooldridge, Knowledge and ability, in: Handbook of Epistemic Logic,

H.P.

van Ditmarsch,

J.Y.

Halpern,

van der Hoek and

B.P.

Kooi, eds, College Publications, 2015, pp. 543–589.

Alur,

T.A.

Henzinger and

Kupferman, Alternating-time temporal logic, Journal of the ACM49 (2002), 672–713. doi:10.1145/585265.585270.

D.A.

Basin,

Gersbach,

Mamageishvili,

Schmid and

Tejada, Election security and economics: It’s all about eve, in: Proceedings of E-Vote-ID, 2017, pp. 1–20.

D.A.

Basin,

Radomirovic and

Schmid, Modeling human errors in security protocols, in: Computer Security Foundations Symposium, CSF, IEEE Computer Society, 2016, pp. 325–340.

Behrmann,

David and

K.G.

Larsen, A tutorial on uppaal, in: Formal Methods for the Design of Real-Time Systems: SFM-RT, LNCS, Vol. 3185, Springer, 2004, pp. 200–236. doi:10.1007/978-3-540-30080-9_7.

Bella and

Coles-Kemp, Layered analysis of security ceremonies, in: Information Security and Privacy Research – 27th IFIP TC 11 Information Security and Privacy Conference, Section 2012, Proceedings, Heraklion, Crete, Greece, June 4–6, 2012, IFIP Advances in Information and Communication Technology, Vol. 376, Springer, 2012, pp. 273–286. doi:10.1007/978-3-642-30436-1_23.

Bella,

Curzon,

Giustolisi and

Lenzini, A socio-technical methodology for the security and privacy analysis of services, in: COMPSAC Workshops, IEEE Computer Society, 2014, pp. 401–406.

Bella,

Curzon and

Lenzini, Service security and privacy as a socio-technical problem, J. Comput. Secur.23(5) (2015), 563–585. doi:10.3233/JCS-150536.

Benaloh and

Tuinstra, Receipt-free secret-ballot elections, in: Proceedings of the Twenty-Sixth Annual ACM Symposium on Theory of Computing, ACM, 1994, pp. 544–553.

10.

Bernhard,

McDonald,

Meng,

Hwa,

Bajaj,

Chang and

J.A.

Halderman, Can voters detect malicious manipulation of ballot marking devices? in: IEEE Symposium on Security and Privacy, IEEE, 2020, pp. 679–694.

11.

L.E.

Bourne, Knowing and using concepts, Psychol. Rev.77 (1970), 546–556. doi:10.1037/h0030000.

12.

Buldas and

Mägi, Practical security analysis of e-voting systems, in: Proceedings of IWSEC, Lecture Notes in Computer Science, Vol. 4752, Springer, 2007, pp. 320–335.

13.

Burton,

Culnane and

S.A.

Schneider, Secure and verifiable electronic voting in practice: The use of vVote in the Victorian state election, 2015, CoRR arXiv:1504.07098.

14.

Carlomagno Carlos,

Everson Martina,

Price and

R.F.

Custódio, A proposed framework for analysing security ceremonies, in: SECRYPT, SciTePress, 2012, pp. 440–445.

15.

Chatterjee,

T.A.

Henzinger and

Piterman, Strategy Logic. Information and Computation208(6) (2010), 677–693. doi:10.1016/j.ic.2009.07.004.

16.

Cortier,

Galindo,

Küsters,

Müller and

T.T.

SoK, Verifiability notions for e-voting protocols, in: IEEE Symposium on Security and Privacy, 2016, pp. 779–798.

17.

Culnane,

P.Y.A.

Ryan,

S.A.

Schneider and

Teague, vvote: A verifiable voting system, ACM Trans. Inf. Syst. Secur.18(1) (2015), 3:1–3:30. doi:10.1145/2746338.

18.

Culnane and

Teague, Strategies for voter-initiated election audits, in: Decision and Game Theory for Security: Proceedings of GameSec, Lecture Notes in Computer Science, Vol. 9996, Springer, 2016, pp. 235–247.

19.

David,

Rydhof Hansen,

Guldstrand Larsen,

Legay,

M.C.

Olesen and

C.W.

Probst, Modelling social-technical attacks with timed automata, in: Proceedings of International Workshop on Managing Insider Security Threats, MIST, ACM, 2015, pp. 21–28.

20.

Davis and

Marcus, Commonsense reasoning, Communications of the ACM58(9) (2015), 92–103. doi:10.1145/2701413.

21.

Delaune,

Kremer and

Ryan, Coercion-resistance and receipt-freeness in electronic voting, in: Computer Security Foundations Workshop, 2006. 19th IEEE, IEEE, 2006, pp. 12.

22.

Distler,

M.-L.

Zollinger,

Lallemand,

P.B.

Rønne,

P.Y.A.

Ryan and

Koenig, Security – visible, yet unseen? in: Proceedings of Conference on Human Factors in Computing Systems, CHI, ACM, 2019, p. 605.

23.

Dreier,

Lafourcade and

Lakhnech, A formal taxonomy of privacy in voting protocols, in: Communications (ICC), 2012 IEEE International Conference on, IEEE, 2012, pp. 6710–6715. doi:10.1109/ICC.2012.6364938.

24.

Fagin,

J.Y.

Halpern,

Moses and

M.Y.

Vardi, Reasoning About Knowledge, MIT Press, 1995.

25.

Feldman, Minimization of Boolean complexity in human concept learning, Nature407 (2000), 630. doi:10.1038/35036586.

26.

Ghallab,

Nau and

Traverso, Automated Planning: Theory and Practice, Morgan Kaufmann, 2004.

27.

Gjøsteen and

A.S.

Lund, An experiment on the security of the Norwegian electronic voting protocol, Ann. des Télécommunications71(7–8) (2016), 299–307. doi:10.1007/s12243-016-0509-8.

28.

Hassenzahl and

Tractinsky, User experience-a research agenda, Behaviour & Information Technology25(2) (2006), 91–97. doi:10.1080/01449290500330331.

29.

Hunker and

C.W.

Probst, Insiders and insider threats – an overview of definitions and mitigation techniques, J. Wirel. Mob. Networks Ubiquitous Comput. Dependable Appl.2(1) (2011), 4–27.

30.

Jamroga,

Kim,

Kurpiewski and

P.Y.A.

Ryan, Towards model checking of voting protocols in uppaal, in: Proceedings of E-Vote-ID, Lecture Notes in Computer Science, Vol. 12455, Springer, 2020, pp. 129–146.

31.

Jamroga,

Knapik and

Kurpiewski, Model checking the SELENE e-voting protocol in multi-agent logics, in: Proceedings of the 3rd International Joint Conference on Electronic Voting (E-VOTE-ID), Lecture Notes in Computer Science, Vol. 11143, Springer, 2018, pp. 100–116.

32.

Jamroga,

Kurpiewski and

Malvone, Natural strategic abilities in voting protocols, in: Proceedings of STAST 2020, 2021, To appear.

33.

Jamroga,

Malvone and

Murano, Reasoning about natural strategic ability, in: Proceedings of the 16th International Conference on Autonomous Agents and Multiagent Systems (AAMAS), IFAAMAS, 2017, pp. 714–722.

34.

Jamroga,

Malvone and

Murano, Natural strategic ability, Artificial Intelligence277 (2019).

35.

Jamroga,

Malvone and

Murano, Natural strategic ability under imperfect information, in: Proceedings of the 18th International Conference on Autonomous Agents and Multiagent Systems AAMAS 2019, IFAAMAS, 2019, pp. 962–970.

36.

Jamroga and

Tabatabaei, Preventing coercion in e-voting: Be open and commit, in: Electronic Voting: Proceedings of E-Vote-ID 2016, Lecture Notes in Computer Science, Vol. 10141, Springer, 2017, pp. 1–17. doi:10.1007/978-3-319-52240-1_1.

37.

Jamroga and

van der Hoek, Agents that know how to play, Fundamenta Informaticae63(2–3) (2004), 185–219.

38.

Juels,

Catalano and

Jakobsson, Coercion-resistant electronic elections, in: Proceedings of the 2005 ACM Workshop on Privacy in the Electronic Society, ACM, 2005, pp. 61–70. doi:10.1145/1102199.1102213.

39.

Kulyk,

Volkamer,

Müller and

Renaud, Towards improving the efficacy of code-based verification in Internet voting, in: Financial Cryptography and Data Security Workshops, Revised Selected Papers, Lecture Notes in Computer Science, Vol. 12063, Springer, 2020, pp. 291–309. doi:10.1007/978-3-030-54455-3_21.

40.

Küsters,

Truderung and

Vogt, A game-based definition of coercion-resistance and its applications, in: Proceedings of the 2010 23rd IEEE Computer Security Foundations Symposium, IEEE Computer Society, 2010, pp. 122–136. doi:10.1109/CSF.2010.16.

41.

Kwiatkowska,

Norman and

Parker, PRISM: Probabilistic symbolic model checker, in: Proceedings of TOOLS, Lecture Notes in Computer Science, Vol. 2324, Springer, 2002, pp. 200–204.

42.

Lomuscio,

Qu and

Raimondi, MCMAS: An open-source model checker for the verification of multi-agent systems, Int. J. Softw. Tools Technol. Transf.19(1) (2017), 9–30. doi:10.1007/s10009-015-0378-x.

43.

Marky,

Kulyk,

Renaud and

Volkamer, What did I really vote for? in: Proceedings of Conference on Human Factors in Computing Systems, CHI, ACM, 2018, p. 176.

44.

Marky,

M.-L.

Zollinger,

Funk,

P.Y.A.

Ryan and

Mühlhäuser, How to assess the usability metrics of e-voting schemes, in: Financial Cryptography Workshops, LNCS, Vol. 11599, Springer, 2019, pp. 257–271.

45.

Martimiano,

Dos Santos,

Olembo and

J.E.

Martina, Ceremony analysis meets verifiable voting: Individual verifiability in Helios, in: SECURWARE, 2015.

46.

Martimiano and

Everson Martina, Threat modelling service security as a security ceremony, in: 11th International Conference on Availability, Reliability and Security, ARES, IEEE Computer Society, 2016, pp. 195–204.

47.

Mogavero,

Murano,

Perelli and

M.Y.

Vardi, Reasoning about strategies: On the model-checking problem, ACM Transactions on Computational Logic15(4) (2014), 1–42. doi:10.1145/2631917.

48.

Okamoto, Receipt-free electronic voting schemes for large scale elections, in: Security Protocols, Springer, 1998, pp. 25–35. doi:10.1007/BFb0028157.

49.

Radulescu,

Mannion,

D.M.

Roijers and

Nowé, Multi-objective multi-agent decision making: A utility-based analysis and survey, Autonomous Agents and Multi Agent Systems34(1) (2020), 10. doi:10.1007/s10458-019-09433-x.

50.

P.Y.A.

Ryan, The computer ate my vote, in: Formal Methods: State of the Art and New Directions, Springer, 2010, pp. 147–184. doi:10.1007/978-1-84882-736-3_5.

51.

P.Y.A.

Ryan,

S.A.

Schneider and

Teague, End-to-end verifiability in voting systems, from theory to practice, IEEE Security & Privacy13(3) (2015), 59–62. doi:10.1109/MSP.2015.54.

52.

F.P.

Santos, Dynamics of Reputation and the Self-organization of Cooperation, PhD thesis, University of Lisbon, 2018.

53.

F.P.

Santos,

F.C.

Santos and

J.M.

Pacheco, Social norm complexity and past reputations in the evolution of cooperation, Nature555 (2018), 242–245. doi:10.1038/nature25763.

54.

Shoham and

Leyton-Brown, Multiagent Systems – Algorithmic, Game-Theoretic, and Logical Foundations, Cambridge University Press, 2009.

55.

Soegaard and

Friis Dam (eds), The Glossary of Human Computer Interaction, Interaction Design Foundation.

56.

Tabatabaei,

Jamroga and

P.Y.A.

Ryan, Expressing receipt-freeness and coercion-resistance in logics of strategic ability: Preliminary attempt, in: Proceedings of the 1st International Workshop on AI for Privacy and Security, PrAISe@ECAI 2016, ACM, 2016, pp. 1:1–1:8.

57.

Verified Voting. Policy on direct recording electronic voting machines and ballot marking devices, 2019.

58.

Zionts, A multiple criteria method for choosing among discrete alternatives, European Journal of Operational Research7(2) (1981), 143–147.

How to measure usable security: Natural strategies in voting protocols 1

Abstract

Keywords

Get full access to this article

References