Analysis of electronic ballot transmission protocols in the applied pi calculus - Wuysang, Danny Francis
In this research, we perform formal analysis of transmission protocols used in electronic voting. We used the applied pi-calculus, a formal language for concurrent and communicating processes with extensions that are particularly advantageous in modeling cryptographic protocols. We begin by formally modeling the two protocols being studied in the calculus. These protocols are based on real-life systems, which are designed specifically for election systems where results must be transmitted between election authorities hierarchically. The models are then slightly modified into scripts that will allow verification using ProVerif, a tool to derive automated proof in the applied pi-calculus. We proceed to verify security properties, namely secrecy, authentication, and privacy, of these protocols with combination of automated derivations and hand proofs. Firstly, results on secrecy show the security of one scheme, while exposing the weakness of the other. The latter was proven to be vulnerable as expected, because encryption was not implemented. During secrecy analysis, we observed the case of corrupt administrator. Secondly, results on authentication show similar outcome for both protocols. Correspondence was achieved, but not injectivity, which is due to the absence of authentication protocol. Thirdly, results on privacy show that one scheme is more secure than the other, this is also because no encryption was employed. Based on verification and analysis, we finally suggest solutions for authentication and corrupt administrator problems. Solutions were formally shown to mitigate those problems. Components that are proven to be secure are suggested to be our formally verified electronic ballot transmission protocol.