A Methodology for Assessing Procedural Security: A Case Study in E-Voting

The organization of elections 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. In this paper we present a methodology for procedural security assessment in order to analyze and eventually make election secure. Our approach is based on modeling the nominal procedures implementation in the form of business process models (which we write in a strict simplified subset of UML), systematically translate the models into executable specification and perform the analysis. We believe such an analysis to be essential to identify the limits of the current procedures (i.e. undetected attacks) and to identify more precisely under what hypotheses we can guarantee secure elections. We demonstrate our approach with the help of an excerpt of e-Voting system scenario that it is derived from the current experimentation of the Italian legislation.