{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:57:26Z","timestamp":1762459046959},"reference-count":48,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2014,1]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>\n            We present formal definitions of anonymity properties for voting protocols using the process algebra CSP. We analyse a number of anonymity definitions, and give formal definitions for\n            <jats:italic>strong<\/jats:italic>\n            and\n            <jats:italic>weak<\/jats:italic>\n            anonymity, highlighting the difference between these definitions. We show that the strong anonymity definition is too strong for practical purposes; the weak anonymity definition, however, turns out to be ideal for analysing voting systems. Two case studies are presented to demonstrate the usefulness of the formal definitions: a conventional voting system, and Pr\u00eat \u00e0 Voter, a paper-based, voter-verifiable scheme. In each case, we give a CSP model of the system, and analyse it against our anonymity definitions by specification checks using the Failures-Divergences Refinement (FDR2) model checker. We give a detailed discussion on the results from the analysis, emphasizing the assumptions that we made in our model as well as the challenges in modelling electronic voting systems using CSP.\n          <\/jats:p>","DOI":"10.1007\/s00165-012-0268-x","type":"journal-article","created":{"date-parts":[[2012,12,5]],"date-time":"2012-12-05T20:25:49Z","timestamp":1354739149000},"page":"63-98","source":"Crossref","is-referenced-by-count":8,"title":["Verifying anonymity in voting systems using CSP"],"prefix":"10.1145","volume":"26","author":[{"given":"Murat","family":"Moran","sequence":"first","affiliation":[{"name":"Department of Computing, University of Surrey, Guildford, GU2 7XH, Surrey, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"James","family":"Heather","sequence":"additional","affiliation":[{"name":"Department of Computing, University of Surrey, Guildford, GU2 7XH, Surrey, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Steve","family":"Schneider","sequence":"additional","affiliation":[{"name":"Department of Computing, University of Surrey, Guildford, GU2 7XH, Surrey, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","unstructured":"Adida B (2008) Helios: web-based open-audit voting. In: Proceedings of the 17th USENIX security symposium pp 335\u2013348"},{"key":"e_1_2_1_2_2_2","doi-asserted-by":"crossref","unstructured":"Boneh D Golle P (2002) Almost entirely correct mixing with applications to voting. In: Proceedings of the 9th ACM conference on computer and communications security CCS \u201902. ACM New York pp 68\u201377","DOI":"10.1145\/586110.586121"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Backes M Hritcu C Maffei M (2008) Automated verification of remote electronic voting protocols in the applied pi-calculus. In: CSF pp 195\u2013209","DOI":"10.1109\/CSF.2008.26"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Bhargava M Palamidessi C (2005) Probabilistic anonymity. In: Abadi M de Alfaro L (eds) CONCUR 2005\u2014concurrency theory. Lecture notes in computer science vol 3653. Springer Berlin pp 171\u2013185","DOI":"10.1007\/11539452_16"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Baskar A Ramanujam R Suresh SP (2007) Knowledge-based modelling of voting protocols. In: TARK pp 62\u201371","DOI":"10.1145\/1324249.1324261"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Clarkson MR Chong S Myers AC (2008) Civitas: toward a secure voting system. In: IEEE symposium on security and privacy pp 354\u2013368","DOI":"10.1109\/SP.2008.32"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"publisher","DOI":"10.1109\/MSP.2008.70"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/358549.358563"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"publisher","DOI":"10.1109\/MSECP.2004.1264852"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Chothia T Orzan S Pang J Dashti MT (2006) A framework for automatically checking anonymity with MuCRL. In: TGC pp 301\u2013318","DOI":"10.1007\/978-3-540-75336-0_19"},{"key":"e_1_2_1_2_11_2","volume-title":"In: Information and computation.","author":"Chatzikokolakis K","year":"2006"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"crossref","unstructured":"Chaum D Ryan PYA Schneider SA (2005) A practical voter-verifiable election scheme. In: ESORICS pp 118\u2013139","DOI":"10.1007\/11555827_8"},{"key":"e_1_2_1_2_13_2","unstructured":"Delaune S Kremer S Ryan M (2006) Coercion-resistance and receipt-freeness in electronic voting. In: CSFW pp 28\u201342"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"publisher","DOI":"10.5555\/1576303.1576305"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.05.047"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"publisher","DOI":"10.1109\/TIT.1983.1056650"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"ElGamal T (1984) A public key cryptosystem and a signature scheme based on discrete logarithms. In: CRYPTO pp 10\u201318","DOI":"10.1007\/3-540-39568-7_2"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"crossref","unstructured":"Fournet C Abadi M (2002) Hiding names: private authentication in the applied pi calculus. In: ISSS pp 317\u2013338","DOI":"10.1007\/3-540-36532-X_20"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Fujioka A Okamoto T Ohta K (1992) A practical secret voting scheme for large scale elections. In: AUSCRYPT pp 244\u2013251","DOI":"10.1007\/3-540-57220-1_66"},{"key":"e_1_2_1_2_20_2","unstructured":"Gardiner P Goldsmith M Hulance J Jackson D Roscoe B Scattergood B Armstrong B. FDR2 user manual"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"Garcia FD Hasuo I Pieters W van Rossum P (2005) Provable anonymity. In: Proceedings of the 2005 ACM workshop on formal methods in security engineering FMSE \u201905. ACM New York pp 63\u201372","DOI":"10.1145\/1103576.1103585"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Heather J (2007) Implementing STV securely in Pr\u00eat \u00e0 Voter. In: CSF pp 157\u2013169","DOI":"10.1109\/CSF.2007.22"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/359576.359585"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"publisher","DOI":"10.5555\/1297689.1297694"},{"key":"e_1_2_1_2_25_2","doi-asserted-by":"crossref","unstructured":"Juels A Catalano D Jakobsson M (2005) Coercion-resistant electronic elections. In: Proceedings of the 2005 ACM workshop on privacy in the electronic society WPES \u201905. ACM New York pp 61\u201370","DOI":"10.1145\/1102199.1102213"},{"key":"e_1_2_1_2_26_2","unstructured":"Jakobsson M Juels A Rivest RL (2002) Making mix nets robust for electronic voting by randomized partial checking. In: USENIX security symposium pp 339\u2013353"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"Kremer S Ryan M (2005) Analysis of an electronic voting protocol in the applied pi calculus. In: ESOP pp 186\u2013200","DOI":"10.1007\/978-3-540-31987-0_14"},{"key":"e_1_2_1_2_28_2","unstructured":"Lazic RS (1999) A semantic study of data independence with applications to model checking. D. phil. thesis Oxford University Computing Laboratory"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Langer BL Jonker H Pieters W (2010) Anonymity and verifiability in voting: understanding (un)linkability. In: ICICS pp 296\u2013310","DOI":"10.1007\/978-3-642-17650-0_21"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"crossref","unstructured":"Lowe G (1996) Breaking and fixing the needham-schroeder public-key protocol using FDR. In: Proceedings of the second international workshop on tools and algorithms for construction and analysis of systems. Springer Berlin pp 147\u2013166","DOI":"10.1007\/3-540-61042-1_43"},{"key":"e_1_2_1_2_31_2","doi-asserted-by":"crossref","unstructured":"Mauw S Verschuren J de Vink EP. (2004) A formalization of anonymity and onion routing. In ESORICS pages 109\u2013124","DOI":"10.1007\/978-3-540-30108-0_7"},{"key":"e_1_2_1_2_32_2","doi-asserted-by":"crossref","unstructured":"Andrew Neff C (2001) A verifiable secret shuffle and its application to e-voting. In: Proceedings of the 8th ACM conference on computer and communications security CCS \u201901. ACM New York pp 116\u2013125","DOI":"10.1145\/501983.502000"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"Paillier P (1999) Public-key cryptosystems based on composite degree residuosity classes. In: EUROCRYPT pp 223\u2013238","DOI":"10.1007\/3-540-48910-X_16"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"crossref","unstructured":"Pfitzmann P K\u00f6hntopp M (2000) Anonymity unobservability and pseudonymity\u2014a proposal for terminology. In: Workshop on design issues in anonymity and unobservability pp 1\u20139","DOI":"10.1007\/3-540-44702-4_1"},{"issue":"4","key":"e_1_2_1_2_35_2","first-page":"662","article-title":"Pr\u00eat \u00e0 Voter: a voter-verifiable voting system","volume":"4","author":"Ryan PYA","year":"2009","journal-title":"IEEE Trans Inf Theory"},{"key":"e_1_2_1_2_36_2","unstructured":"Rivest RL (2006) The ThreeBallot voting system. http:\/\/theory.csail.mit.edu\/~rivest\/Rivest-TheThreeBallotVotingSystem.pdf."},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"publisher","DOI":"10.5555\/550448"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"publisher","DOI":"10.5555\/1941861"},{"key":"e_1_2_1_2_39_2","unstructured":"Ryan PYA Peacock T (2005) Pr\u00eat \u00e0 Voter: a systems perspective. Technical report University of Newcastle"},{"key":"e_1_2_1_2_40_2","doi-asserted-by":"crossref","unstructured":"Ryan PYA Peacock T (2010) A threat analysis of Pr\u00eat \u00e0 Voter. In: Chaum D Jakobsson M Rivest R Ryan P Benaloh J Kutylowski M Adida B (eds) Towards trustworthy elections. Lecture notes in computer science vol 6000. Springer Berlin pp 200\u2013215","DOI":"10.1007\/978-3-642-12980-3_12"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"crossref","unstructured":"Ryan PYA Schneider SA (2006) Pr\u00eat \u00e0 Voter with re-encryption mixes. In: ESORICS pp 313\u2013326","DOI":"10.1007\/11863908_20"},{"key":"e_1_2_1_2_42_2","unstructured":"Ryan PYA Schneider SA Goldsmith MH Lowe G Roscoe AW (2000) The modelling and analysis of security protocols: the CSP approach 1 edn. Addison-Wesley Professional Reading"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"crossref","unstructured":"Ryan PYA (2005) A variant of the Chaum voter-verifiable scheme. In: Proceedings of 2005 workshop on issues in the theory of security pp 81\u201388","DOI":"10.1145\/1045405.1045414"},{"key":"e_1_2_1_2_44_2","doi-asserted-by":"crossref","unstructured":"Ryan PYA (2006) Putting the human back in voting protocols. In: Security protocols workshop pp 20\u201325","DOI":"10.1007\/978-3-642-04904-0_4"},{"issue":"1","key":"e_1_2_1_2_45_2","doi-asserted-by":"crossref","first-page":"1646","DOI":"10.1016\/j.mcm.2008.05.015","article-title":"Pr\u00eat \u00e0 Voter with Paillier encryption","volume":"48","author":"Ryan PYA","year":"2008","journal-title":"Math Comput Model"},{"key":"e_1_2_1_2_46_2","doi-asserted-by":"publisher","DOI":"10.5555\/555233"},{"key":"e_1_2_1_2_47_2","doi-asserted-by":"crossref","unstructured":"Schneider SA Sidiropoulos A (1996) CSP and anonymity. In: ESORICS pp 198\u2013218","DOI":"10.1007\/3-540-61770-1_38"},{"key":"e_1_2_1_2_48_2","doi-asserted-by":"crossref","unstructured":"Xia Z Culnane C Heather J Jonker H Ryan PYA Schneider SA Srinivasan S (2010) Versatile Pr\u00eat \u00e0 Voter: handling multiple election methods with a unified interface. In: INDOCRYPT pp 98\u2013114","DOI":"10.1007\/978-3-642-17401-8_8"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-012-0268-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-012-0268-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-012-0268-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,6]],"date-time":"2022-01-06T16:01:59Z","timestamp":1641484919000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-012-0268-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,1]]},"references-count":48,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2014,1]]}},"alternative-id":["10.1007\/s00165-012-0268-x"],"URL":"https:\/\/doi.org\/10.1007\/s00165-012-0268-x","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,1]]}}}