Receipt-freeness as a special case of anonymity in epistemic logic

Formal methods have provided us with tools to check both anonymity of protocols and - more specifically - receipt-freeness of voting protocols. One of the frameworks used for proving anonymity is epistemic logic. However, to the best of our knowledge, epistemic logic has never been used to prove receipt-freeness of voting protocols. Still, the concept of indistinguishability used in formalizing anonymity seems to apply to receipt-freeness as well: a vote for one party should be indistinguishable from a vote for another party, even if the voter supplies additional in- formation outside the scope of the protocol. In this paper, we formalize this aspect of anonymity relations, in order to provide an alternative formalization of receipt-freeness in voting protocols, based on epistemic logic.