Formalizing and Proving Privacy Properties of Voting Protocols Using Alpha-Beta Privacy

Abstract

Most common formulations of privacy-type properties for security protocols are specified as bisimilarity of processes in applied- π calculus. For instance, voting privacy is specified as the bisimilarity between two processes that differ only by a swap of two votes. Similar methods are applied to formalize receipt-freeness. We believe that there exists a gap between these technical encodings and an intuitive understanding of these properties. We use (α, β) -privacy to formalize privacy goals in a different way, namely as a reachability problem. Every state consists of a pair of formulae: α expresses the publicly released information (like the result of the vote) and β expresses the additional information available to the intruder (like observed messages). Privacy holds in a state if every model of α can be extended to a model of β, i.e., the intruder cannot make any deductions beyond what was deliberately released; and privacy of a protocol holds if privacy holds in every reachable state. This allows us to give formulations of voting privacy and receipt-freeness that are more declarative than the common bisimilarity based formulations, since we reason about models that are consistent with all observations like interaction with coerced (but potentially lying) voters. Also, we show a relation between the goals: receipt-freeness implies voting privacy. Finally, the logical approach also allows for declarative manual proofs (as opposed to long machine-generated proofs) like reasoning about a permutation of votes and the intruder’s knowledge about that permutation.