CPDY：通过物理层交互扩展Dolev-Yao攻击器
CPDY: Extending the Dolev-Yao Attacker with Physical-Layer Interactions
摘要：
我们提出了扩展Dolev-Yao攻击者模型，使其适用于有关网络物理系统安全性的争论。Dolev-Yao攻击者模型使用一组规则来定义攻击者在协议执行期间关于各方之间交换的消息（即信息）的潜在动作。由于传统的Dolev-Yao模型只考虑信息（通过攻击者控制的信道交换），因此该模型不能直接用于讨论物理层交互可能存在的网络物理系统的安全性。我们的Dolev-Yao扩展，称为网络物理Dolev-Yao（CPDY）攻击者模型，允许各方之间的额外正交交互通道。特别地，这种正交通道可以用于对部件之间的物理层机械、化学或电相互作用进行建模。此外，我们还讨论了包括物理属性，如位置或距离的规则集。我们为Dolev-Yao攻击者提供了一组额外规则的示例，使用这些规则，我们能够正式发现以前只能通过经验方法或详细的物理过程模型发现的物理攻击。
英文摘要：
We propose extensions to the Dolev-Yao attacker model to make it suitable for arguments about security of Cyber-Physical Systems. The Dolev-Yao attacker model uses a set of rules to define potential actions by an attacker with respect to messages (i.e. information) exchanged between parties during a protocol execution. As the traditional Dolev-Yao model considers only information (exchanged over a channel controlled by the attacker), the model cannot directly be used to argue about the security of cyber-physical systems where physical-layer interactions are possible. Our Dolev-Yao extension, called cyber-physical Dolev-Yao (CPDY) attacker model, allows additional orthogonal interaction channels between the parties. In particular, such orthogonal channels can be used to model physical-layer mechanical, chemical, or electrical interactions between components. In addition, we discuss the inclusion of physical properties such as location or distance in the rule set. We present an example set of additional rules for the Dolev-Yao attacker, using those we are able to formally discover physical attacks that previously could only be found by empirical methods or detailed physical process models.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
