Abstract:
In the last couple of decades a large number of reliable e-voting protocols
are introduced. However, it is quite challenging to completely verify these
protocols quantitatively due to their distributive nature and complex structures. In this paper, we propose a formal approach, based on probabilistic
model checking, to analyze and compare the performance of contemporary
electronic voting protocols. The rigour of this technique allows us to completely assess the security and correctness of E-voting protocols and thus
would in turn help in conducting secure and error-free elections. For illustration purposes, we compare two E-voting protocols, i.e., a cryptographic
and a non-cryptographic protocol. Other than formally verifying these protocols, we also provide a comparison, in terms of computational speed and
performance, between the two state-of-the-art probabilistic model checkers,
i.e., PRISM and Storm, in this context.
