Modeling and Analysis of Procedural Security in (e)Voting:
the Trentino's Approach and Experiences
This paper describes the experiences and the challenges we are facing within
the ProVotE project, a four years project sponsored by the Autonomous Province of
Trento that has the goal of switching to e-voting for local elections.
One of the activities we are carrying out within ProVotE is the systematic
analysis of the weaknesses and strengths of the procedures regulating local
elections in Italy, in order to derive possible attacks and their effects.
The approach we take is based on providing formal specifications of the
procedures and using model checkers to help us analyze the effects of
attacks. We believe such an analysis to be essential to identify the limits
of the current procedures (i.e. under what hypotheses attacks are
undetectable) and to identify more precisely under what hypotheses and
conditions we can guarantee reasonably secure electronic elections.
This paper presents the methodology and the techniques we are devising and
experimenting with to tackle problem highlighted above.