### 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.

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 language | English |
---|---|

Title of host publication | Proceedings of 24th European Symposium on Research in Computer Security |

Number of pages | 21 |

Publisher | Springer |

Publication date | 2019 |

Pages | 535-555 |

ISBN (Print) | 9783030299583 |

DOIs | |

Publication status | Published - 2019 |

Event | The European Symposium on Research in Computer Security - Parc Alvisse Hotel, Luxembourg city, Luxembourg Duration: 23 Sep 2019 → 27 Sep 2019 https://esorics2019.uni.lu/ |

### Conference

Conference | The European Symposium on Research in Computer Security |
---|---|

Location | Parc Alvisse Hotel |

Country | Luxembourg |

City | Luxembourg city |

Period | 23/09/2019 → 27/09/2019 |

Internet address |

Series | Lecture Notes in Computer Science |
---|---|

Volume | 11735 |

ISSN | 0302-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