Role Interchange for Anonymity and Privacy of Voting

摘要

We propose a new information-hiding property called role interchangeability for the verification of the anonymity and privacy of security protocols. First, we formally specify the new property in multi-agent systems, and describe its relationship with known anonymity properties that are also defined in multi-agent systems. Moreover, we define privacy in a way that is symmetric with anonymity, and show that exploiting this symmetry is useful for deriving anonymity and privacy from role interchangeability. Next, we show a way of verifying the new property. We show that role interchangeability in a multi-agent system is characterized by the existence of role-interchange functions on the set of traces corresponding to the system. In addition, a simulation proof method is presented to prove the existence of the functions for a protocol described as an automaton. Finally, as a case study, we apply our method to the formal verification of the FOO electronic voting protocol.