  This article presents a novel intruder model for automated reasoning about
anonymity (vote-privacy) and secrecy properties of voting systems. We adapt the
lazy spy for this purpose, as it avoids the eagerness of pre-computation of
unnecessary deductions, reducing the required state space for the analysis.
This powerful intruder behaves as a Dolev-Yao intruder, which not only observes
a protocol run but also interacts with the protocol participants, overhears
communication channels, intercepts and spoofs any messages that he has learned
or generated from any prior knowledge.
  We make several important modifications in relation to existing channel types
and the deductive system. For the former, we define various channel types for
different threat models. For the latter, we construct a large deductive system
over the space of messages transmitted in the voting system model. The model
represents the first formal treatment of the vVote system, which was used in
November 2014, in state elections in Victoria, Australia.
