{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,10]],"date-time":"2026-06-10T16:29:07Z","timestamp":1781108947971,"version":"3.54.1"},"reference-count":25,"publisher":"IGI Global Scientific Publishing","issue":"2","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013,4,1]]},"abstract":"<p>Electronic voting protocols have many advantages over traditional voting but they are complex and subject to many kinds of attacks. Therefore, the use of formal verification methods is crucial to ensure some security properties. We propose to model a recent protocol of remote electronic voting in the applied Pi-calculus. We focalized on some security properties such as fairness which expresses the impossibility of obtaining partial results, eligibility which requires that only legitimate voters can vote, coercion resistance which ensures that no voter may vote under pressure, and verifiability which supposes that anyone can verify the accuracy of the final result. We proved either manually or using the automated verification tool ProVerif that the protocol satisfies these security properties.<\/p>","DOI":"10.4018\/jisp.2013040104","type":"journal-article","created":{"date-parts":[[2013,9,27]],"date-time":"2013-09-27T11:29:40Z","timestamp":1380281380000},"page":"57-85","source":"Crossref","is-referenced-by-count":0,"title":["Formal Verification of Secrecy, Coercion Resistance and Verifiability Properties for a Remote Electronic Voting Protocol"],"prefix":"10.4018","volume":"7","author":[{"given":"Khaoula","family":"Marzouki","sequence":"first","affiliation":[{"name":"LIP2-LR99ES18, Faculty of Science of Tunis, Tunis-El Manar University, Tunis, Tunisia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Amira","family":"Radhouani","sequence":"additional","affiliation":[{"name":"LIP2-LR99ES18, Faculty of Science of Tunis, Tunis-El Manar University, Tunis, Tunisia"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Narjes","family":"Ben Rajeb","sequence":"additional","affiliation":[{"name":"INSAT, LIP2-LR99ES18, Carthage University, Tunis, Tunisia"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"2432","reference":[{"key":"jisp.2013040104-0","first-page":"104","article-title":"Mobile values, new names, and secure communication.","volume":"28","author":"M.Abadi","year":"2001","journal-title":"Financial Cryptography and Data Security"},{"key":"jisp.2013040104-1","doi-asserted-by":"crossref","unstructured":"Araujo, R., Rajeb, N. B., Robbana, R., Traor, J., & Youssfi, S. (2010). Towards practical and secure coercion-resistant electronic elections. CAN\u2019s, 278-297.","DOI":"10.1007\/978-3-642-17619-7_20"},{"key":"jisp.2013040104-2","doi-asserted-by":"crossref","unstructured":"Backes, M., Hritcu, C., & Maei, M. (2008). Automated verification of remote electronic voting protocols in the applied picalculus. In Proceedings of the IEEE Computer Security Foundations Symposium, 21.","DOI":"10.1109\/CSF.2008.26"},{"key":"jisp.2013040104-3","unstructured":"Blanchet, B. (2006). V\u2019erification automatique de protocoles cryptographiques: Mod\u00e8le formel et mod\u00e8le calculatoire. Unpublished doctoral dissertation, Paris-Dauphin University."},{"key":"jisp.2013040104-4","unstructured":"Chaum, D., Ryan, P. Y. A., & Schneider, S. (2005). A practical, voter-veriable election scheme. In Proceedings of the 10th European Symposium On Research In Computer Security (ESORICS05) (pp. 3679)."},{"key":"jisp.2013040104-5","unstructured":"Chevallier-Mames, B., Fouque, P.-A., Pointcheval, D., Stern, J., & Traore, J. (2006). On some incompatible properties of voting schemes. In Proceedings of the International Association for Voting Systems Sciences Workshop on Trustworthy Elections (WOTE06)."},{"key":"jisp.2013040104-6","unstructured":"Delaune, S., & Kremer, S. (2009). Sp\u00b4ecificites des protocoles de vote \u00e9lectronique. Deliverable AVOTE 1.1."},{"key":"jisp.2013040104-7","doi-asserted-by":"crossref","unstructured":"Delaune, S., Kremer, S., & Ryan, M. (2009). Verifying privacy-type properties of electronic voting protocols. Journal of Computer Security, 435-487.","DOI":"10.3233\/JCS-2009-0340"},{"key":"jisp.2013040104-8","doi-asserted-by":"crossref","unstructured":"Delaune, S., Ryan, M., & Smyth, B. (2008). Automatic verification of privacy properties in the applied pi-calculus. In Proceedings of the Ifiptm\u201908: 2nd Joint iTrust and PST Conferences on Privacy, Trust Management and Security (Vol. 263, pp. 263-278). Springer.","DOI":"10.1007\/978-0-387-09428-1_17"},{"key":"jisp.2013040104-9","unstructured":"Dreier, J., Ene, C., Lafourcade, P., & Lakhnech, Y. (2011). On unique decomposition of processes in the applied calculus (Tech. Rep. No. TR-2012-3). Verimag Research Report."},{"key":"jisp.2013040104-10","doi-asserted-by":"crossref","unstructured":"ElGamal, T. (1985). A public key cryptosystem and a signature scheme based on discrete logarithms. Advances in cryptology (CRYPTO 84), 132.","DOI":"10.1007\/3-540-39568-7_2"},{"key":"jisp.2013040104-11","doi-asserted-by":"crossref","unstructured":"Fujioka, A., Okamoto, T., & Ohta, K. (1992). A practical secret voting scheme for large scale elections. In Proceedings of Advances in Cryptology (AUSCRYPT92), 718 of LNCS.","DOI":"10.1007\/3-540-57220-1_66"},{"key":"jisp.2013040104-12","doi-asserted-by":"crossref","unstructured":"Jakobsson, M., & Juels, A. (2000). Mix and match: Secure function evaluation via ciphertext. T. Okamoto (Ed.), ASIACRYPT, 1976 of Lecture Notes in Computer Science.","DOI":"10.1007\/3-540-44448-3_13"},{"key":"jisp.2013040104-13","doi-asserted-by":"crossref","unstructured":"Jakobsson, M., Sako, K., & Impagliazzol, R. (1996). Designated verifier proofs and their applications. EUROCRYPT 96.","DOI":"10.1007\/3-540-68339-9_13"},{"key":"jisp.2013040104-14","doi-asserted-by":"crossref","unstructured":"Juels, A., Catalano, D., & Jakobsson, M. (2005). Coercion-resistant electronic elections. In Proceedings of the Workshop on Privacy in the Electronic Society (WPES 05) (pp. 61-70).","DOI":"10.1145\/1102199.1102213"},{"key":"jisp.2013040104-15","unstructured":"Kremer, S., & Ryan, M. (2005a). Analysis of an electronic voting protocol in the applied pi-calculus. Deliverable AVOTE 1.1 (ANR-07-SESU-002), 344."},{"key":"jisp.2013040104-16","unstructured":"Kremer, S., & Ryan, M. (2005b). Analysis of an electronic voting protocol in the applied pi calculus. In Proceedings of the 4th European Symposium on Programming (ESOP05), 3444 of LNCS."},{"key":"jisp.2013040104-17","doi-asserted-by":"crossref","unstructured":"Kremer, S., Ryan, M., & Smyth, B. (2010). Election verifiability in electronic voting protocols. In Proceedings of the European Symposium on Research in Computer Security, 15.","DOI":"10.1007\/978-3-642-15497-3_24"},{"key":"jisp.2013040104-18","doi-asserted-by":"crossref","unstructured":"Kusters, R., & Truderung, T. (2009). Using proverif to analyze protocols with di_e-hellman exponentiation. IEEE Computer Security Foundations Symposium, 22, 157-171.","DOI":"10.1109\/CSF.2009.17"},{"key":"jisp.2013040104-19","unstructured":"Lafourcade, P. (2006). V\u2019erification de protocoles cryptographiques en pr\u00e9sence de th\u00e9ories \u00e9quationnelles. Unpublished doctoral dissertation, LEcole Normale Sup\u2019erieure de CACHAN."},{"key":"jisp.2013040104-20","doi-asserted-by":"crossref","unstructured":"Lee, B., Boyd, C., Dawson, E., Yang, J., Kim, K., & Yoo, S. (2004). Providing receipt-freeness in mixnet-based voting protocols. In Proceedings of the Information Security and Cryptology (ICISC03), 2971 of LNCS.","DOI":"10.1007\/978-3-540-24691-6_19"},{"key":"jisp.2013040104-21","unstructured":"Pieters, W. (2006). What proof do we prefer? Variants of variability in voting. In Proceedings of the Workshop on Electronic Voting and e-Government in the UK (pp. 33-39)."},{"key":"jisp.2013040104-22","unstructured":"Ryan, M., & Smyth, B. (2010). Formal models and techniques for analyzing security protocols. IOS Press, 2(6)."},{"key":"jisp.2013040104-23","article-title":"Applied pi calculus","author":"M.Ryan","year":"2011","journal-title":"Formal models and techniques for analyzing security protocols"},{"key":"jisp.2013040104-24","unstructured":"Weber, S. G. (2012). On transaction pseudonyms with implicit attributes. IACR Cryptology ePrint Archive, (pp. 568\u2013568)."}],"container-title":["International Journal of Information Security and Privacy"],"original-title":[],"language":"ng","link":[{"URL":"https:\/\/www.igi-global.com\/viewtitle.aspx?TitleId=87425","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,6,1]],"date-time":"2022-06-01T23:09:42Z","timestamp":1654124982000},"score":1,"resource":{"primary":{"URL":"https:\/\/services.igi-global.com\/resolvedoi\/resolve.aspx?doi=10.4018\/jisp.2013040104"}},"subtitle":[""],"short-title":[],"issued":{"date-parts":[[2013,4,1]]},"references-count":25,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2013,4]]}},"URL":"https:\/\/doi.org\/10.4018\/jisp.2013040104","relation":{},"ISSN":["1930-1650","1930-1669"],"issn-type":[{"value":"1930-1650","type":"print"},{"value":"1930-1669","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,4,1]]}}}