CRFeb 16, 2017
Existential Assertions for Voting Protocols
arXiv:1702.05000v14 citations
Originality Synthesis-oriented
AI Analysis
This work addresses security verification for voting protocols, but it is incremental as it builds on prior extensions to the Dolev-Yao model.
The authors tackled the problem of verifying anonymity in voting protocols by extending a formal model with existential abstraction to translate protocol constructs into proof properties, and they proved anonymity for the FOO voting protocol.
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.