Abstract
Electronic voting promises the possibility of a convenient, efficient and secure facility for recording and tallying votes in an election. Recently highlighted inadequacies of implemented systems have demonstrated the importance of formally verifying the underlying voting protocols. The applied pi calculus is a formalism for modelling such protocols, and allows us to verify properties by using automatic tools, and to rely on manual proof techniques for cases that automatic tools are unable to handle. We model a known protocol for elections known as FOO 92 in the applied pi calculus, and we formalise three of its expected properties, namely fairness, eligibility, and privacy. We use the ProVerif tool to prove that the first two properties are satisfied. In the case of the third property, ProVerif is unable to prove it directly, because its ability to prove observational equivalence between processes is not complete. We provide a manual proof of the required equivalence.
Chapter PDF
Similar content being viewed by others
References
Abadi, M., Blanchet, B., Fournet, C.: Just fast keying in the pi calculus. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 340–354. Springer, Heidelberg (2004)
Abadi, M., Cortier, V.: Deciding knowledge in security protocols under equational theories. In: Díaz, J., Karhumäki, J., Lepistö, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol. 3142, pp. 46–58. Springer, Heidelberg (2004)
Abadi, M., Fournet, C.: Mobile values, new names, and secure communication. In: Nielson, H.R. (ed.) Proceedings of the 28th ACM Symposium on Principles of Programming Languages, London, UK, January 2001, pp. 104–115. ACM Press, New York (2001)
Blanchet, B.: An efficient cryptographic protocol verifier based on prolog rules. In: Schneider, S. (ed.) 14th IEEE Computer Security Foundations Workshop, Cape Breton, Nova Scotia, Canada, June 2001, pp. 82–96. IEEE Computer Society Press, Los Alamitos (2001)
Blanchet, B.: Automatic Proof of Strong Secrecy for Security Protocols. In: IEEE Symposium on Security and Privacy, Oakland, California, May 2004, pp. 86–100 (2004)
Chadha, R., Kremer, S., Scedrov, A.: Formal analysis of multi-party contract signing. In: Focardi, R. (ed.) 17th IEEE Computer Security Foundations Workshop, Asilomar, CA, USA, June 2004, pp. 266–279. IEEE Computer Society Press, Los Alamitos (2004)
Chaum, D.: Blind signatures for untraceable payments. In: Advances in Cryptology, Proceedings of CRYPTO 1982, pp. 199–203. Plenum Press, New York (1983)
Corin, R., Doumen, J., Etalle, S.: Analysing password protocol security against off-line dictionary attacks. In: 2nd International Workshop on Security Issues with Petri Nets and other Computational Models (WISP 2004). Electronic Notes in Theoretical Computer Science. Elsevier, Amsterdam (2004) (to appear)
Véronique Cortier. Personal communication (2004)
Delaune, S., Jacquemard, F.: A theory of dictionary attacks and its complexity. In: Focardi, R. (ed.) 17th IEEE Computer Security Foundations Workshop, Asilomar, Pacific Grove, CA, USA, June 2004, pp. 2–15. IEEE Computer Society Press, Los Alamitos (2004)
Fournet, C., Abadi, M.: Hiding names: Private authentication in the applied pi calculus. In: Okada, M., Pierce, B.C., Scedrov, A., Tokuda, H., Yonezawa, A. (eds.) ISSS 2002. LNCS, vol. 2609, pp. 317–338. Springer, Heidelberg (2003)
Fujioka, A., Okamoto, T., Ohta, K.: A practical secret voting scheme for large scale elections. In: Zheng, Y., Seberry, J. (eds.) AUSCRYPT 1992. LNCS, vol. 718, pp. 244–251. Springer, Heidelberg (1993)
Kohno, T., Stubblefield, A., Rubin, A.D., Wallach, D.S.: Analysis of an electronic voting system. In: IEEE Symposium on Security and Privacy. IEEE Computer Society Press, Los Alamitos (2004)
Lowe, G.: An attack on the Needham-Schroeder public-key authentication protocol. Information Processing Letters 56, 131–133 (1995)
Lowe, G.: Analysing protocols subject to guessing attacks. In: Guttman, J. (ed.) Proceedings of the Workshop on Issues in the Theory of Security (WITS 2002), Portland, Oregon, USA (January 2002)
Zuzana Rjaskova. Electronic voting schemes. Master’s thesis, Comenius University (2002), http://www.tcs.hut.fi/~helger/crypto/link/protocols/voting.html
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kremer, S., Ryan, M. (2005). Analysis of an Electronic Voting Protocol in the Applied Pi Calculus. In: Sagiv, M. (eds) Programming Languages and Systems. ESOP 2005. Lecture Notes in Computer Science, vol 3444. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-31987-0_14
Download citation
DOI: https://doi.org/10.1007/978-3-540-31987-0_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25435-5
Online ISBN: 978-3-540-31987-0
eBook Packages: Computer ScienceComputer Science (R0)Springer Nature Proceedings Computer Science
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.