  We advance the state-of-the-art in automated symbolic analysis for e-voting
protocols by introducing three conditions that together are sufficient to
guarantee ballot secrecy. There are two main advantages to using our
conditions, compared to existing automated approaches. The first is a
substantial expansion of the class of protocols and threat models that can be
automatically analysed: we can systematically deal with (a) honest authorities
present in different phases, (b) threat models in which no dishonest voters
occur, and (c) protocols whose ballot secrecy depends on fresh data coming from
other phases. The second advantage is that it can significantly improve
verification efficiency, as the individual conditions are often simpler to
verify. E.g., for the LEE protocol, we obtain a speedup of over two orders of
magnitude. We show the scope and effectiveness of our approach using ProVerif
in several case studies, including FOO, LEE, JCJ, and Belenios. In these case
studies, our approach does not yield any false attacks, suggesting that our
conditions are tight.
