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

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

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 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
Number of pages21
PublisherSpringer
Publication date2019
Pages535-555
ISBN (Print)9783030299583
DOIs
Publication statusPublished - 2019
EventThe European Symposium on Research in Computer Security - Parc Alvisse Hotel, Luxembourg city, Luxembourg
Duration: 23 Sep 201927 Sep 2019
https://esorics2019.uni.lu/

Conference

ConferenceThe European Symposium on Research in Computer Security
LocationParc Alvisse Hotel
CountryLuxembourg
CityLuxembourg city
Period23/09/201927/09/2019
Internet address
SeriesLecture Notes in Computer Science
Volume11735
ISSN0302-9743

Keywords

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

Cite this

Gondron, S. P. C., & Mödersheim, S. A. (2019). Formalizing and Proving Privacy Properties of Voting Protocols Using Alpha-Beta Privacy. In Proceedings of 24th European Symposium on Research in Computer Security (pp. 535-555). Springer. Lecture Notes in Computer Science, Vol.. 11735 https://doi.org/10.1007/978-3-030-29959-0_26