Securing Internet Routing: Machine-Checked Proofs for ASPA Route-Leak Detection and a False-Positive Flaw in the ASRA Extension

Route leaks—BGP announcements that send Internet traffic through networks that should not carry it—have repeatedly caused large outages and traffic interception. ASPA (Autonomous System Provider Authorization) lets BGP speakers detect route leaks by checking an AS_PATH against RPKI-signed lists of provider ASes. The verification procedure of draft-ietf-sidrops-aspa-verification has reached working-group consensus, and its correctness properties are stated in prose (Section 5.2 and Appendix B of the draft). We transcribe Sections 5.3–5.6 and prove in Lean 4, for paths of any length, assuming that business relationships are seen consistently from both ends and that every registered ASPA lists exactly the providers of its AS: the procedure never marks a valley-free path Invalid; a Valid outcome implies the path is valley-free; Property 1 of Appendix B holds; and under full deployment the procedure never returns Unknown, so that Valid and Invalid coincide exactly with valley-free and route leak. We then analyse ASRA (Autonomous System Relationship Authorization), a proposed extension that adds fake-link detection and is stated to “fully preserve the route leak detection capabilities of ASPA”. Step 4 of its downstream enhancement, in both Algorithm A and Algorithm B, marks valley-free paths Invalid: when the origin has no ASPA and the apex of the path is a lateral-peer hop, a single AS with correct ASPA and ASRA objects suffices. The smallest instance has four ASes, and in exhaustive enumeration of four-AS topologies every false positive comes from Step 4. Starting the Step 4 range at max_up_ramp + 1 instead of min_up_ramp + 1 removes the flaw; we prove in Lean that the modified step fires only on route leaks. We also record a consequence of ASPA for AS-path poisoning. This record contains the paper (PDF and LaTeX source) and the artifacts: the Lean 4 development (core Lean, no sorry, no Classical.choice) and the Python transcriptions and exhaustive checkers. Code is licensed under Apache-2.0; the paper under CC BY 4.0. Repository: https://github.com/otoinobuo/aspa-verify