Formalization of Receipt-Freeness in the Context of Electronic Voting

The secret nature of elections is of major importance to guarantee free and democratic elections. Due to it´s importance it has to be enforced even against the voter himself. I.e. every (electronic) voting system has to ensure that the voter does not gain any receipt that enables him to prove his voting decision to others. In this paper we present a formal model addressing the security requirement of receipt-freeness for electronic voting systems. This formal model can bee seen as a step towards a formal security model which enables the Common Criteria evaluation and certification of online voting products according to Evaluation Assurance Level EAL 5 or higher. Thus, it can help to strengthen the trust of the voters in the voting system.