English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

We advance the state-of-the-art in automated symbolic analysis for e-votingprotocols by introducing three conditions that together are sufficient toguarantee ballot secrecy. There are two main advantages to using ourconditions, compared to existing automated approaches. The first is asubstantial expansion of the class of protocols and threat models that can beautomatically analysed: we can systematically deal with (a) honest authoritiespresent in different phases, (b) threat models in which no dishonest votersoccur, and (c) protocols whose ballot secrecy depends on fresh data coming fromother phases. The second advantage is that it can significantly improveverification efficiency, as the individual conditions are often simpler toverify. E.g., for the LEE protocol, we obtain a speedup of over two orders ofmagnitude. We show the scope and effectiveness of our approach using ProVerifin several case studies, including FOO, LEE, JCJ, and Belenios. In these casestudies, our approach does not yield any false attacks, suggesting that ourconditions are tight.

Improving Automated Symbolic Analysis for E-voting Protocols: A Method Based on Sufficient Conditions for Ballot Secrecy