Introduction

The organization of an election in Italy involves various offices of the Public Administration and private contractors, has a time-span of months, and has strict security and traceability requirements. Sensibility by citizens and politicians is very high, and litigation over, e.g., implementation of procedures and validity of results are not uncommon. As an example, one of the major candidates at the last general elections in Italy distributed -- via the website of his party -- a leaflet describing possible misconducts of poll-officers during elections and some counter-measures. The goal of the leaflet was help ensuring that poll-officers of the opposing party could not try and illegally alter the results of the election.

We are involved in a project named ProVotE [1] that it is related to the evaluation and possible introduction of e-voting for local elections held in the Autonomous Province of Trento, Italy. The e-voting system developed within the project has been used with experimental value by more than ten thousand citizens and with legal value in two small elections, making the initiative the largest experimentation of e-Voting in Italy, so far. The switch to electronic elections in Italy, however, is a long and difficult process, that requires extreme attention to all the aspects characterizing an (electronic) election, including a thorough understanding of the limits and the security breaches that are inherent in the procedures and/or that derive from a combination of procedures and systems adopted.

Therefore, one of the concerns of our work is understanding how the switch to the new technology changes security risks, with the ultimate goal of defining the laws and the procedures regulating electronic elections, that guarantee the same level or a higher level of security. Interestingly, paper voting and the procedures regulating paper elections are not immune to attacks, which can usually be carried out under the hypothesis of multiple ``failures''. For instance, if a ballot is stolen before the election and the polling officers do not report it, it is possible to control how voters vote in a polling station. The usage of electronic devices, however, shifts and ``re-shapes'' some of the risks (see, e.g., [2,3,4,5,6,7]).

Various approaches for specifying, modeling, analyzing, and assessing security have been proposed in the past and have been proven useful for zeroing the security lacks of the software systems under analysis (see, for instance, [8,9,10,11]). However, these techniques are less or otherwise not effective in what we call procedurally rich scenarios, namely situations in which software systems are just part of a more complex organizational setting, in which procedures have to be executed on security-critical assets (belonging both to the digital and to the physical realm). This is exactly the case of (voting and) e-voting, in which even in those countries that have adopted a high level of automation, the executions of procedures and controls, carried out by people on physical assets (e.g. printouts of the digital votes), remains a necessary and unavoidable part (for instance, see detail analysis and evaluation report of the EVEREST project [7]).

We are approaching the problem by reasoning about the procedures and controls that regulate the usage of e-voting systems. We do so by providing formal models of the procedures, by "injecting" threats in such models and by analyzing, through the help of model checkers, the effects of such threats. We believe such an analysis to be essential to, first, identify the security boundaries, that is, the conditions under which procedures can be carried out securely and, secondly, to devise a set of requirement to be applied both at the organizational level and on the (software) systems used.

This paper is structured as follows. In the next section we introduce the ProVotE project, within which this work has been developed. In Section 3, we describe the context of procedural security in detail. In Section 4, we describe our methodology for procedural security analysis and illustrate the approach with snippet example. Section 5 discuses some related work and finally we draw our conclusion in Section 6.