On the Soundness of Infrastructure Adversaries
Alexander Dax, Robert K\"unnemann

TL;DR
This paper introduces a methodology to validate rule-based attacker models in network security, ensuring their soundness and completeness through formal verification, and demonstrates its effectiveness by identifying flaws in a threat model for email confidentiality.
Contribution
It proposes a novel layered approach to justify attacker models by linking symbolic cryptography reasoning with network protocol abstractions.
Findings
Verified the soundness of a threat model for email confidentiality.
Discovered and fixed two flaws in a recent threat model.
Ensured symbolic soundness of the threat model after corrections.
Abstract
Companies and network operators perform risk assessment to inform policy-making, guide infrastructure investments or to comply with security standards such as ISO 27001. Due to the size and complexity of these networks, risk assessment techniques such as attack graphs or trees describe the attacker with a finite set of rules. This characterization of the attacker can easily miss attack vectors or overstate them, potentially leading to incorrect risk estimation. In this work, we propose the first methodology to justify a rule-based attacker model. Conceptually, we add another layer of abstraction on top of the symbolic model of cryptography, which reasons about protocols and abstracts cryptographic primitives. This new layer reasons about Internet-scale networks and abstracts protocols. We show, in general, how the soundness and completeness of a rule-based model can be ensured by…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
