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.