International Association
for Cryptologic Research

State-of-the-art e-voting systems rely on voters to perform certain

actions to ensure that the election authorities are not manipulating the election result.

This so-called ``end-to-end (E2E) verifiability\'\' is the hallmark

of current e-voting protocols; nevertheless,

thorough analysis of current systems is still far from

being complete.

In this work, we initiate the study of

e-voting protocols as ceremonies.

A ceremony, as introduced by Ellison,

is an extension of the notion of a

protocol that includes human participants as separate nodes of the system that

should be taken into account when performing the security analysis.

We propose a model for secure e-voting ceremonies

that centers on the two properties of end-to-end verifiability

and privacy/receipt-freeness and allows the consideration of

arbitrary behavioral distributions for the human participants.

We then analyze the Helios system

as an e-voting ceremony. Security in the e-voting ceremony model

requires the specification of a class of human behaviors with respect

to which the security properties can be preserved. We show how

end-to-end verifiability is sensitive to human

behavior in the protocol by characterizing the set of behaviors under which

the security can be preserved and also showing explicit scenarios where it fails.