Today’s Internet interdomain routing protocol, the Border Gateway Protocol (BGP), is increasingly complicated and fragile due to policy misconfig- urations by individual autonomous systems (ASes). These misconfigurations are often difficult to manually diagnose beyond a small number of nodes due to the state explosion problem. To aid the diagnosis of potential anomalies, researchers have developed various formal models and analysis tools. However, these tech- niques do not scale well or do not cover the full set of anomalies. Current tech- niques use oversimplified BGP models that capture either anomalies within or across ASes, but not the interactions between the two. To address these limita- tions, we propose a novel approach that reduces network size prior to analysis, while preserving crucial BGP correctness properties. Using Maude, we have de- veloped a toolkit that takes as input a network instance consisting of ASes and their policy configurations, and then performs formal analysis on the reduced instance for safety (protocol convergence). Our results show that our reduction- based analysis allows us to analyze significantly larger network instances at low reduction overhead.