改进电子投票协议的自动化符号分析：基于选票保密充分条件的方法
密码学与安全
2019-03-18 v5
摘要
我们通过引入三个共同足以保证选票保密的条件，推进了电子投票协议自动化符号分析的最新水平。与现有自动化方法相比，使用我们的条件有两个主要优势。第一是可自动分析的协议类和威胁模型类大幅扩展：我们能系统地处理（a）不同阶段存在的诚实权威，（b）不存在不诚实投票者的威胁模型，以及（c）选票保密依赖于来自其他阶段的新鲜数据的协议。第二个优势是能显著提高验证效率，因为单个条件通常更易验证。例如，对于LEE协议，我们获得了两个数量级以上的加速。我们通过在ProVerif中的若干案例研究（包括FOO、LEE、JCJ和Belenios）展示了我们方法的范围和有效性。在这些案例研究中，我们的方法未产生任何虚假攻击，表明我们的条件是紧致的。
引用
@article{arxiv.1709.00194,
title = {Improving Automated Symbolic Analysis for E-voting Protocols: A Method Based on Sufficient Conditions for Ballot Secrecy},
author = {Cas Cremers and Lucca Hirschi},
journal= {arXiv preprint arXiv:1709.00194},
year = {2019}
}
备注
Accepted for publication at EURO S&P 2019