Sage Journals: Discover world-class research

Abstract

Norway used e-voting in its last political election both in September 2011 and September 2013, with more than 28,000 voters using the e-voting option in 2011, and 70,000 in 2013. While some other countries use a black-box, proprietary voting solution, Norway has made its system publicly available. The underlying protocol, designed by Scytl, involves several authorities (a ballot box, a receipt generator, a decryption service, and an auditor). Of course, trusting the correctness and security of e-voting protocols is crucial in that context. In this paper, we propose a formal analysis of the protocol used in Norway, w.r.t. ballot secrecy, considering several corruption scenarios. We use a state-of-the-art definition of ballot secrecy, based on equivalence properties and stated in the applied pi-calculus.

Keywords

Ballot secrecy formal methods e-voting

Get full access to this article

View all access options for this article.

References

Abadi and

Fournet, Mobile values, new names, and secure communication, in: 28th ACM Symposium on Principles of Programming Languages (POPL), 2001.

Arapinis,

Bursuc and

Ryan, Reduction of equational theories for verification of trace equivalence: Re-encryption and AC, in: First International Conference on Principles of Security and Trust (POST’12), Springer, 2012.

Arapinis,

Cortier and

Kremer, When are three voters enough for privacy properties? in: Proceedings of the 21st European Symposium on Research in Computer Security (ESORICS’16), 2016.

Armando,

Basin,

Boichut,

Chevalier,

Compagna,

Cuellar,

Hankes Drielsma,

P.-C.

Héam,

Kouchnarenko,

Mantovani,

Mödersheim,

von Oheimb,

Rusinowitch,

Santiago,

Turuani,

Viganò and

Vigneron, The AVISPA tool for the automated validation of Internet security protocols and applications, in: 17th International Conference on Computer Aided Verification (CAV), 2005.

Basin,

Dreier and

Sasse, Automated symbolic proofs of observational equivalence, in: ACM Conference on Computer and Communications Security (CCS’15), 2015.

Benaloh,

M.D.

Byrne,

Eakin,

P.T.

Kortum,

McBurnett,

Pereira,

P.B.

Stark,

D.S.

Wallach,

Fisher,

Montoya,

Parker and

Winn, STAR-Vote: A secure, transparent, auditable, and reliable voting system, in: 2013 Electronic Voting Technology Workshop/Workshop on Trustworthy Elections (EVT/WOTE’13), 2013.

Bernhard,

Cortier,

Pereira,

Smyth and

Warinschi, Adapting helios for provable ballot secrecy, in: 16th European Symposium on Research in Computer Security (ESORICS), 2011.

Bernhard,

Pereira and

Warinschi, How not to prove yourself: Pitfalls of the fiat-shamir heuristic and applications to helios, in: International Conference on the Theory and Application of Cryptology and Information Security (ASIACRYPT), 2012.

Bhargavan,

Corin,

Fournet and

Zalinescu, Cryptographically verified implementations for TLS, in: 15th ACM Conference on Computer and Communications Security (CCS), 2008.

10.

Blanchet, An automatic security protocol verifier based on resolution theorem proving (invited tutorial), in: 20th International Conference on Automated Deduction (CADE), 2005.

11.

Blanchet, Vérification Automatique de Protocoles Cryptographiques: Modèle Formel et Modèle Calculatoire. Mémoire d’habilitation à diriger des recherches, Université Paris-Dauphine, 2008.

12.

Blanchet,

Abadi and

Fournet, Automated verification of selected equivalences for security protocols, Journal of Logical and Algebraic Methods in Programming (2008).

13.

Chadha,

Ş.

Ciobâcă and

Kremer, Automated verification of equivalence properties of cryptographic protocols, in: 21th European Symposium on Programming (ESOP), 2012.

14.

Chaum,

Carback,

Clark,

Essex,

Popoveniuc,

R.L.

Rivest,

P.Y.A.

Ryan,

Shen,

A.T.

Sherman and

P.L.

