Cybersecurity research · Tokyo

ba-cybersecurity.comResearch by Nobuo Otoi

Verifying Internet standards · IETF SIDROPS, aspa-verification-29 and asra-verification-05

BGP path verification with ASRA could mark a correct route Invalid; the ASPA procedure is proved correct

Status · With the authorsPosted · 29 Oct 2026, SIDROPS listPreprint · Zenodo, 28 Oct 2026

Route leaks send Internet traffic through networks that should not carry it. ASPA lets a BGP router detect them by checking the AS path against signed lists of providers; ASRA is a proposed extension stated to fully preserve that detection. One step of ASRA, as drafted, marks some correct routes Invalid, so a router implementing it could drop legitimate traffic. The ASPA procedure itself was proved correct along the way.

The problem

draft-ietf-sidrops-aspa-verification has reached working-group consensus, and its correctness properties are stated in prose. draft-sriram-sidrops-asra-verification-05 adds fake-link detection on top of it. Step 4 of its downstream enhancement, in both Algorithm A and Algorithm B, checks a range of positions in the path that starts at min_up_ramp + 1. When the origin AS has no ASPA record and the apex of the path is a lateral-peer hop, that range includes a hop that is legitimately a peer, and the path is marked Invalid although it is valley-free, that is, a correct route.

A single AS with correct ASPA and ASRA objects suffices to trigger it; the smallest instance has four ASes.

How it was shown

The counterexample is checkable by hand (below). In an exhaustive enumeration of four-AS topologies, every false positive of ASRA-05 comes from Step 4 (4,608 for each algorithm). Starting the Step 4 range at max_up_ramp + 1 instead of min_up_ramp + 1 removes them all, and the modified step is proved in Lean 4 to fire only on route leaks.

For ASPA itself, Sections 5.3–5.6 of aspa-verification-29 were transcribed into Lean 4 (core library, no sorry, no Classical.choice) and proved, for paths of any length, under the stated assumptions 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 Valid and Invalid coincide with valley-free and route leak. The 25 worked examples published by the ASPA authors are re-checked by decide.

Check it by hand

Route AS0 → AS3 → AS2 → AS1 Up to a provider, across to a peer, down to a customer: no leak. Only AS3 publishes: an ASPA, and an ASRA listing AS2 as a lateral peer. AS0 and AS2 have no ASPA, so min_up_ramp = 1, min_down_ramp = 1, N = 3. Step 4 checks i from (min_up_ramp + 1) to (N - min_down_ramp), so i = 2. AS(2) = AS3 asserts that AS(3) = AS2 is a lateral peer. -05 Invalid fix start at max_up_ramp + 1 = 3: nothing to check, not Invalid

ASRA draft §4.2, Algorithm A · ASPA draft -29

Response

The finding and the proofs were posted to the SIDROPS working group list on 29 Oct 2026 (JST). The same day an author of the ASRA draft replied, thanking for the work and saying they will re-check the algorithms in ASRA-05 and eliminate the issue with the range that was pointed out.

As of 6 Nov 2026, ASRA revision -05 is the current one.

Cite as

Nobuo Otoi (ba-cybersecurity.com). Securing Internet Routing: Machine-Checked Proofs for ASPA Route-Leak Detection and a False-Positive Flaw in the ASRA Extension. 2026. https://doi.org/10.5281/zenodo.23734450.

@misc{otoi2026aspa,
  author       = {Otoi, Nobuo},
  title        = {Securing Internet Routing: Machine-Checked Proofs for ASPA Route-Leak Detection and a False-Positive Flaw in the ASRA Extension},
  year         = {2026},
  doi          = {10.5281/zenodo.23734450},
  publisher    = {Zenodo},
  howpublished = {\url{https://ba-cybersecurity.com/research/aspa-asra-verification/}},
  note         = {Preprint, version 1. Code and proofs: https://github.com/otoinobuo/aspa-verify}
}

Preprint published 28 Oct 2026 · List post and author's reply 29 Oct 2026 (JST) · This page: updated 7 Nov 2026 · Permanent address: https://ba-cybersecurity.com/research/aspa-asra-verification/