# Existential Assertions for Voting Protocols

## TL;DR

This paper extends the Dolev-Yao model with existential assertions to analyze voting protocols, providing a formal proof of anonymity for the FOO protocol using this enhanced framework.

## Contribution

It introduces existential abstraction into the model and offers an equivalence-based definition of anonymity, enabling formal verification of voting protocols.

## Key findings

- Proved anonymity of the FOO voting protocol.
- Extended the Dolev-Yao model with existential assertions.
- Provided a formal framework for analyzing voting protocols.

## Abstract

In earlier work, we extend the Dolev-Yao model with assertions. We build on that work and add existential abstraction to the language, which allows us to translate common constructs used in voting protocols into proof properties. We also give an equivalence-based definition of anonymity in this model, and prove anonymity for the FOO voting protocol.