Formalizing Voting Protocol in Process Algebra

Ainita Ban(1*), Zarina Shukur(2)

(1) Faculty of Information Science and Technology, Universiti Kebangsaan, Malaysia
(2) Universiti Kebangsaaan, Malaysia
(*) Corresponding author

DOI's assignment:
the author of the article can submit here a request for assignment of a DOI number to this resource!
Cost of the service: euros 10,00 (for a DOI)


Electronic voting can be seen as one of the best alternatives of today’s election for it will provide many advantages such as efficient and accurate data management and accumulation as well as convenience to voters. In order to gain confidence and trust among people to implement electronic voting system, a formal method is chosen. Formal method has been proven successfully in verifying properties. This paper presents work of specifying voting protocol formally using CSP (Communicating Sequential Process). We demonstrated the work on two voting. The first protocol was using blind signature based while the second was blind signature and threshold IBE (Identity Based Encryption) scheme. The specification will be used in verifying properties of voting protocol in later work.
Copyright © 2020 Praise Worthy Prize - All rights reserved.


Voting Protocol; Formal Specification; CSP; Blind Signature

Full Text:



Rjaskova, Z., 2002. Electronic voting schemes. M.S. thesis, Department of Computer Science Faculty of Mathematics, Physics and Informatics, University of Comenius

Roscoe, A.W., 1995. Modelling and verifying key-exchange protocols using csp and fdr. In: In 8th IEEE Computer Security Foundations Workshop, pp: 98–107

Lowe, G., 1996. Breaking and fixing the needham-schroeder public-key protocol using fdr. In: TACAs ’96: Proceedings of the Second International Workshop on Tools and Algorithms for Construction and Analysis of Systems, London, UK, Springer-Verlag, pp: 147–166

Lowe, G., 1998. Casper: A compiler for the analysis of security protocols. Journal of Computer Security, Society Press, pp: 53–84

Juels, A., Catalano, D. and Jakobsson, M., 2005. Coercion-resistant electronic elections (Extended Abastract). Proceedings of the 2005 ACM workshop on Privacy in the electronic society, pp: 61-70.

Kremer, S., Ryan, M., 2005. Analysis of an electronic voting protocol in the applied picalculus.In: In European Symposium on Programming, number 3444 in Lecture Notes in Computer Science, Springer, pp: 186–200

Delaune, S., Kremer, S. and Ryan, M., 2006. Coercion-resistance and receipt-freeness in electronic voting. Computer Security Foundations Workshop. 19th IEEE, pp: 28-42.

Novotný, M. 2009. Design and Analysis of a Practical E-Voting Protocol. The Future of Identity in the Information Society, IFIP Advances in Information and Communication Technology. ( 298), pp: 170-183.

Fujioka, A., Okamoto, T., Ohta, K., 1993. A practical secret voting scheme for large scale elections. In: ASIACRYPT ’92: Proceedings of the Workshop on the Theory and Application of Cryptographic Techniques, London, UK, Springer-Verlag (1993), pp: 244–251

Gallegos-G,G., Gómez-C, M., Duchén-S, G.I., 2010. Identity based threshold cryptography and blind signatures for electronic voting. W. Trans. on Comp. 9, 1 (January 2010), pp: 62-71.

Failures-Divergence Refinement: FDR2 User Manual. Formal Systems (Europe) Ltd. Retreived on: 20/6/11.

Meng, B. 2007. An Internet Voting Protocol with Receipt-Free and Coercion-Resistant, Computer and Information Technology, 2007. CIT 2007. 7th IEEE International Conference, pp: 721-726.


  • There are currently no refbacks.

Please send any question about this web site to
Copyright © 2005-2022 Praise Worthy Prize