Vora, Corrections to scantegrity II: End-to-end verifiability by voters of optical scan elections through confirmation codes, IEEE Trans. Information Forensics and Security 5(1) (2010), 194. doi:10.1109/TIFS.2010.2040672.

15.

Cheval,

Comon-Lundh and

Delaune, Trace equivalence decision: Negative tests and non-determinism, in: 18th ACM Conference on Computer and Communications Security (CCS), 2011.

16.

Cortier and

Delaune, A method for proving observational equivalence, in: 22nd Computer Security Foundations Symposium (CSF), 2009.

17.

Cortier and

Smyth, Attacking and fixing helios: An analysis of ballot secrecy, Journal of Computer Security (2013).

18.

Cortier and

Wiedling, A formal analysis of the Norwegian E-voting protocol, in: First International Conference on Principles of Security and Trust (POST), 2012.

19.

Cramer,

Gennaro and

Schoenmakers, A secure and optimally efficient multi-authority election scheme, in: International Conference on the Theory and Application of Cryptographic Techniques (EuroCrypt), 1997.

20.

Cremers, The scyther tool: Verification, falsification, and analysis of security protocols, in: 20th International Conference of Computer Aided Verification (CAV), 2008.

21.

Delaune,

Kremer and

Ryan, Verifying privacy-type properties of electronic voting protocols, Journal of Computer Security (2009).

22.

Fujioka,

Okamoto and

Ohta, A practical secret voting scheme for large scale elections, in: Workshop on the Theory and Application of Cryptographic Techniques: Advances in Cryptology, 1992.

23.

Gjøsteen, Analysis of an internet voting protocol. Cryptology ePrint Archive, Report 2010/380, 2010.

24.

Gjøsteen, The Norwegian internet voting protocol. Cryptology ePrint Archive, Report 2013/473, 2013.

25.

Government, Article of the Norwegian government on the deployment of E-voting (last seen: 08-26-16), https://www.regjeringen.no/en/aktuelt/Internet-voting-pilot-to-be-discontinued/id764300/.

26.

Halderman and

Teague, The new South Wales iVote system: Security failures and verification flaws in a live online election, in: 5th International Conference on E-voting and Identity (VoteID’15), 2015.

27.

Khader and

P.Y.A.

Ryan, Receipt freeness of Prêt à voter provably secure. IACR Cryptology ePrint Archive, 2011:594, 2011.

28.

Klus,

Smyth and

M.D.

Ryan, ProSwapper: Improved equivalence verifier for ProVerif (last seen: 08-26-16), 2010, http://www.bensmyth.com/proswapper.php.

29.

Küsters and

Truderung, An epistemic approach to coercion-resistance for electronic voting protocols, in: IEEE Symposium on Security and Privacy (S&P), 2009.

30.

Lee,

Boyd,

Dawson,

Kim,

Yang and

Yoo, Providing receipt-freeness in mixnet-based voting protocols, in: 6th International Conference on Information Security and Cryptology (ICISC), 2004.

31.

Liu, A proof of coincidence of labeled bisimilarity and observational equivalence in applied pi calculus, 2011, http://lcs.ios.ac.cn/~jliu/papers/LiuJia0608.pdf.

32.

Ohkubo,

Miura,

Abe,

Fujioka and

Okamoto, An improvement on a practical secret voting scheme, in: 2nd International Information Security Workshop (ISW), 1999.

33.

A.T.

Sherman,

Carback,

Chaum,

Clark,

Essex,

P.S.

Herrnson,

Mayberry,

Popoveniuc,

R.L.

Rivest,

Shen,

Sinha and

P.L.

Vora, Scantegrity mock election at Takoma Park, in: 4th International Conference on Electronic Voting 2010 (EVOTE’10), 2010, pp. 45–61.

34.

Tiu and

J.E.

Dawson, Automating open bisimulation checking for the spi calculus, in: 3rd IEEE Computer Security Foundations Symposium (CSF), 2010.

35.

Wiedling, Source files for ProVerif code, http://people.rennes.inria.fr/Cyrille.Wiedling/Resources/resources.html.