Abstract
E-voting protocols aim at achieving a wide range of sophisticated security properties and, consequently, commonly employ advanced cryptographic primitives. This makes their design as well as rigorous analysis quite challenging. As a matter of fact, existing automated analysis techniques, which are mostly based on automated theorem provers, are inadequate to deal with commonly used cryptographic primitives, such as homomorphic encryption and mix-nets, as well as some fundamental security properties, such as verifiability.
This work presents a novel approach based on refinement type systems for the automated analysis of e-voting protocols. Specifically, we design a generically applicable logical theory which, based on pre- and post-conditions for security-critical code, captures and guides the type-checker towards the verification of two fundamental properties of e-voting protocols, namely, vote privacy and verifiability. We further develop a code-based cryptographic abstraction of the cryptographic primitives commonly used in e-voting protocols, showing how to make the underlying algebraic properties accessible to automated verification through logical refinements. Finally, we demonstrate the effectiveness of our approach by developing the first automated analysis of Helios, a popular web-based e-voting protocol, using an off-the-shelf type-checker.
Chapter PDF
References
Adida, B.: Helios: Web-based Open-Audit Voting. In: USENIX 2008, pp. 335–348 (2008)
Arapinis, M., Cortier, V., Kremer, S., Ryan, M.D.: Practical Everlasting Privacy. In: POST 2013, pp. 21–40 (2013)
Armando, A., Carbone, R., Compagna, L., Cuellar, J., Tobarra, L.: Formal analysis of SAML 2.0 web browser single sign-on: breaking the SAML-based single sign-on for Google Apps. In: FMSE 2008, pp. 1–10 (2008)
Backes, M., Cortesi, A., Focardi, R., Maffei, M.: A calculus of challenges and responses. In: FMSE 2007, pp. 51–60 (2007)
Backes, M., Cortesi, A., Maffei, M.: Causality-based abstraction of multiplicity in security protocols. In: CSF 2007, pp. 355–369 (2007)
Backes, M., Grochulla, M.P., Hritcu, C., Maffei, M.: Achieving security despite compromise using zero-knowledge. In: CSF 2009, pp. 308–323 (2009)
Backes, M., Hriţcu, C., Maffei, M.: Automated Verification of Remote Electronic Voting Protocols in the Applied Pi-calculus. In: CSF 2008, pp. 195–209 (2008)
Backes, M., Lorenz, S., Maffei, M., Pecina, K.: The CASPA Tool: Causality-Based Abstraction for Security Protocol Analysis. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 419–422. Springer, Heidelberg (2008)
Backes, M., Hriţcu, C., Maffei, M.: Union and Intersection Types for Secure Protocol Implementations. In: Mödersheim, S., Palamidessi, C. (eds.) TOSCA 2011. LNCS, vol. 6993, pp. 1–28. Springer, Heidelberg (2012)
Backes, M., Maffei, M., Hriţcu, C.: Union and Intersection Types for Secure Protocol Implementations. JCS, 301–353 (2014)
Backes, M., Maffei, M., Unruh, D.: Computationally Sound Verification of Source Code. In: CCS 2010, pp. 387–398 (2010)
Barthe, G., Fournet, C., Grégoire, B., Strub, P., Swamy, N., Béguelin, S.Z.: Probabilistic Relational Verification for Cryptographic Implementations. In: POPL 2014, pp. 193–206 (2014)
Bengtson, J., Bhargavan, K., Fournet, C., Gordon, A.D., Maffeis, S.: Refinement Types for Secure Implementations. TOPLAS 33(2), 8 (2011)
Bernhard, D., Cortier, V., Pereira, O., Smyth, B., Warinschi, B.: Adapting Helios for provable ballot secrecy. In: Atluri, V., Diaz, C. (eds.) ESORICS 2011. LNCS, vol. 6879, pp. 335–354. Springer, Heidelberg (2011)
Blanchet, B.: An Efficient Cryptographic Protocol Verifier Based on Prolog Rules. In: CSFW 2001, pp. 82–96 (2001)
Blanchet, B., Abadi, M., Fournet, C.: Automated Verification of Selected Equivalences for Security Protocols. JLAP 75(1), 3–51 (2008)
Bortolozzo, M., Centenaro, M., Focardi, R., Steel, G.: Attacking and Fixing PKCS#11 Security Tokens. In: CCS 2010, pp. 260–269 (2010)
Bugliesi, M., Focardi, R., Maffei, M.: Analysis of typed-based analyses of authentication protocols. In: CSFW 2005, pp. 112–125. IEEE (2005)
Bugliesi, M., Focardi, R., Maffei, M.: Dynamic types for authentication. JCS 15(6), 563–617 (2007)
Bugliesi, M., Calzavara, S., Eigner, F., Maffei, M.: Resource-aware Authorization Policies in Statically Typed Cryptographic Protocols. In: CSF 2011, pp. 83–98 (2011)
Bugliesi, M., Calzavara, S., Eigner, F., Maffei, M.: Logical Foundations of Secure Resource Management in Protocol Implementations. In: Basin, D., Mitchell, J.C. (eds.) POST 2013. LNCS, vol. 7796, pp. 105–125. Springer, Heidelberg (2013)
Bugliesi, M., Focardi, R., Maffei, M.: Principles for entity authentication. In: Broy, M., Zamulin, A.V. (eds.) PSI 2003. LNCS, vol. 2890, pp. 294–306. Springer, Heidelberg (2003)
Bugliesi, M., Focardi, R., Maffei, M.: Authenticity by tagging and typing. In: FMSE 2004, pp. 1–12 (2004)
Chadha, R., Ciobâcă, Ş., Kremer, S.: Automated verification of equivalence properties of cryptographic protocols. In: ESOP 2012, pp. 108–127 (2012)
Cheval, V.: APTE: an Algorithm for Proving Trace Equivalence. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 587–592. Springer, Heidelberg (2014)
Cohen, J.D., Fischer, M.J.: A Robust and Verifiable Cryptographically Secure Election Scheme. In: FOCS 1985, pp. 372–382 (1985)
Cortier, V., Eigner, F., Kremer, S., Maffei, M., Wiedling, C.: Type-Based Verification of Electronic Voting Protocols. Cryptology ePrint Archive, Report 2015/039 (2015)
Cortier, V., Galindo, D., Glondu, S., Izabachène, M.: Election Verifiability for Helios under Weaker Trust Assumptions. In: Kutyłowski, M., Vaidya, J. (eds.) ICAIS 2014, Part II. LNCS, vol. 8713, pp. 327–344. Springer, Heidelberg (2014)
Cortier, V., Smyth, B.: Attacking and fixing Helios: An analysis of ballot secrecy. In: CSF 2011, pp. 297–311 (2011)
Cortier, V., Wiedling, C.: A formal analysis of the Norwegian E-voting protocol. In: POST 2012, pp. 109–128 (2012)
Cramer, R., Gennaro, R., Schoenmakers, B.: A Secure and Optimally Efficient Multi-Authority Election Scheme. In: Fumy, W. (ed.) EUROCRYPT 1997. LNCS, vol. 1233, pp. 103–118. Springer, Heidelberg (1997)
Cremers, C.: The Scyther Tool: Verification, Falsification, and Analysis of Security Protocols. In: CAV 2008, pp. 414–418 (2008)
Delaune, S., Kremer, S., Ryan, M.D.: Verifying privacy-type properties of electronic voting protocols. JCS 17(4), 435–487 (2009)
Eigner, F., Maffei, M.: Differential Privacy by Typing in Security Protocols. In: CSF 2013, pp. 272–286. IEEE (2013)
Estehghari, S., Desmedt, Y.: Exploiting the Client Vulnerabilities in Internet E-voting Systems: Hacking Helios 2.0 as an Example. In: EVT/WOTE 2010 (2010)
Focardi, R., Maffei, M.: Types for security protocols. In: Formal Models and Techniques for Analyzing Security Protocols. IOS (2011)
Fournet, C., Kohlweiss, M., Strub, P.: Modular Code-Based Cryptographic Verification. In: CCS 2011, pp. 341–350 (2011)
Fujioka, A., Okamoto, T., Ohta, K.: A Practical Secret Voting Scheme for Large Scale Elections. In: Zheng, Y., Seberry, J. (eds.) AUSCRYPT 1992. LNCS, vol. 718, pp. 244–251. Springer, Heidelberg (1993)
Gordon, A.D., Jeffrey, A.: Types and effects for asymmetric cryptographic protocols. JCS 12(3), 435–484 (2004)
IACR. Elections page at http://www.siacr.org/elections/
Juels, A., Catalano, D., Jakobsson, M.: Coercion-Resistant Electronic Elections. In: Chaum, D., Jakobsson, M., Rivest, R.L., Ryan, P.Y.A., Benaloh, J., Kutylowski, M., Adida, B. (eds.) Towards Trustworthy Elections. LNCS, vol. 6000, pp. 37–63. Springer, Heidelberg (2010)
Kremer, S., Ryan, M.D.: Analysis of an Electronic Voting Protocol in the Applied Pi Calculus. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 186–200. Springer, Heidelberg (2005)
Kremer, S., Ryan, M., Smyth, B.: Election verifiability in electronic voting protocols. In: Gritzalis, D., Preneel, B., Theoharidou, M. (eds.) ESORICS 2010. LNCS, vol. 6345, pp. 389–404. Springer, Heidelberg (2010)
Küsters, R., Truderung, T., Vogt, A.: Clash Attacks on the Verifiability of E-Voting Systems. In: S&P 2012, pp. 395–409 (2012)
Küsters, R., Truderung, T., Vogt, A.: A Game-Based Definition of Coercion-Resistance and its Applications. In: CSF 2010, pp. 122–136 (2010)
Küsters, R., Truderung, T., Vogt, A.: Accountabiliy: Definition and Relationship to Verifiability. In: CCS 2010, pp. 526–535 (2010)
Küsters, R., Truderung, T., Vogt, A.: Verifiability, Privacy, and Coercion-Resistance: New Insights from a Case Study. In: S&P 2011, pp. 538–553 (2011)
Lowe, G.: Breaking and Fixing the Needham-Schroeder Public-Key Protocol using FDR. In: Margaria, T., Steffen, B. (eds.) TACAS 1996. LNCS, vol. 1055, pp. 147–166. Springer, Heidelberg (1996)
Morris, J.: Protection in Programming Languages. CACM 16(1), 15–21 (1973)
de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
Rivest, R.L.: The threeballot voting system, unpublished draft (2006)
Smyth, B., Ryan, M., Kremer, S., Kourjieh, M.: Towards automatic analysis of election verifiability properties. In: Armando, A., Lowe, G. (eds.) ARSPA-WITS 2010. LNCS, vol. 6186, pp. 146–163. Springer, Heidelberg (2010)
Sumii, E., Pierce, B.: A Bisimulation for Dynamic Sealing. TCS 375(1-3), 169–192 (2007)
Swamy, N., Chen, J., Fournet, C., Strub, P.Y., Bhargavan, K., Yang, J.: Secure Distributed Programming with Value-Dependent Types. In: ICFP 2011, pp. 266–278 (2011)
Wagner, D., Schneier, B.: Analysis of the SSL 3.0 protocol. In: USENIX Workshop on Electronic Commerce, pp. 29–40 (1996)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Cortier, V., Eigner, F., Kremer, S., Maffei, M., Wiedling, C. (2015). Type-Based Verification of Electronic Voting Protocols. In: Focardi, R., Myers, A. (eds) Principles of Security and Trust. POST 2015. Lecture Notes in Computer Science(), vol 9036. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-46666-7_16
Download citation
DOI: https://doi.org/10.1007/978-3-662-46666-7_16
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-46665-0
Online ISBN: 978-3-662-46666-7
eBook Packages: Computer ScienceComputer Science (R0)