Receipt-freeness: formal definition and fault attacks
Stephanie Delaune, Steve Kremer, Mark Ryan (France Telecom R&D, France School of Computer Science, University of Birmingham)
In this paper we propose a formalisation of receipt-freeness in terms of observational equivalence in the applied
pi calculus. The formalisation of receipt-freeness is non trivial and gives interesting insights. Among others, our
formalisation highlights a new kind of fault attacks. The idea of a fault attack is to let the coercer test the loyalty of a
coerced voter. It may work in protocols in which the coercer gives the voter messages that the voter should use during
the protocol. The coercer can send a garbage message to the voter. If the voter is unable to decide whether the message
is garbage or not, the attacker may distinguish a voter who follows the coercer’s instructions from a voter who is trying
to cheat the coercer, as the protocol would block on the incorrect message. Verifying whether a message is correct
or not is often difficult when, for instance, ciphertexts are sent. In practice, a coercer can use this technique to check
whether a coerced voter is behaving as expected. We illustrate the attack on a simple protocol inspired by a voting
protocol proposed by Lee et al.