Time, computational complexity, and probability in the analysis of distance-bounding protocols
Time, computational complexity, and probability in the analysis of distance-bounding protocols
复制标题
距离限制协议分析中的时间、计算复杂度和概率
DOI：
--
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
C. Talcott
中科院分区：
文献类型：
--
作者：
M. Kanovich;Tajana Ban Kirigin;Vivek Nigam;A. Scedrov;C. Talcott
许多安全协议依赖于对其协议会话将在其中执行的物理属性的假设。例如，距离边界协议考虑消息的往返时间和传输速度来推断两个代理之间的距离的上限。我们将这种安全协议归类为网络物理协议。时间在许多这些协议的设计和分析中起着关键作用。本文研究了离散时间模型和密集时间模型的基本差异及其对分析的影响。我们表明，有攻击，可以发现模型使用密集的时间，但不是当使用离散时间。我们说明了这一点与一种新的攻击，可以进行大多数距离边界协议。在这种攻击中，利用一个时钟周期内指令的执行延迟来使验证者相信他处于与他的实际位置不同的位置。我们还提出了这种新的攻击的概率分析。作为描述和分析网络物理特性的形式化模型，我们提出了一个适合于描述网络物理安全协议的稠密时间多集重写模型。我们介绍了Circle-Boundary，并表明它们可以用来象征性地解决我们模型的可达性问题，并表明对于重要的平衡理论类，可达性问题是PSPACE完全的。我们还展示了如何使用计算重写工具Maude来实现我们的模型，Maude是自动搜索此类攻击的机器。
Many security protocols rely on the assumptions on the physical properties in which its protocol sessions will be carried out. For instance, Distance Bounding Protocols take into account the round trip time of messages and the transmission velocity to infer an upper bound of the distance between two agents. We classify such security protocols as Cyber-Physical. Time plays a key role in design and analysis of many of these protocols. This paper investigates the foundational differences and the impacts on the analysis when using models with discrete time and models with dense time. We show that there are attacks that can be found by models using dense time, but not when using discrete time. We illustrate this with a novel attack that can be carried out on most Distance Bounding Protocols. In this attack, one exploits the execution delay of instructions during one clock cycle to convince a verifier that he is in a location different from his actual position. We additionally present a probabilistic analysis of this novel attack. As a formal model for representing and analyzing Cyber-Physical properties, we propose a Multiset Rewriting model with dense time suitable for specifying cyber-physical security protocols. We introduce Circle-Configurations and show that they can be used to symbolically solve the reachability problem for our model, and show that for the important class of balanced theories the reachability problem is PSPACE-complete. We also show how our model can be implemented using the computational rewriting tool Maude, the machinery that automatically searches for such attacks.