Modelchecking Safety Properties in Randomized Security Protocols. In: Nigam V. et al. (eds) Logic, Language, and Security.
Modelchecking Safety Properties in Randomized Security Protocols. In: Nigam V. et al. (eds) Logic, Language, and Security.
复制标题
随机安全协议中的模型检查安全属性。
DOI：
10.1007/978-3-030-62077-6_12
复制
发表时间：
2020
期刊：
影响因子：
--
通讯作者：
Matt S. Bauer, Rohit Chadha
中科院分区：
文献类型：
--
作者：
Matt S. Bauer, Rohit Chadha
用于安全协议的自动推理工具将协议建模为通过Dolev-Yao攻击者进行通信的不确定性过程。然而，有一大类协议的正确性依赖于对随机性进行建模和推理的明确能力。尽管这些协议是许多广泛采用的匿名通信系统的核心，但迄今为止，它们还没有得到自动验证技术的支持。提出了一种随机协议安全属性推理算法。该算法是作为随机协议分析器（Stochastic Protocol ANalyzer, Span）的扩展而实现的，该工具是分析随机协议不可区分特性的机械化工具。使用Span，我们对几个随机安全协议进行了第一次自动验证，并在我们分析的几个协议中发现了以前未知的设计弱点。
Automated reasoning tools for security protocols model protocols as non-deterministic processes that communicate through a Dolev-Yao attacker. There are, however, a large class of protocols whose correctness relies on an explicit ability to model and reason about randomness. Although such protocols lie at the heart of many widely adopted systems for anonymous communication, they have so-far eluded automated verification techniques. We propose an algorithm for reasoning about safety properties for randomized protocols. The algorithm is implemented as an extension of Stochastic Protocol ANalyzer (Span), the mechanized tool that reasons about the indistinguishability properties of randomized protocols. Using Span, we conduct the first automated verification on several randomized security protocols and uncover previously unknown design weaknesses in several of the protocols we analyzed.