To our knowledge, so far, formal procedural security analysis
is quite an unexplored area. However, various work have been going on the
representation and effective implementation of e-voting procedures using business
process notations. In this area, the work closest in
spirit to ours can be found in [20,21], where the
authors argue the need for procedural security in electronic elections
and provide various examples of procedural risks occurred during trials
in UK. The same authors in [22] also investigate the
need for applying business process re-engineering to electoral process.
Our focus, however, is on the technical machinery to automate analyses.
In [23,24], the authors stress the
importance to define roles and responsibilities within the e-voting process in
order to come with a better understanding of electoral processes. Our approach
complement and possibly extend these works by providing tools to support such
analyses.
Last but not least, Volha et al. [25] presented an approach
to reason on security properties of the to-be models (which are
derived from as-is model) in order to evaluate procedural
alternatives in e-voting systems. In particular, using formal approach
(using Datalog [26] and its underlying theorem prover)
they express and verify security concerns (such as, delegation of
responsibility among untrusted parties, trust conflict and so on).
The aim is that of
understanding problematic trust/delegation relationships and
eventually finding ways to adopt a solution to the detected security
properties violations.