×

Analysis of an electronic voting protocol in the applied pi calculus. (English) Zbl 1108.68462

Sagiv, Mooly (ed.), Programming languages and systems. 14th European symposium on programming, ESOP 2005, held as part of the joint European conferences on theory and practice of software, ETAPS 2005, Edinburgh, UK, April 4–8, 2005. Proceedings. Berlin: Springer (ISBN 3-540-25435-8/pbk). Lecture Notes in Computer Science 3444, 186-200 (2005).
Summary: 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.
For the entire collection see [Zbl 1068.68008].

MSC:

68P25 Data encryption (aspects in computer science)
68Q60 Specification and verification (program logics, model checking, etc.)

Software:

ProVerif
PDFBibTeX XMLCite
Full Text: DOI