Electronic voting is now used in many countries and in many elections, from small elections such as parents representatives in schools, to politically binding elections. Electronic voting facilitates counting and enables a wide variety of elections, such as preferential voting where voters rank their candidates by order of preference. In such a case, counting the votes by hand can be a very complex task that can, in contrast, easily be handled by a computer. Another advantage of electronic voting is that voters may vote from anywhere and it can last several weeks if needed. It is often used at least as a replacement of postal voting. However, electronic voting also comes with security threats and has been subject to severe attacks. For example, the Washington, D.C., Internet voting system has been attacked [7], during a trial just before the election. Recently, Switzerland has stopped temporarily using electronic voting after a public penetration test that has revealed severe weaknesses [6]. Ideally, electronic voting should offer the same guarantees that traditional paper-based election. In particular, it should guarantee vote privacy (no one should know how I voted) and verifiability: anyone should be able to check that the votes are accurately counted and correspond to the voters intent. In this talk, we will present the Belenios voting protocol [4] that has been used in more than 500 elections in 2020, through its voting platform1. We will discuss its security properties as well as its limitations. As for security protocols in general, the design of electronic voting systems is error-prone and it is hard to assess whether a protocol ensures the required security properties. For these reasons, a common good practice is to design a protocol together with a formal security analysis, as it has been done in the context of TLS1.3 [5] for example. The Swiss Chancellerie requires both computational and formal proofs of security before the deployment of an electronic voting system [1]. We will explain how the tools developed for the automated analysis of security protocols, like ProVerif [3], can help gaining a better confidence in e-voting protocols. One particular issue in the context of voting is that the formalization of security properties is still an on-going work, even for crucial properties like vote secrecy [2]. Hence electronic voting still raises many challenges for our research community.
展开▼
