论基础设施攻击者的可靠性

公司与网络运营商进行风险评估，以辅助政策制定、指导基础设施投资或遵从如 ISO 27001 的安全标准。由于这些网络的规模与复杂性，诸如攻击图或攻击树的风险评估技术以有限规则集描述攻击者。这种对攻击者的刻画容易遗漏或夸大攻击向量，可能导致错误的风险估计。在本工作中，我们提出首个证明基于规则的攻击者模型合理性的方法。在概念上，我们在密码学的符号模型之上添加另一层抽象，该符号模型对协议进行推理并抽象化密码学原语。这一新层对互联网规模网络进行推理并抽象化协议。我们一般地展示了如何通过验证迹属性来确保基于规则的模型的可靠性与完备性，将可靠性联系于安全性属性、将完备性联系于活性属性。随后我们针对一个近期提出的、量化互联网上包括 DNS、DNSSEC 与 SMTP 的电子邮件通信机密性的威胁模型演示了该途径。利用现成的协议验证工具，我们发现其威胁模型中的两个缺陷。修正后，我们表明其提供了符号可靠性。