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  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.  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  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.