基于主动入侵者模型的投票系统CSP自动化分析
密码学与安全
2017-05-03 v1
摘要
本文提出了一种新颖的入侵者模型，用于投票系统匿名性（投票隐私）和保密性的自动化推理。为此，我们采用惰性间谍(lazy spy)，因其避免了不必要推导的急切预计算，从而减少了分析所需的状态空间。该强大入侵者的行为类似于Dolev-Yao入侵者，不仅观察协议运行，还与协议参与者交互，窃听通信信道，截获并伪造其从任何先验知识中学习或生成的任何消息。我们针对现有信道类型和推导系统做了若干重要修改。对于前者，我们为不同威胁模型定义了多种信道类型。对于后者，我们在投票系统模型中传输的消息空间上构建了一个大型推导系统。该模型代表了对vVote系统的首次形式化处理，该系统于2014年11月用于澳大利亚维多利亚州的州选举。
引用
@article{arxiv.1705.00795,
title = {Automated Analysis of Voting Systems under an Active Intruder Model in CSP},
author = {Murat Moran and James Heather},
journal= {arXiv preprint arXiv:1705.00795},
year = {2017}
}