Formal Verification of Secure Forwarding Protocols
OPEN ACCESS
Loading...
Author / Producer
Date
2021-06
Publication Type
Conference Paper
ETH Bibliography
yes
Citations
Altmetric
OPEN ACCESS
Data
Rights / License
Abstract
Today’s Internet is built on decades-old networking protocols that lack scalability, reliability, and security. In response, the networking community has developed path-aware Internet architectures that solve these issues while simultaneously empowering end hosts. In these architectures, autonomous systems construct authenticated forwarding paths based on their routing policies. Each end host then selects one of these authorized paths and includes it in the packet header, thus allowing routers to efficiently determine how to forward the packet. A central security property of these architectures is path authorization, requiring that packets can only travel along authorized paths. This property protects the routing policies of autonomous systems from malicious senders.The fundamental role of packet forwarding in the Internet and the complexity of the authentication mechanisms employed call for a formal analysis. In this vein, we develop in Isabelle/HOL a parameterized verification framework for path-aware data plane protocols. We first formulate an abstract model without an attacker for which we prove path authorization. We then refine this model by introducing an attacker and by protecting authorized paths using (generic) cryptographic validation fields. This model is parameterized by the protocol’s authentication mechanism and assumes five simple verification conditions that are sufficient to prove the refinement of the abstract model. We validate our framework by instantiating it with several concrete protocols from the literature and proving that they each satisfy the verification conditions and hence path authorization. No invariants must be proven for the instantiation. Our framework thus supports low-effort security proofs for data plane protocols. The results hold for arbitrary network topologies and sets of authorized paths, a guarantee that state-of-the-art automated security protocol verifiers cannot currently provide.
Permanent link
Publication status
published
External links
Editor
Book title
2021 IEEE 34th Computer Security Foundations Symposium (CSF)
Journal / series
Volume
Pages / Article No.
9505227
Publisher
IEEE
Event
34th IEEE Computer Security Foundations Symposium (CSF 2021)
Edition / version
Methods
Software
Geographic location
Date collected
Date created
Subject
network-security; security-protocols; Isabelle/HOL; formal-verification; data-plane; parametrized-verification
Organisational unit
03634 - Basin, David / Basin, David
Notes
Conference lecture held on June 23, 2021