Abstract
A voting system should not merely report the outcome: it should also provide
sufficient evidence to convince reasonable observers that the reported outcome
is correct. Many deployed systems, notably paperless DRE machines still in use
in US elections, fail certainly the second, and quite possibly the first of
these requirements. Rivest and Wack proposed the principle of software
independence (SI) as a guiding principle and requirement for voting systems. In
essence, a voting system is SI if its reliance on software is
``tamper-evident'', that is, if there is a way to detect that material changes
were made to the software without inspecting that software. This important
notion has so far been formulated only informally.
Here, we provide more formal mathematical definitions of SI. This exposes
some subtleties and gaps in the original definition, among them: what elements
of a system must be trusted for an election or system to be SI, how to
formalize ``detection'' of a change to an election outcome, the fact that SI is
with respect to a set of detection mechanisms (which must be legal and
practical), the need to limit false alarms, and how SI applies when the social
choice function is not deterministic.