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

Sébastien Pierre Christophe Gondron, Sebastian Alexander Mödersheim

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

93 Downloads (Pure)


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 receiptfreeness 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.
Original languageEnglish
Title of host publicationProceedings of 24th European Symposium on Research in Computer Security
Publication date2019
ISBN (Print)9783030299583
Publication statusPublished - 2019
EventThe European Symposium on Research in Computer Security - Parc Alvisse Hotel, Luxembourg city, Luxembourg
Duration: 23 Sep 201927 Sep 2019


ConferenceThe European Symposium on Research in Computer Security
LocationParc Alvisse Hotel
CityLuxembourg city
Internet address
SeriesLecture Notes in Computer Science


  • Formal security models
  • Logic and verification
  • Privacy preserving systems
  • Voting protocols
  • Receipt-freeness
  • Security requirements
  • Security protocols

Cite this