We are involved in a project named ProVotE  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 ).
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.