| ||||
| ||||
![]() Title:N-Tube: Formally Verified Secure Bandwidth Reservation in Path-Aware Internet Architectures Conference:CSF22 Tags:DDoS attacks, formal methods and verification, network security, path-aware Internet architectures and secure bandwidth allocation Abstract: We present N-Tube, a novel, provably secure, inter-domain bandwidth reservation algorithm that runs on a network architecture supporting path-based forwarding. N-Tube reserves global end-to-end bandwidth along network paths in a distributed, neighbor-based, and tube-fair way. It guarantees that benign bandwidth demands are granted available allocations that are immutable, stable, lower-bounded, and fair, even during adversarial demand bursts. We formalize N-Tube and powerful adversaries as a labeled transition system, and inductively prove its safety and security properties. We also apply statistical model checking to validate our proofs and perform an additional quantitative assessment of N-Tube, providing strong guarantees for protection against DDoS attacks. We are not aware of any other complex networked system designs that have been subjected to a comparable analysis of both their qualitative properties (such as correctness and security) and their quantitative properties (such as performance). N-Tube: Formally Verified Secure Bandwidth Reservation in Path-Aware Internet Architectures ![]() N-Tube: Formally Verified Secure Bandwidth Reservation in Path-Aware Internet Architectures | ||||
Copyright © 2002 – 2025 EasyChair |